1: \documentclass[11pt]{article}
2: \usepackage{setspace}
3: \usepackage{times}
4: \usepackage{algorithm}
5: \usepackage{algorithmic}
6: \usepackage{eucal}
7: \usepackage{amsfonts}
8: \usepackage{verbatim}
9:
10: \def\blackbox{{\rule{1.5mm}{1.5mm}}}
11: \def\sol{{\tt sol} }
12: \def\bool{{\tt bool} }
13: \def\fun{{\tt fun} }
14: \def\img{{\tt img} }
15: \def\called{{\tt do} }
16:
17: \def\S{{\cal S} }
18: \def\A{{\cal A} }
19: \def\T{{\cal T} }
20: \def\C{{\cal C} }
21: \newcommand{\email}[1]{${\tt #1}$}
22: \newtheorem{proposition}{Proposition}
23: \newtheorem{example}{Example}
24:
25: \title
26: {
27: Constraint-based \mbox{analysis} of composite solvers\thanks
28: {
29: Financially supported
30: by Centre Franco-Russe Liapunov (Project 06--98) and
31: by European project COCONUT IST--2000--26063.
32: }
33: }
34: \date{}
35:
36: \author
37: {
38: Evgueni Petrov\\
39: Ecole des Mines de Nantes\\
40: La Chantrerie, 4 rue Kastler, B.P.20722\\
41: 44307 Nantes Cedex 03 France\\
42: \email{evgueni.petrov@emn.fr}
43: \and
44: \'Eric Monfroy\\
45: Universit\'e de Nantes\\
46: 2 Houssini\`ere, 44300 Nantes Cedex 03 France\\
47: \email{eric.monfroy@irin.univ-nantes.fr}
48: }
49:
50: \begin{document}
51: \doublespace
52:
53: \maketitle
54:
55: \begin{abstract}
56: Cooperative constraint solving is an area of constraint programming
57: that studies the interaction between constraint solvers with the aim of discovering the interaction patterns that amplify the positive qualities of individual solvers.
58: Automatisation and formalisation of such studies is an important issue of cooperative constraint solving.
59:
60: In this paper we present a constraint-based \mbox{analysis} of composite solvers that integrates reasoning about the individual solvers and the processed data.
61: The idea is to approximate this reasoning by resolution of set constraints on the finite sets representing the predicates that express all the necessary properties.
62: We illustrate application of our analysis to two important cooperation patterns: deterministic choice and loop.
63:
64: \end{abstract}
65:
66:
67: \section{Introduction}
68: \label{intro}
69:
70: Cooperative constraint solving is an area of constraint programming
71: that studies interaction between constraint solvers with the aim of discovering the interaction patterns that amplify the positive qualities of individual solvers.
72: Papers \cite{coop:jaffar-michaylov-stuckey-yap-acm-92,coop:beringer-backer-lp-elsevier-95,coop:marti-rueher-jait-95,vH-numerica,coop:hickey-lncs-00}
73: describe some examples of successful cooperative constraint solving systems.
74:
75: At the present time, successful patterns of cooperation are detected with the sole help of
76: intuition, feelings, experience, and experiments with software engineering tools supporting cooperative constraint solving
77: such as \cite{ECLIPSE00,PROLOGIV,MOZART,coop:monfroy-frocos-00}.
78: One cannot make such experiments systematic without a mathematical framework for analysis of cooperative constraint solving systems (``composite solvers'').
79:
80: An important practical application for such a framework is integration and development of domain-specific software.
81: The expected applications for the analysis are
82: detection of inconsistencies in the specifications of individual software packages and
83: construction of the specifications for the packages needed in order to meet the requirements on the over-all functionality.
84: The COCONUT project is an example of such software development project in the domain of numerical optimization and constraint programming.
85:
86: The authors of \cite{coop:granvilliers-monfroy-benhamou-issac-01}
87: illustrate practical importance of \mbox{analysis} of composite solvers with examples from interval constraint programming.
88: They point out two aspects of this analysis:
89: (a) detection of good cooperation strategies subject to expectations from the composite solver and the individual solvers in hand;
90: (b) reasoning about the properties of individual solvers subject to the expectations from the composite solver.
91: In this paper we focus on the latter aspect.
92:
93: Certain properties of composite solvers are expressible in terms of the properties of the processed {\em data}.
94: One can study the properties of this sort using the frameworks of software verification, programming logics, model checking program analysis.
95: In order to reason about the properties of {\em individual solvers} one needs a new kind of analysis.
96:
97: In this paper we present a constraint-based \mbox{analysis} of the composite solvers
98: that integrates reasoning about the individual solvers and the processed data.
99: The idea is to approximate this reasoning by resolution of set constraints on the finite sets representing the predicates that express all the necessary properties.
100: We illustrate application of our analysis to two important cooperation patterns: deterministic choice and loop.
101:
102: Before going further we give a quick motivational example.
103:
104: \begin{example}[Motivation]
105:
106: Suppose that we, rather ``engineers'' than experts in global optimization,
107: have in hand a library of numerical algorithms that includes the standard methods for local and global optimization, different tests, etc.
108: and develop a software for minimization of quadratic functions (quadratic programming).
109: Algorithm \ref{motivation-ex} specifies the composite solver that we have built with the intention to avoid the costly exhaustive search in the case of convex objective functions.
110:
111: \begin{algorithm}
112: \begin{algorithmic}
113: \IF{ $f$ is convex }
114: \STATE solve $x=\arg\min_{x\ge 0} f$ by the method of steepest descent
115: \ELSE
116: \STATE solve $x=\arg\min_{x\ge 0} f$ by the exhaustive search
117: \ENDIF
118: \end{algorithmic}
119: \caption
120: { A na\"\i{}ve composite solver for quadratic programming.
121: }
122: \label{motivation-ex}
123: \end{algorithm}
124:
125: Our logic is as follows:
126: if the graph of the objective is like a tea-cup (``convex''), then we use the steepest descent to go to its lowest point; otherwise we do the exhaustive search.
127: Will this work?
128: Well, sometimes: we have not thought of the objectives that are convex and unbounded from below in the orthant $x\ge 0$, e.g. $f(x_1,x_2)=(x_1-x_2)^2-x_1$.
129: The method of steepest descent may fail to terminate in this case.
130:
131: How can we detect similar situations automatically?
132: How do we change a composite solver in order that it work correctly?
133: In this paper we propose a formalism suitable for this kind of \mbox{analisys}.
134:
135: \end{example}
136:
137: The paper is structured as follows.
138: In Section \ref{coop-model} we introduce the basic notions of the paper and describe the operation of composite solvers.
139: In Section \ref{infinite-calc} we describe a technique for reasoning about composite solvers in terms of constraints on finite sets.
140: In this Section \ref{examples} we explain how to express certain properties of the composite solvers in terms of set constraints.
141: Section \ref{conclusion} concludes the paper.
142:
143: \section{Solvers, contexts, operation model}
144: \label{coop-model}
145:
146: In this section we introduce the basic notions of the paper and describe the operation of composite solvers.
147:
148: A set of individual solvers that interact and exchange some data through a shared data store is called {\em composite solver}.
149: We number the individual solvers by integers from 1 to $n$.
150: The content of the data store, called {\em context}, is divided into {\em control data} and {\em application specific data}.
151: The control data specify the set of the individual solvers that ``are called''.
152: In the constraint programming framework the application specific data are, usually, specifications in some declarative language.
153: The set of all contexts is denoted $\C$.
154:
155: The operation of the composite solver is divided into ticks.
156: At the beginning of a tick every solver $s$ checks the control data and either changes some part of the context if it is called, or does nothing otherwise.
157: The initial context is provided by the user of the composite solver.
158: Thus our composite solvers are either sequential or synchronous bulk parallel systems.
159:
160: A solver $s$ determines a transformation $F_s:\C\to \C$ of the contexts at the beginning of the ticks into the contexts at the end of the ticks.
161: The synchronous modifications of the data store must be coherent, that is, $F_s(c)=F_{s'}(c)$
162: for any context $c$ that contains the control data indicating that solvers $s$ and $s'$ are called.
163:
164: A context is {\em feasible}, if it is generated from the initial context by some sequence of the transformations $F_s$'s where $s$'s are some solvers.
165:
166: Now we proceed to the description of our constraint-based formalism.
167:
168: \section{From composite solvers to finite sets}
169: \label{infinite-calc}
170:
171: In this section we describe a technique for reasoning about composite solvers in terms of constraints on finite sets.
172: We axiomatize the operation model from Section \ref{coop-model} in the first order logic and
173: view the axioms as set constraints on the interpretation of the symbols involved therein.
174: Since the exact solutions to these constraints may be (non-constructible explicitly) infinite sets,
175: we solve our set constraints approximately modulo a finite set of clusters of the contexts $\C$.
176: We assume that the reader is familiar with the generic concepts of constraint and constraint satisfaction.
177:
178: The axioms in question are written in terms of
179: a constant symbol $c_0$ denoting the initial context,
180: a unary predicate symbol $p$ denoting the set of feasible contexts and
181: unary function symbols $f_s$'s denoting the transformations $F_s$.
182: The axioms are plain and open ($n$ is the number of individual solvers):
183: \begin{eqnarray}
184: &&p(c_0) \label{first-ax}\\
185: &&\forall c\; p(c)\wedge f_s(c)=c' \Longrightarrow p(c') \quad s=1,\ldots,n \label{next-ax}\\
186: &&\forall c' \exists c\; p(c') \wedge c'\ne c_0 \Longrightarrow \left(c'=f_1(c)\vee\ldots\vee c'=f_n(c)\right)\wedge p(c) \label{last-ax}
187: \end{eqnarray}
188:
189: The axiom (\ref{first-ax}) states that the initial context is feasible.
190: The $n$ axioms (\ref{next-ax}) say that the transformations $F_s$'s map feasible contexts onto themselves.
191: The axiom (\ref{last-ax}) states that every feasible context except the initial one has a feasible pre-image under some transformation $F_s$.
192:
193: The axioms (\ref{first-ax})--(\ref{last-ax}) are nothing else than
194: constraints on the interpretation $\dot{c_0}$, $\dot{p}$ and $\dot{f_s}$'s, in the model-theoretic sense, of the symbols $c_0$, $p$ and $f_s$'s.
195: One can write down these constraints are as follows:
196: \begin{eqnarray}
197: &\fun\left(\dot{f_1}\right), \ldots, \fun\left(\dot{f_n}\right)& \label{first-cnt}\\
198: &\dot{p} = \{\dot{c_0}\} \cup \img\left(\dot{f_1},\dot{p}\right) \cup \cdots \cup \img\left(\dot{f_n},\dot{p}\right)& \label{last-cnt}
199: \end{eqnarray}
200: The domains of $\dot{c_0}$, $\dot{p}$ and $\dot{f_s}$'s consist of the contexts $\C$, of all the subsets of $\C$ and, respectively, of all the binary relations on $\C$.
201: The symbols $=$ and $\cup$ denote equality and union of subsets of $\C$.
202: The symbol $\fun$ denotes the constraint ``is a function from $\C$ to $\C$''.
203: The symbol $\img$ denotes the image of a subset of $\C$ under a binary relation on $\C$.
204:
205: Since many exact solutions to the constraints (\ref{first-cnt})--(\ref{last-cnt}) involve infinite sets,
206: we sacrifice precision for tractability and group the individual contexts from $\C$ into finitely many clusters called {\em context properties}, denoted $\C^\star$.
207: A binary relation on $\C^\star$ whose domain is $\C^\star$ is called {\em abstract solver}.
208: A context property $c^\star$ {\em approximates} a context $c$, iff $c\in c^\star$.
209: A set $P^\star$ of context properties {\em approximates} a set $P\subseteq\C$, iff $P\subseteq \cup P^\star$.
210: An abstract solver $R^\star$ {\em approximates} a binary relation $R\subseteq \C^2$, iff $R\subseteq \cup R^\star$.
211:
212: \begin{example}[Hull Consistency in sharpness analysis]
213:
214: \def\acycl{{\tt tree}}
215: \def\compl{{\tt ok}}
216:
217: Consider the Hull Consistency (HC) algorithm \cite{opt:benhamou-goualard-granvilliers-iclp-99} from interval constraint programming.
218: Given a set $i$ of interval constraints, this algorithm computes a box $b$ that bounds the set $\sol(i)$ of the solutions to $i$.
219: Let the context specify the constraints $i$, the box $b$, and the necessary control data (of no interest at the moment).
220:
221: The well-known fact about the HC algorithm is that it bounds the set $\sol(i)$ sharply, i.e. $b$ cannot be improved without losing a solution to $i$,
222: if $i$ has an acyclic constraint graph (see \cite{intervals:hansen-reliable-comp-97}).
223: We can express this fact in terms of the context properties ``$i$ has an acyclic constraint graph'' (abbreviated $\acycl$) and ``$b=\sol(i)$'' (abbreviated $\compl$)
224: by the abstract solver $HC^\star=\left\{\left(\acycl,\compl\right)\;\left(\C,\C\right)\;\left(\compl,\compl\right)\right\}$.
225: For example, $(\acycl,\compl) \in HC^\star$ means that the HC algorithm bounds $\sol(i)$ sharply, if $i$ has an acyclic constraint graph.
226:
227: \end{example}
228:
229: \begin{proposition}[Correctness]
230: If $\dot{c_0}\in\C^\star$, $\dot{p}\subseteq \C^\star$ and abstract solvers $\dot{f_s}$'s approximate some solution to the constraints (\ref{first-cnt})--(\ref{last-cnt}),
231: then they satisfy these same constraints with respect to the following definition of $=$, $\cup$, $\fun$, $\img$:
232: \begin{eqnarray*}
233: \fun(R^\star) & \iff & \mbox{$R^\star$ is an abstract solver}\\
234: \img(R^\star,P^\star) & = & \mbox{the image of} \; P^\star \; \mbox{under} \; R^\star\\
235: P^\star \cup Q^\star & = & \mbox{the standard union of subsets of $\C^\star$}\\
236: P^\star = Q^\star & \iff & \mbox{the standard equality of subsets of $\C^\star$}
237: \end{eqnarray*}
238:
239: \end{proposition}
240:
241: In practice the constraints (\ref{first-cnt})--(\ref{last-cnt}) are joined to (some of) the constraints
242: \begin{eqnarray}
243: &\dot{f_1}=F_1^\star, \ldots, \dot{f_n}=F_n^\star& \label{optional-cnt}
244: \end{eqnarray}
245: specifying the abstract solvers.
246: We build these latter $F_s^\star$'s using two data bases
247: that contain patterns of the individual solvers and the relation of logical equivalence on the set of properties of the processed data.
248:
249: A {\em pattern} of an individual solver is a collection of {\em rules} of the form ``pre-condition $\to$ post-condition''
250: that have as common formal parameters the processed data and the called solvers.
251: The pre- and post-condition are conjunctions of atomic formulas containing the formal parameters of the pattern.
252: The formal parameters corresponding to the data not modified by the solver can be marked as ``read-only''.
253:
254: The fact that some solver is called is expressed by the unary predicate symbol $\called$; the interpretation of other predicate symbols is arbitrary.
255: The pre- and post-conditions in the pattern of a solver $s$ are of the form $\called(s)\wedge C$ and the symbol $\called$ does not occur in the conjunction $C$.
256: Thus parallelism is not actually allowed.
257:
258: \def\rhs{{\tt rhs}}
259:
260: Let $\pi_1$, \ldots, $\pi_n$ be the patterns of the individual solvers with instantiated formal parameters.
261: The context properties are conjunctions $\called(s)\wedge C$,
262: ---where $s=1, \ldots, n$ and $C$ is a conjunction of the atomic formulas from $\pi_1$, \ldots, $\pi_n$,---
263: that are not equivalent to the false conjunction.
264: We assume that two equivalent conjunctions are the same object.
265:
266: The image of a context property $c^\star$ under the abstract solver $F_s^\star$ corresponing to a pattern $\pi_s$ is built as follows.
267: Let $c^\star = \called(s') \wedge C_{\tt ro} \wedge C_{\tt rw}$ such that
268: every conjunct in $C_{\tt rw}$ contains a value taken by some non read-only formal parameter of $\pi_s$ and
269: $C_{\tt ro}$ contains all the other conjuncts from $c^\star$ except $\called(s')$.
270:
271: If $s\ne s'$ then $\img\left( F_s^\star, \left\{ c^\star \right\} \right) = \left\{ c^\star \right\} $.
272: Otherwise $\img\left( F_s^\star, \left\{ c^\star \right\} \right)$ =
273: $\bigwedge \left\{ \left\{ C_{\tt ro} \right\} \right\} \cup \left\{ \rhs(c^\star_1, \pi_s) | c^\star_1 \; \mbox{is implied by} \; c^\star \right\}$
274: where each set of conjunctions is interpreted as the disjunction of its elements,
275: e.g. $\{a,b\}\wedge \{x,y\}=\{a \wedge x, a \wedge y, b \wedge x, b \wedge y\}$,
276: and $\rhs(c^\star_1, \pi_s)$ denotes the set of the post-conditions following a pre-condition $c^\star_1$ in the pattern $\pi_s$.
277: Finally, $c^\star_1$ ``is implied by'' $c^\star$ iff $c^\star_1 \wedge c^\star$ is equivalent to $c^\star$.
278:
279: The next section illustrates our approach by several examples.
280:
281: \section{Examples}
282: \label{examples}
283:
284: The examples in this section illustrate application of our approach to two important cooperation patterns: deterministic choice and loop.
285: Our ultimate goal (out of the scope of this paper) is to couple the analysis with the language for specification of composite solvers in the framework of the COCONUT project.
286: In order that the reader can feel our approach better, we provide in Appendix \ref{logicalc} the complete specification of the set constraints from Section \ref{cplex-ac}.
287:
288:
289: \subsection{The na\"\i{}ve solver from Section \ref{intro}}
290:
291: The patterns of the individual solvers from the example in Section \ref{intro} are as follows:
292: {
293: \small
294: \begin{eqnarray*}
295: &&{\tt cnvx?}( {\tt ro}(F); S_1, S_2 ) =
296: \{
297: \called(1) \wedge {\tt cnvx}(F) \to \called(S_1),
298: \called(1) \to \called(S_2)
299: \}\\
300: &&{\tt dscnt}( {\tt ro}(F), X; S ) =
301: \{
302: \called(2) \wedge {\tt stCnvx}(F) \to \called(S) \wedge {\tt min}(F, X),
303: \called(2) \to \called(S)
304: \}\\
305: &&{\tt glblSrch}( {\tt ro}(F), X; S ) =
306: \{
307: \called(3) \to \called(S) \wedge {\tt min}(F, X)
308: \}\\
309: &&{\tt done}() =
310: \{
311: \called(4) \to \called(4)
312: \}
313: \end{eqnarray*}
314: }
315: The symbols ${\tt cnvx}$, ${\tt stCnvx}$, ${\tt min}$ denote the properties ``is convex'', ``is strictly convex'', ``is the global minimizer in the positive orthant''.
316: The only non-trivial equivalence is ${\tt cnvx}(F)\wedge {\tt stCnvx}(F)\equiv {\tt stCnvx}(F)$.
317: The read-only parameters are marked ${\tt ro}$.
318:
319: The instantiated patterns are ${\tt cnvx?}( f; 2, 3 )$, ${\tt dscnt}( f, x; 4 )$, ${\tt glblSrch}( f, x; 4 )$, ${\tt done}()$.
320: The set of context properties is (we use the notation for disjunctions from Section \ref{infinite-calc}):
321: \{$\called(1)$, $\called(2)$, $\called(3)$, $\called(4)$\}
322: $\wedge$
323: \{${\tt cnvx}(f)$, ${\tt stCnvx}(f)$, ${\tt min}(f,x)$, ${\tt true}$\}
324: $\wedge$
325: \{${\tt min}(f,x)$, ${\tt true}$\}.
326: In practice these 24 context properties are numbered and the set constraints involve only their numbers.
327:
328: Of the specifications for $F_1^\star$, $F_2^\star$, $F_3^\star$, $F_4^\star$ generated by the procedure from Section \ref{infinite-calc}, we provide the first one:
329: {\small
330: \begin{eqnarray*}
331: &&\img( F_1^\star, \{ \called(1) \wedge {\tt cnvx}(f) \} ) = \{ \called(2) \wedge {\tt cnvx}(f)\}\\
332: &&\img( F_1^\star, \{ \called(1) \wedge {\tt stCnvx}(f) \} ) = \{ \called(2) \wedge {\tt stCnvx}(f)\}\\
333: &&\img( F_1^\star, \{ \called(1) \wedge {\tt min}(f,x) \wedge {\tt cnvx}(f) \} ) = \{ \called(2) \wedge {\tt min}(f,x) \wedge {\tt cnvx}(f) \}\\
334: &&\img( F_1^\star, \{ \called(1) \wedge {\tt min}(f,x) \wedge {\tt stCnvx}(f)\} ) = \{ \called(2) \wedge {\tt min}(f,x) \wedge {\tt stCnvx}(f) \}\\
335: &&\img( F_1^\star, \{ \called(1) \wedge {\tt min}(f,x) \} ) = \{ \called(2) \wedge {\tt min}(f,x) \wedge {\tt cnvx}(f), \called(3) \wedge {\tt min}(f,x) \}\\
336: &&\img( F_1^\star, \{ \called(1) \} ) = \{ \called(2) \wedge {\tt cnvx}(f), \called(3) \}
337: \end{eqnarray*}}
338: and $\img( F_1^\star, \{ c^\star \} ) = \{ c^\star \}$ for the other context properties $c^\star$.
339:
340: Solving the constraints (\ref{first-cnt})--(\ref{optional-cnt}) and $\dot{c_0}=\called(1)$,
341: we obtain the following approximation for the set of feasible contexts:
342: $\dot{p}$ = \{$\called(1)$, $\called(2)$ $\wedge$ ${\tt cnvx}(f)$, $\called(3)$, $\called(4)$, $\called(4)$ $\wedge$ ${\tt min}(f,x)$\}.
343: Since this $\dot{p}$ contains $\called(4)$, we are not sure that our composite solver always finds the minimizer of $f(x)$ subject to $x\ge 0$.
344:
345: The question ``When does our composite finds the minimizer?'' is translated into the constraints (\ref{first-cnt})--(\ref{optional-cnt}) and
346: the constraints that
347: say that we examine what happens after the convexity test is called ($\called(1)$ ``is implied by'' $\dot{c_0}$)
348: and
349: forbid the uncertain situation after termination ($\called(4) \not \in \dot{p}$).
350: Solving these constraints for the initial context $\dot{c_0}$, we obtain the following solutions:
351: $\dot{c_0}=\called(1) \wedge {\tt stCnvx}(f)$,
352: $\dot{c_0}=\called(1) \wedge {\tt min}(f,x) \wedge {\tt stCnvx}(f)$.
353: This means that the objective has to be strictly convex in order that our solver can find its global minimizer.
354:
355:
356: \subsection{The Simplex method and Hull Consistency}
357: \label{cplex-ac}
358:
359: Consider a composite solver that makes cooperate the Simplex method from linear programming and the HC algorithm \cite{opt:benhamou-goualard-granvilliers-iclp-99}
360: (a similar composite solver is described e.g. in \cite{coop:beringer-backer-lp-elsevier-95}).
361: The context specifies some linear, interval and bound constraints, denoted $\ell$, $i$ and, respectively $b$.
362: The Simplex method updates $b$ by bounding the solution set $\sol(\ell \cup b)$ and calls the HC algorithm,
363: which in its turn updates $b$ by bounding the solution set $\sol(i\cup b)$ and calls the Simplex method, and so on until stabilization of $b$.
364: The important quality of this strategy is that bounds the solution set $\sol(l\cup i\cup b)$ more sharply than the HC algorithm.
365:
366: The patterns of the individual solvers are as follows:
367: {\small
368: \begin{eqnarray*}
369: &&{\tt cplex}( {\tt ro}(L), B; S ) =
370: \left\{
371: \called(1) \to \called(S) \wedge {\tt ok}(L)
372: \right\}\\
373: &&{\tt hc}( {\tt ro}(I), B; S ) =
374: \left\{
375: \called(2) \to \called(S),
376: \called(2) \wedge {\tt tree}(I) \to \called(S) \wedge {\tt ok}(I)
377: \right\}\\
378: &&{\tt same?}( {\tt ro}(B); S_1, S_2 ) =
379: \left\{
380: \called(3) \to \called(S_1),
381: \called(3) \to \called(S_2)
382: \right\}\\
383: &&{\tt done}() =
384: \left\{
385: \called(4) \to \called(4)
386: \right\}
387: \end{eqnarray*}}
388: The symbols ${\tt ok}$, ${\tt tree}$ denote the properties ``has the solution set that we can bound sharply'', ``has an acyclic constraint graph''.
389: All the equivalences are trivial.
390:
391: The instantiated patterns are ${\tt cplex}( \ell, b; 2 )$, ${\tt hc}( i, b; 3 )$, ${\tt same?}( b; 1, 4 )$, ${\tt done}()$.
392: There are 32 context properties built as follows:
393: \{$\called(1)$, $\called(2)$, $\called(3)$, $\called(4)$\}
394: $\wedge$
395: \{${\tt ok}(\ell)$, ${\tt ok}(i)$, ${\tt tree}(i)$, ${\tt true}$\}
396: $\wedge$
397: \{${\tt ok}(i)$, ${\tt tree}(i)$, ${\tt true}$\}
398: $\wedge$
399: \{${\tt tree}(i)$, ${\tt true}$\}.
400:
401: The specifications for the abstract solvers $F_1^\star$, $F_2^\star$, $F_3^\star$, $F_4^\star$ generated by the procedure from Section \ref{infinite-calc}
402: are provided in Appendix \ref{logicalc}.
403:
404: Solving the constraints (\ref{first-cnt})--(\ref{optional-cnt}) and $\dot{c_0}=\called(1)$,
405: we obtain the following approximation for the set of feasible contexts:
406: $\dot{p}=\{ \called(1), \called(1) \wedge {\tt ok}(\ell), \called(2) \wedge {\tt ok}(\ell), \called(3) \wedge {\tt ok}(\ell), \called(4) \wedge {\tt ok}(\ell)\}$.
407: Since this $\dot{p}$ contains only $\called(4) \wedge {\tt ok}(\ell)$,
408: the solution set of the linear constraints is {\em always} bounded sharply after termination of the composite solver.
409:
410: We can figure out when the composite solver bounds the solution set $\sol(\ell\cup i\cup b)$ sharply, solving the constraints (\ref{first-cnt})--(\ref{optional-cnt}) and
411: the constraints that say
412: that we examine what happens after the Simplex method is called ($\called(1)$ ``is implied by'' $\dot{c_0}$) and
413: that the solution set is bounded sharply after termination
414: ($\dot{c}_\infty \in \dot{p}$, $\called(4) \wedge {\tt ok}(i) \wedge {\tt ok}(\ell)$ ``is implied by'' $\dot{c}_\infty$).
415: These constraints have 6 solutions.
416: The first two assign $\called(4)$ $\wedge$ ${\tt ok}(\ell)$ $\wedge$ ${\tt ok}(i)$ to $\dot{c}_\infty$ and
417: either $\called(1)$ $\wedge$ ${\tt ok}(i)$, or $\called(1)$ $\wedge$ ${\tt ok}(i) \wedge {\tt ok}(\ell)$ to $\dot{c_0}$.
418: The other four assign $\called(4)$ $\wedge$ ${\tt ok}(\ell)$ $\wedge$ ${\tt tree}(i)$ $\wedge$ ${\tt ok}(i)$ to $\dot{c}_\infty$ and
419: one of the 4 context properties that ``imply'' $\called(1)$ $\wedge$ ${\tt tree}(i)$ to $\dot{c_0}$.
420: This means that,
421: the composite solver bounds the solution set $\sol(\ell\cup i\cup b)$ sharply, if the interval constraints $i$ have an acyclic constraint graph.
422:
423: \section{Conclusion}
424: \label{conclusion}
425:
426: We have presented a formalism for automatic analysis of composite solvers.
427: This formalism provides
428: a structure for expressing properties of the data store (context properties),
429: a structure for specifying the behaviour of solvers (abstract solvers),
430: a method for approximation of composite solvers by set constraints
431: that can be efficiently solved by conventional set constraint solvers like \cite{Gervet97,petrov-yakhno-lncs-1755-99}.
432: The ultimate goal (out of the scope of this paper) is to couple our analysis with the language for specification of composite solvers in the framework of the COCONUT project.
433:
434: \paragraph*{Acknowledgements}
435: We thank Lucas Bordeaux from l'Institut de Recherche en Informatique de Nantes for the comments on quantified constraints.
436:
437: \paragraph*{Disclaimer}
438: No solver has been damaged during the preparation of this document.
439:
440: \bibliographystyle{abbrv}
441:
442: \begin{thebibliography}{10}
443:
444: \bibitem{opt:benhamou-goualard-granvilliers-iclp-99}
445: F.~Benhamou, F.~Goualard, L.~Granvilliers, and J.-F. Puget.
446: \newblock Revising hull and box consistency.
447: \newblock In {\em Proc. 16th Int. Conf. Logic Programming}, pages 230--244. The
448: MIT Press, 1999.
449:
450: \bibitem{coop:beringer-backer-lp-elsevier-95}
451: H.~Beringer and B.~{De Backer}.
452: \newblock Combinatorial problem solving in constraint logic programming with
453: cooperating solvers.
454: \newblock In {\em Logic Programming: formal methods and practical
455: applications}. Elsevier Science Publishers, 1994.
456:
457: \bibitem{Gervet97}
458: C.~Gervet.
459: \newblock Interval propagation to reason about sets: definition and
460: implementation of a practical language.
461: \newblock In {\em Constraints}, volume~3, pages 191--244. Kluwer Academic
462: Publishers, 1997.
463:
464: \bibitem{coop:granvilliers-monfroy-benhamou-issac-01}
465: L.~Granvilliers, E.~Monfroy, and F.~Benhamou.
466: \newblock Symbolic-interval cooperation in constraint programming.
467: \newblock In {\em Proc. ISSAC 2001}. ACM, 2001.
468:
469: \bibitem{intervals:hansen-reliable-comp-97}
470: E.~R. Hansen.
471: \newblock Sharpness in interval computations.
472: \newblock {\em Reliable Computing}, 3(1):17--19, 1997.
473:
474: \bibitem{coop:hickey-lncs-00}
475: P.~Hickey.
476: \newblock {CLIP}: a {CLP}({I}ntervals) dialect for metalevel constraint
477: solving.
478: \newblock In {\em Proc. Int. Workshop on Practical Aspects of Declarative
479: Languages}, volume 1753 of {\em Lecture Notes in Computer Science}, pages
480: 200--214. Springer, 2000.
481:
482: \bibitem{ECLIPSE00}
483: International Computers Limited \& Imperial College of London.
484: \newblock {\em ECL$^i$PS$^e$ User Manual (release 5.3)}, 1996--2000.
485:
486: \bibitem{coop:jaffar-michaylov-stuckey-yap-acm-92}
487: J.~Jaffar, S.~Michaylov, P.~Stuckey, and R.~Yap.
488: \newblock The {CLP}({$\Re$}) language and system.
489: \newblock {\em ACM Trans. on Progamming Languages and Systems}, 14(3):339--395,
490: July 1992.
491:
492: \bibitem{coop:marti-rueher-jait-95}
493: P.~Marti and M.~Rueher.
494: \newblock Distributed cooperating constraint solving systems.
495: \newblock {\em International Journal of Artificial Intelligence Tools},
496: 4(1\&2):95--113, 1995.
497:
498: \bibitem{coop:monfroy-frocos-00}
499: E.~Monfroy.
500: \newblock The constraint solver collaboration language of {BALI}.
501: \newblock In D.~M. Gabbay and M.~{de Rijke}, editors, {\em Frontiers of
502: Combining Systems 2}. Research Studies Press / Wiley, 2000.
503:
504: \bibitem{MOZART}
505: {\sc Mozart consortium}.
506: \newblock {\em The {Mozart} programming system}, 1999.
507:
508: \bibitem{PROLOGIV}
509: {PROLOGIA}.
510: \newblock {\em Prolog {IV}: constraints inside (reference manual)}, 1996.
511:
512: \bibitem{vH-numerica}
513: P.~{Van Hentenryck}, L.~Michel, and Y.~Deville.
514: \newblock {\em Numerica: a Modelling Language for Global Optimization}.
515: \newblock The MIT Press, Cambridge, MA, 1997.
516:
517: \bibitem{petrov-yakhno-lncs-1755-99}
518: T.~Yakhno and E.~Petrov.
519: \newblock Extensional set library for {ECL$^i$PS$^e$}.
520: \newblock In {\em Proc. Ershov Memorial Conference 1999}, volume 1755 of {\em
521: Lecture Notes in Computer Science}, pages 434--444. Springer, 1999.
522:
523: \end{thebibliography}
524:
525: \appendix
526:
527: \section{Specification of the example from Section \ref{cplex-ac}}
528: \label{logicalc}
529:
530: The constraints from the sharpness example are provided in Fig. \ref{logicalc-spec} in the LogiCalc language \cite{petrov-yakhno-lncs-1755-99}.
531: We recall its syntax/semantics.
532: The LogiCalc language allows the user to specify constraints on integer numbers, tuples and finite sets.
533: Tuples of sets, sets of tuples, sets of sets, etc. are allowed.
534: The constraints are specified in terms of set inclusion ${\tt subset}$, membership ${\tt in}$, equality ${\tt =}$, and inequality ${\tt <=}$.
535: The left and right hand sides of the constraints are expressions built from variables, arithmetic and set operations, and specifications of finite set.
536:
537: Finite sets are specified by either enumeration of the elements, or by their common property.
538: For example,
539: {\small
540: \begin{verbatim}
541: x subset { 2, 3, 5, 7 };
542: y = { i * j | i in x; j in x; i + 1 <= j };
543: y = { 6, 10, 15 }
544: \end{verbatim}}
545: specify the set $y=\{ i\cdot j | i\in x, j\in x, i < j \}=\{6,10,15\}$ and the set $x=\{2,3,5\}$ of their prime factors.
546: Notice implicit existential quantification of the variables $i$ and $j$ that do not occur outside the specification of $y$.
547: Notice that the equation $y=\{ i\cdot j | \ldots \}$ is, in fact, a constraint on $x$ and $y$.
548:
549: \begin{figure}[ht]
550: {\small
551: \begin{verbatim}
552: % Notation for the data properties: %
553: treeI = 0; okL = 1; okI = 2; treeIokL = 3;
554: okIokL = 4; true = 5; treeIokI = 6; treeIokLokI = 7;
555: Cdata = { treeI, okL, okI, treeIokL,
556: okIokL, true, treeIokI, treeIokLokI };
557: % cplex %
558: F1star = {
559: ((1, treeI), (2, treeIokL)),
560: ((1, okL), (2, okL)),
561: ((1, okI), (2, okIokL)),
562: ((1, treeIokL), (2, treeIokL)),
563: ((1, okIokL), (2, okIokL)),
564: ((1, true), (2, okL)),
565: ((1, treeIokI), (2, treeIokLokI))
566: ((1, treeIokLokI), (2, treeIokLokI)) } \/
567: { ((i1, z1), (i1, z1)) | i1 in { 2, 3, 4 }, z1 in Cdata };
568: % hc %
569: F2star = {
570: ((2, treeI), (3, treeIokI)),
571: ((2, okL), (3, okL)),
572: ((2, okI), (3, okI)),
573: ((2, treeIokL), (3, treeIokLokI)),
574: ((2, okIokL), (3, okIokL)),
575: ((2, true), (3, true)),
576: ((2, treeIokI), (3, treeIokI))
577: ((2, treeIokLokI), (3, treeIokLokI)) } \/
578: { ((i2, z2), (i2, z2)) | i2 in { 1, 3, 4 }, z2 in Cdata };
579: % same? %
580: F3star = { ((3, z3), (i3, z3)) | z3 in Cdata, i3 in { 1, 4 } };
581: % done %
582: F4star = { ((4, z4), (4, z4)) | z4 in Cdata };
583: % constraints (4)--(5): %
584: img1 = { c11 | (c1, c11) in F1star; c1 in p };
585: img2 = { c22 | (c2, c22) in F2star; c2 in p };
586: img3 = { c33 | (c3, c33) in F3star; c3 in p };
587: img4 = { c44 | (c4, c44) in F4star; c4 in p };
588: p = { c0 } \/ img1 \/ img2 \/ img3 \/ img4;
589: \end{verbatim}
590: }
591: \caption{
592: Specification of the sharpness example in the LogiCalc language;
593: ${\tt\{\}}$ denotes the empty set,
594: ${\tt \symbol{'134}/}$ denotes set union,
595: ${\tt F1star}$ specifies the abstract CPLEX,
596: ${\tt F2star}$ specifies the abstract arc consistency,
597: ${\tt c0}$ denotes the initial context that we search for,
598: ${\tt img1}$, ${\tt img2}$ denote the images of the set of feasible contexts under the abstract CPLEX and arc consistency.}
599: \label{logicalc-spec}
600: \end{figure}
601:
602: \end{document}
603: