1: \NeedsTeXFormat{LaTeX2e}
2: \documentclass[runningheads]{llncs}
3:
4: \usepackage{amssymb}
5: \def\bbbn{{\rm I\!N}}
6: \def\Win{{\it W_{in}}}
7: \def\Wout{{\it W_{out}}}
8: \def\var{{\mbox{var}}}
9: \def\cons{{\mbox{cons}}}
10: \def\step{{\mbox{step}}}
11: \def\root{{\mbox{root}}}
12: \def\da{\hspace{-1.5mm}\downarrow}
13: \def\ua{\hspace{-1.5mm}\uparrow}
14:
15: \begin{document}
16: \setcounter{page}{17}
17: \title{Value withdrawal explanations: a theoretical tool for programming environments}
18: \titlerunning{Value withdrawal explanations: a theoretical tool\ldots{}}
19: \author{Willy Lesaint}
20: \authorrunning{W. Lesaint}
21: \institute{Laboratoire d'Informatique Fondamentale d'Orl\'{e}ans \\
22: rue L\'{e}onard de Vinci -- BP 6759 --
23: F-45067 Orl\'{e}ans Cedex 2 -- France \\
24: \email{Willy.Lesaint@lifo.univ-orleans.fr}}
25:
26: \maketitle
27:
28: \addtocounter{footnote}{1}
29: \footnotetext{In Alexandre Tessier (Ed), proceedings of the 12th International Workshop on Logic Programming Environments (WLPE 2002), July 2002, Copenhagen, Denmark.\\Proceedings of WLPE 2002: \texttt{http://xxx.lanl.gov/html/cs/0207052} (CoRR)}
30:
31: \begin{abstract}
32: Constraint logic programming combines declarativity and efficiency
33: thanks to constraint solvers implemented for specific domains.
34: Value withdrawal explanations have been efficiently used in several
35: constraints programming environments but there does not exist any
36: formalization of them. This paper is an attempt to fill this lack.
37: Furthermore, we hope that this theoretical tool could help to validate
38: some programming environments. A value withdrawal explanation is a
39: tree describing the withdrawal of a value during a domain reduction by
40: local consistency notions and labeling. Domain reduction is formalized
41: by a search tree using two kinds of operators: operators for local
42: consistency notions and operators for labeling. These operators are
43: defined by sets of rules. Proof trees are built with respect to these
44: rules. For each removed value, there exists such a proof tree which is
45: the withdrawal explanation of this value.
46: \end{abstract}
47:
48: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
49: \section{Introduction}
50: \label{Sect:I}
51: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
52:
53: Constraint logic programming is one of the most important computing
54: paradigm of the last years.
55: It combines declarativity and efficiency thanks to constraint solvers
56: implemented for specific domains.
57: Consequently the needs in programming environments is growing.
58: But logic programming environments are not always sufficient
59: to deal with the constraint side of constraint logic programming.
60: Value withdrawal explanations have been efficiently used in several
61: constraints programming environments but there does not exist any
62: formalization of them. This paper is an attempt to fill this lack.
63: This work is supported by the french RNTL\footnote{R\'eseau National
64: des Technologies Logicielles} project OADymPPaC\footnote{Outils pour
65: l'Analyse Dynamique et la mise au Point de Programmes avec
66: Contraintes {\tt http://contraintes.inria.fr/OADymPPaC/}} which aim is
67: to provide constraint programming environments.
68:
69: A value withdrawal explanation is a tree describing the withdrawal of
70: a value during a domain reduction.
71: This description is done in the framework of domain reduction of
72: finite domains by notions of local consistency and labeling. A first
73: work \cite{FerLesTes-wflp-02} dealt with explanations in the
74: framework of domain reduction by local consistency notions only.
75: A value withdrawal explanation contains the whole information about a
76: removal and may therefore be a useful tool for programming environments.
77: Indeed it allows to perform:
78: \begin{itemize}
79: \item failure analysis: a failure explanation being a set of value
80: withdrawal explanations;
81: \item constraint retraction: explanations provides the values which
82: have been withdrawn directly or indirectly by the constraint
83: and then allow to easily repair the domains;
84: \item debugging: an explanation being a kind of declarative trace of
85: a value withdrawal, it can be used to find an error from a
86: symptom.
87: \end{itemize}
88: The first and second item have been implemented in the \texttt{PaLM}
89: system \cite{BarJus-trics-00}.
90: \texttt{PaLM} is based on the constraint solver \textsc{choco}
91: \cite{Lab-trics-00} where labeling is replaced by the use of
92: explanations.
93: Note that the constraint retraction algorithm of \texttt{PaLM} has
94: been proved correct thanks to our definition of explanations, and more
95: generally a large family of constraint retraction algorithms are also
96: included in this framework.
97:
98: The main motivation of this work is not only to provide a common model
99: for the partners of the OADymPPaC project but also to use explanations
100: for the debugging of constraints programs.
101: Nevertheless, the aim of this paper is not to describe the
102: applications of value withdrawal explanations but to formally define
103: this notion of explanation.
104:
105: The definition of a Constraint Satisfaction Problem is given in the
106: preliminary section.
107: In third and fourth sections a theoretical framework for the
108: computation of solutions is described in sections \ref{Sect:DR} and
109: \ref{Sect:ADR}.
110: A computation is viewed as a search tree where each branch is an
111: iteration of operators.
112: Finally, explanations are presented in the last section thanks to the
113: definition of rules associated to these operators.
114:
115:
116: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
117: \section{Preliminaries}
118: \label{Sect:P}
119: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
120:
121: Following \cite{Tsang-book-93}, a \emph{Constraint Satisfaction
122: Problem} (CSP) is made of two parts: a syntactic part and a semantic
123: part.
124: The syntactic part is a finite set $V$ of variables, a finite set $C$
125: of constraints and a function $\var : C \rightarrow {\cal P}(V)$,
126: which associates a set related variables to each constraint.
127: Indeed, a constraint may involve only a subset of $V$.
128:
129: For the semantic part, we need to introduce some preliminary
130: concepts. We consider various \emph{families} $f=(f_i)_{i \in I}$.
131: Such a family is referred to by the \emph{function} $i \mapsto f_i$ or
132: by the \emph{set} $\{(i,f_i) \mid i \in I \}$.
133:
134: Each variable is associated to a set of possible values.
135: Therefore, we consider a family $(D_x)_{x \in V}$ where each $D_x$ is
136: a \emph{finite non empty set}.
137:
138: We define the \emph{domain} by
139: $\mathbb{D} = \bigcup_{x \in V} (\{x\} \times D_x)$.
140: This domain allows simple and uniform definitions of (local
141: consistency) operators on a power-set.
142: For domain reduction, we consider subsets $d$ of $\mathbb{D}$.
143: Such a subset is called an \emph{environment}.
144: We denote by $d|_W$ the restriction of a set $d \subseteq \mathbb{D}$
145: to a set of variables $W \subseteq V$, that is,
146: $d|_W = \{ (x,e) \in d \mid x \in W \}$.
147: Any $d \subseteq \mathbb{D}$ is actually a family $(d_x)_{x \in V}$
148: with $d_x \subseteq D_x$: for $x \in V$, we define
149: $d_x=\{e \in D_x \mid (x,e) \in d\}$ and call it the
150: \emph{environment of $x$}.
151:
152: Constraints are defined by their set of allowed tuples.
153: A \emph{tuple} $t$ on $W \subseteq V$ is a particular environment such
154: that each variable of $W$ appears only once:
155: $t \subseteq \mathbb{D}|_W$ and
156: $\forall x \in W, \exists e \in D_x, t|_{\{x\}}=\{(x,e)\}$.
157: For each $c \in C$, $T_c$ is a set of tuples on $\var(c)$, called the
158: solutions of $c$.
159:
160: We can now formally define a CSP.
161:
162: \begin{definition}
163: A \emph{Constraint Satisfaction Problem} (CSP) is defined by:
164: \begin{itemize}
165: \item a finite set $V$ of variables;
166: \item a finite set $C$ of constraints;
167: \item a function $\var : C \rightarrow {\cal P}(V)$;
168: \item the family $(D_x)_{x \in V}$ (the domains);
169: \item a family $(T_c)_{c \in C}$ (the constraints semantics).
170: \end{itemize}
171: \end{definition}
172:
173: Note that a tuple $t \in T_c$ is equivalent to the family
174: $(e_x)_{x \in \var(c)}$ and that $t$ is identified to
175: $\{(x,e_x) \mid x \in \var(c)\}$.
176:
177: A user is interested in particular tuples (on $V$) which associate a
178: value to each variable, such that all the constraints are satisfied.
179:
180: \begin{definition}
181: A tuple $t$ on $V$ is a \emph{solution} of the CSP if
182: $\forall c \in C, t|_{\var(c)} \in T_c$.
183: \end{definition}
184:
185: \begin{example}{Conference problem}
186:
187: Mike, Peter and Alan wants to give a talk on their work to each other
188: during three half-days. Peter knows Alan's work and vice versa. There
189: are four talks (and so four variables): Mike to Peter (MP), Peter to
190: Mike (PM), Mike to Alan (MA) and Alan to Mike (AM). Note that Mike can
191: not listen to Alan and Peter simultaneously (AM $\neq$ PM). Mike wants
192: to know the works of Peter and Alan before talking (MA $>$ AM, MA $>$
193: PM, MP $>$ AM, MP $>$ PM).
194:
195: This can be written in \textsc{GNU-Prolog} \cite{DiaCod-acm-00} (with
196: a labeling on PM) by:
197: \begin{verbatim}
198: conf(AM,MP,PM,MA):-
199: fd_domain([MP,PM,MA,AM],1,3),
200: MA #> AM,
201: MA #> PM,
202: MP #> AM,
203: MP #> PM,
204: AM #\= PM,
205: fd_labeling(PM).
206: \end{verbatim}
207: The values $1,2,3$ corresponds to the first, second and third
208: half-days. Note that the labeling on $PM$ is sufficient to obtain the
209: solutions. Without this labeling, the solver provides reduced domains
210: only (no solution).
211:
212: This example will be continued all along the paper.\hfill$\Box$
213: \end{example}
214:
215: The aim of a solver is to provide one (or more) solution. In order to
216: obtain them, two methods are interleaved: domain reduction thanks to
217: local consistency notions and labeling.
218: The first one is correct with respect to the solutions, that is it
219: only removes values which cannot belong to any solution, whereas the
220: second one is used to restrict the search space.
221:
222: Note that to do a labeling amounts to cut a problem in several
223: sub-problems.
224:
225: In the next section, we do not consider the whole labeling (that is
226: the passage from a problem to a set of sub-problems) but only the
227: passage from a problem to one of its sub-problems. The whole labeling
228: will be consider in section~\ref{Sect:ADR} with the well-known notion
229: of search tree.
230:
231:
232: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
233: \section{Domain reduction mechanism}
234: \label{Sect:DR}
235: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
236:
237: In practice, operators are associated with the constraints and are
238: applied with respect to a propagation queue. This method is
239: interleaved with some restriction (due to labeling).
240: In this section, this computation of a reduced environment is
241: formalized thanks to a chaotic iteration of operators.
242: The reduction operators can be of two types: operators associated with
243: a constraint and a notion of local consistency, and operators
244: associated with a restriction.
245: The resulting environment is described in terms of closure ensuring
246: confluence.
247:
248: Domain reduction with respect to notions of consistency can be
249: expressed in terms of operators.
250: Such an operator computes a set of consistent values for a set of
251: variables $\Wout$ according to the environments of another set of
252: variables $\Win$.
253:
254: \begin{definition}
255: A \emph{local consistency operator} of type $(\Win,\Wout)$, with
256: $\Win, \Wout$ $\subseteq V$ is a monotonic function
257: $f: {\cal P}(\mathbb{D}) \rightarrow {\cal P}(\mathbb{D})$ such
258: that: $\forall d \subseteq \mathbb{D}$,
259: \begin{itemize}
260: \item $f(d)|_{V \setminus \Wout} = \mathbb{D} |_{V \setminus \Wout}$,
261: \item $f(d)=f(d|_{\Win})$
262: \end{itemize}
263: \end{definition}
264:
265: Note that the first item ensures that the operator is only concerned
266: by the variables $\Wout$. The second one ensures that this result only
267: depends on the variable $\Win$.
268:
269: These operators are associated with constraints of the CSP.
270: So each operator must not remove solutions of its associated
271: constraint (and of course of the CSP).
272: These notions of correction are detailed
273: in~\cite{FerLesTes-RR2001-05}.
274:
275: \begin{example}
276: In \textsc{GNU-Prolog}, two local consistency operators are associated
277: to the constraint \verb+MA #> PM+: the operator which reduce the
278: domain of MA with respect to PM and the one which reduce the
279: domain of PM with respect to MA.\hfill$\Box$
280: \end{example}
281:
282: From now on, we denote by $L$ a set of local consistency operators
283: (the set of local consistency operators associated with the
284: constraints of the CSP).
285:
286: Domain reduction by notions of consistency alone is not always
287: sufficient.
288: The resulting environment is an approximation of the solutions (that
289: is all the solutions are included in this environment).
290: This environment must be restricted (for example by the choice of a
291: value for a variable).
292: Of course, such a restriction (formalized by the application of a
293: restriction operator) does not have the properties of correctness of a
294: local consistency operator: the application of such an operator may
295: remove solutions.
296: But, in the next section, these operators will be considered as a set
297: (corresponding to the whole labeling on a variable).
298: Intuitively, if we consider a labeling search tree, this section only
299: deals with only one branch of this tree.
300:
301: In the same way local consistency operators have been defined,
302: restriction operators are now introduced.
303:
304: \begin{definition}
305: A \emph{restriction operator} on $x \in V$ is a constant function
306: $f: {\cal P}(\mathbb{D}) \rightarrow {\cal P}(\mathbb{D})$ such
307: that: $\forall d \subseteq \mathbb{D}, f(d)|_{V \setminus \{x\}} =
308: \mathbb{D} |_{V \setminus \{x\}}$.
309: \end{definition}
310:
311: \begin{example}
312: The function $f$ such that $\forall d \in \mathbb{D}, f(d) =
313: \mathbb{D}|_{V \setminus \{PM\}} \cup \{ ($PM$, 1) \}$ is a restriction
314: operator.\hfill$\Box$
315: \end{example}
316:
317: From now on we denote by $R$ a set of restriction operators.
318:
319: These two kind of operators are successively applied to the
320: environment.
321: The environment is replaced by its intersection with the result of the
322: application of the operator.
323: We denote by $F$ the set of operators $L \cup R$.
324:
325: \begin{definition}
326: The \emph{reduction operator} associated with the operator $f \in F$
327: is the monotonic and contracting function $d \mapsto d \cap f(d)$.
328: \end{definition}
329:
330: A common fix-point of the reduction operators associated with $F$
331: starting from an environment $d$ is an environment $d' \subseteq d$
332: such that $\forall f \in F, d'=d' \cap f(d')$, that is
333: $\forall f \in F, d' \subseteq f(d')$.
334: The greatest common fix-point is this greatest environment $d$.
335: To be more precise:
336:
337: \begin{definition}
338: The \emph{downward closure} of $d$ by $F$ is
339: $max \{d' \subseteq \mathbb{D} \mid d' \subseteq d \wedge \forall f
340: \in F, d' \subseteq f(d') \}$ and is denoted by
341: $CL \downarrow (d,F)$.
342: \end{definition}
343:
344: Note that $CL \downarrow (d, \emptyset) = d$ and
345: $CL \downarrow (d,F) \subseteq CL \downarrow (d,F')$ if
346: $F' \subseteq F$.
347:
348: In practice, the order of application of these operators is determined
349: by a propagation queue. It is implemented to ensures to never forget
350: any operator and to always reach the closure $CL \downarrow (d, F)$.
351: From a theoretical point of view, this closure can also be computed by
352: \emph{chaotic iterations} introduced for this aim in
353: \cite{FagFowSol-iclp-95}.
354: The following definition is taken from Apt \cite{Apt-tcs-99}.
355:
356: \begin{definition}
357: A \emph{run} is an \emph{infinite} sequence of operators of $F$, that
358: is, a run associates with each $i \in \bbbn$ $(i \ge 1)$ an element
359: of $F$ denoted by $f^i$. A run is \emph{fair} if each $f \in F$
360: appears in it infinitely often, that is,
361: $\forall f \in F, \{i \mid f = f^i \}$ is infinite.
362:
363: The \emph{iteration} of the set of operators $F$ from the
364: environment $d \subseteq \mathbb{D}$ with respect to an infinite
365: sequence of operators of $F$: $f^1, f^2, \dots$ is the infinite
366: sequence $d^0, d^1, d^2, \dots$ inductively defined by:
367: \begin{enumerate}
368: \item $d^0 = d$;
369: \item for each $i \in \bbbn$, $d^{i+1} = d^i \cap f^{i+1}(d^i)$.
370: \end{enumerate}
371: Its \emph{limit} is $\cap_{i \in \bbbn} d^i$.
372:
373: A \emph{chaotic iteration} is an iteration with respect to a
374: sequence of operators of $F$ (with respect to $F$ in short) where
375: each $f \in F$ appears infinitely often.
376: \end{definition}
377:
378: Note that an iteration may start from a domain $d$ which can be
379: different from $\mathbb{D}$.
380: This is more general and convenient for a lot of applications (dynamic
381: aspects of constraint programming for example).
382:
383: The next well-known result of confluence
384: \cite{CouCou-saipl-77,FagFowSol-iclp-95} ensures that any chaotic
385: iteration reaches the closure.
386: Note that, since $\subseteq$ is a well-founded ordering
387: (i.e. $\mathbb{D}$ is a finite set), every iteration from
388: $d \subseteq \mathbb{D}$ is stationary, that is,
389: $\exists i \in \bbbn, \forall j \ge i, d^j=d^i$.
390:
391: \begin{lemma}\label{lemma:chaotic iteration}
392: The limit $d^F$ of every chaotic iteration of a set of operators $F$
393: from $d \subseteq \mathbb{D}$ is the \emph{downward closure} of $d$
394: by $F$.
395: \end{lemma}
396:
397: \begin{proof}
398: Let $d^0, d^1, d^2, \dots$ be a chaotic iteration of $F$ from $d$
399: with respect to $f^1, f^2, \ldots$
400:
401: [$CL \downarrow (d,F) \subseteq d^F$]
402: For each $i$, $CL \downarrow (d,F) \subseteq d^i$, by induction:
403: $CL \downarrow (d,F) \subseteq d^0 = d$.
404: Assume $CL \downarrow (d,F) \subseteq d^i$,
405: $CL \downarrow (d,F) \subseteq f^{i+1} (CL \downarrow (d,F))
406: \subseteq f^{i+1}(d^i)$ by monotonicity. Thus,
407: $CL \downarrow (d,F) \subseteq d^i \cap f^{i+1}(d^i) = d^{i+1}$.
408:
409: [$d^F \subseteq CL \downarrow (d,F)$]
410: There exists $k \in \bbbn$ such that $d^F=d^k$ because $\subseteq$
411: is a well-founded ordering. The iteration is chaotic, hence $d^k$ is
412: a common fix-point of the set of operators associated with $F$, thus
413: $d^k \subseteq CL \downarrow (d,F)$ (the greatest common fix-point).
414: \end{proof}
415:
416: In order to obtain a closure, it is not necessary to have a chaotic
417: iteration.
418: Indeed, since restriction operators are constant functions, they can
419: be apply only once.
420:
421: \begin{lemma}
422: $d^{L \cup R} = CL \downarrow ( CL \downarrow (d, R), L)$
423: \end{lemma}
424:
425: \begin{proof}
426: $d^{L \cup R} = CL \downarrow (d, L \cup R)$ by
427: lemma~\ref{lemma:chaotic iteration} and
428: $CL \downarrow (d, L \cup R) = CL \downarrow ( CL \downarrow (d, R),
429: L)$ because operators of $R$ are constant functions.
430: \end{proof}
431:
432: As said above, we have considered in this section a computation in a
433: single branch of a labeling search tree.
434: This formalization is extended in the next section in order to take
435: the whole search tree into account.
436:
437:
438: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
439: \section{Search tree}
440: \label{Sect:ADR}
441: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
442:
443: A labeling on a variable can be viewed as the passage from a problem
444: to a set of problems.
445: The previous section has treated the passage from this problem to one
446: of its sub-problems thanks to a restriction operator. In order to
447: consider the whole set of possible values for the labeling on a
448: variable, restriction operators on a same variable must be grouped
449: together.
450: The union of the environments of the variable (the variable concerned
451: by the labeling) of each sub-problem obtained by the application of
452: each of these operators must be a partition of the environment of the
453: variable in the initial problem.
454:
455: \begin{definition}
456: A set $\{ d_i \mid 1 \le i \le n\}$ is a
457: \emph{partition of $d$ on $x$} if:
458: \begin{itemize}
459: \item $\forall i, 1 \le i \le n, ~d|_{V \setminus \{x\}} \subseteq
460: d_i|_{V \setminus \{x\}}$,
461: \item $d|_{\{x\}} \subseteq \cup_{1 \le i \le n} d_i|_{\{x\}}$,
462: \item $\forall i,j, 1 \le i \le n, 1 \leq j \leq n, i \neq j,
463: d_i|_{\{x\}} \cap d_j|_{\{x\}} = \emptyset$.
464: \end{itemize}
465: \end{definition}
466:
467: In practice, environment reductions by local consistency operators and
468: labeling are interleaved to be the most efficient.
469:
470: A labeling on $x \in V$ can be a complete enumeration (each
471: environment of the partition is reduced to a singleton) or a
472: splitting.
473: Note that the partitions always verify:
474: $\forall i, 1 \leq i \leq n, d_i|_{\{x\}} \neq \emptyset$.
475:
476: \begin{example}
477: $\{\mathbb{D}|_{V \setminus \{PM\}} \cup \{($PM$,1)\}, \mathbb{D}|_{V
478: \setminus \{PM\}} \cup \{($PM$,2)\}, \mathbb{D}|_{V \setminus \{PM\}}
479: \cup \{($PM$,3)\}$ is a partition of $\mathbb{D}$. \hfill$\Box$
480:
481: \end{example}
482:
483: Next lemma ensures that no solution is lost during a labeling step
484: (each solution will remains in exactly one branch of the search tree
485: defined later).
486:
487: \begin{lemma}
488: If $t \subseteq d$ is a solution of the CSP and
489: $\{ d_i \mid 1 \le i \le n\}$ is a partition of $d$ then
490: $t \subseteq \cup_{1 \leq i \leq n} CL\downarrow (d_i, L)$.
491: \end{lemma}
492:
493: \begin{proof}
494: straightforward.
495: \end{proof}
496:
497: Each node of a search tree can be characterized by a quadruple
498: containing the environment $d$ (which have been computed up to now),
499: the depth $p$ in the tree, the operator $f$ (local consistency
500: operator or restriction operator) connecting it with its father and
501: the restricted environment $e$.
502: The restricted environment is obtained from the initial environment
503: when only the restricted operators are applied.
504:
505: \begin{definition}
506: A \emph{search node} is a quadruple $(d, e, f, p)$ with
507: $d, e \in {\cal P}(\mathbb{D})$, $f \in F \cup \{\bot\}$ and
508: $p \in \bbbn$.
509: \end{definition}
510:
511: The depth and the restricted environment allow to localize the node in
512: the search tree.
513:
514: There exists two kinds of transition in a search tree, those caused by
515: a local consistency operator which ensure the passage to one only son
516: and the transitions caused by a labeling which ensure the passage to
517: some sons (as many as environments in the partition).
518:
519: \begin{definition}
520: A \emph{search tree} is a tree for which each node is a search step
521: inductively defined by:
522: \begin{itemize}
523: \item $(\mathbb{D}, \mathbb{D}, \bot, 0)$ is the root of the tree,
524: \item if $(d, e, op, p)$ is a non leave node then it has:
525: \begin{itemize}
526: \item ever one son: $(d \cap f(d), e, f, p+1)$ with
527: $f \in L$;
528: \item ever $n$ sons:
529: $(d \cap f_i(d), e \cap f_i(d), f_i, p+1)$
530: with $\{f_i(d) \mid 1 \leq i \leq n \}$ a
531: partition of $d$ and $f_i \in R$.
532: \end{itemize}
533: \end{itemize}
534: \end{definition}
535:
536: \begin{definition}
537: A search tree is said \emph{complete} if each leaf $(d,e,f,p)$
538: is such that: $d = CL\downarrow(e,L)$.
539: \end{definition}
540:
541: This section has formally described the computation of solvers in
542: terms of search trees. Each branch is an iteration of operators.
543:
544:
545: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
546: \section{Value withdrawal explanations}
547: \label{Sect:VWE}
548: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
549:
550: This section is devoted to value withdrawal explanations.
551: These explanations are defined as trees which can be extracted from a
552: computation.
553: First, rules are associated with local consistency operators,
554: restriction operators and the labeling process. Explanations are then
555: defined from a system of such rules \cite{Aczel-handbook-77}.
556:
557: From now on we consider a fixed CSP and a fixed computation.
558: The set of local consistency operators is denoted by $L$ and the set
559: of restriction operators by $R$.
560: The labeling introduces a notion of context based on the restricted
561: environments of the search node.
562: The following notation is used:
563: $\Gamma \vdash h$ with $\Gamma \subseteq {\cal P}(\mathbb{D})$ and $h
564: \in \mathbb{D}$. $\Gamma$ is named a \emph{context}.
565:
566: Intuitively, $\Gamma \vdash h$ means $\forall e \in \Gamma, h \not\in
567: CL\downarrow (e,L \cup R)$. A $\Gamma$ is an union of restricted
568: environments, that is each $e \in \Gamma$ corresponds to a branch of
569: the search tree. If an element $h$ is removed in different branches of
570: the search tree, then a context for $h$ may contain all these
571: branches.
572:
573: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
574: \subsection{Rules}
575: \label{Sect:T}
576:
577: The definition of explanations is based on three kinds of rules.
578: These rules explain the removal of a value as the consequence of other
579: value removals or as the consequence of a labeling.
580:
581: First kind of rule is associated with a local consistency
582: operator. Indeed, such an operator can be defined by a system of rules
583: \cite{Aczel-handbook-77}. If the type of this operator is $(\Win,
584: \Wout)$, each rule explains the removal of a value in the environment
585: of $\Wout$ as the consequence of the lack of values in the environment
586: of $\Win$.
587:
588: \begin{definition}
589: \label{Def:LCR}
590: The set of \emph{local consistency rules} associated with $l \in L$
591: is:
592: \begin{center}
593: \begin{tabular}{rcl}
594: & $\Gamma \vdash h_1 \ldots \Gamma \vdash h_n$ & \\
595: ${\cal R}_l = \{$ & $\hrulefill$ &
596: $\mid \Gamma \subseteq {\cal P}(\mathbb{D}), \forall d \subseteq
597: \mathbb{D}, h_1, \ldots, h_n \not\in d \Rightarrow h \not\in
598: l(d)\}$ \\
599: & $\Gamma \vdash h$ & \\
600: \end{tabular}
601: \end{center}
602: \end{definition}
603:
604: Intuitively, these rules explain the propagation mechanism. Using its
605: notation, the definition \ref{Def:LCR} justify the removal of $h$
606: by the removals of $h_1, \ldots, h_n$.
607:
608: \begin{example}
609: $\forall e \in \mathbb{D}$, the rule
610: \begin{small}
611: \begin{center}
612: \begin{tabular}{ccc}
613: $\{e\} \vdash ($PM$,2)$ & & $\{e\} \vdash ($PM$,3)$ \\
614: \multicolumn{3}{c}{$\hrulefill$} \\
615: \multicolumn{3}{c}{$\{e\} \vdash ($AM$,1)$}\\
616: \end{tabular}
617: \end{center}
618: \end{small}
619: is associated with the local consistency operator of type
620: $(\{$PM$\},\{$AM$\})$ (for the constraint AM $\neq$ PM).\hfill$\Box$
621: \end{example}
622:
623: As said above, the context is only concerned by labeling. So, here,
624: the rule does not modify it. Note that if we restrict ourselves to
625: solving by consistency techniques alone (that is without any
626: labeling), then the context will always be the initial environment and
627: can be forgotten \cite{FerLesTes-wflp-02}.
628:
629: From now on, we consider ${\cal R}_L = \cup_{l \in L} {\cal R}_l$.
630:
631: The second kind of rules is associated to restriction operators. In
632: this case the removal of a value is not the consequence of any other
633: removal and so these rules are facts.
634:
635: \begin{definition}
636: The set of \emph{restriction rules} associated with $r \in R$ is:
637: \begin{center}
638: \begin{tabular}{rcl}
639: ${\cal R}_r = \{$ & $\hrulefill$ &
640: $\mid h \not\in r(\mathbb{D}), d \subseteq r(\mathbb{D}) \}$ \\
641: & $\{d\} \vdash h$ & \\
642: \end{tabular}
643: \end{center}
644: \end{definition}
645:
646: These rules provide the values which are removed by a restriction.
647:
648: \begin{example}
649: The set of restriction rules associated with the restriction operator
650: $r$ such that $\forall d \in \mathbb{D}, r(d) = \mathbb{D}|_{V
651: \setminus \{PM\}} \cup \{ ($PM$, 1) \}$ is:
652:
653: \begin{small}
654: \begin{tabular}{cccccc}
655: $\{$ & $\hrulefill$ &, & $\hrulefill$ & $\}$ & with
656: $e_1 \subseteq r(\mathbb{D})$. \\
657: & $\{e_1\} \vdash ($PM$,2)$ & & $\{e_1\} \vdash ($PM$,3)$ \\
658: \end{tabular}
659: \end{small}\hfill$\Box$
660: \end{example}
661:
662: This restriction ensures the computation to go in a branch of the
663: search tree and must be memorized because future removals may be true
664: only in this branch. The context is modified in order to remember that
665: the computation is in this branch.
666:
667: From now on, we consider ${\cal R}_R = \cup_{r \in R} {\cal R}_r$.
668:
669: %La derniere regle sert a collecter les informations sur une valeur
670: %retiree. Si durant une resolution, une valeur est retiree dans
671: %differentes branches de l'arbre de recherche, un arbre de preuve
672: %pourra être construit pour chacun de ces retraits. La regle suivante
673: %permet de regrouper toutes les informations concernant le retrait
674: %d'une valeur dans differentes branches de l'arbre de recherche dans un
675: %seul arbre de preuve.
676:
677: The last kind of rule corresponds to the reunion of informations
678: coming from several branches of the search tree.
679:
680: \begin{definition}
681: The set of \emph{labeling rules} for $h \in \mathbb{D}$ is defined by:
682: \begin{center}
683: \begin{tabular}{rcl}
684: & $\Gamma_1 \vdash h \ldots \Gamma_n \vdash h$ & \\
685: ${\cal R}_h = \{$ & $\hrulefill$ & $\mid \Gamma_1, \ldots, \Gamma_n
686: \subseteq {\cal P}(\mathbb{D}) \}$ \\
687: & $\Gamma_1 \cup \ldots \cup \Gamma_n \vdash h$ & \\
688: \end{tabular}
689: \end{center}
690: \end{definition}
691:
692: Intuitively, if the value $h$ has been removed in several branches,
693: corresponding to the contexts $\Gamma_1, \ldots, \Gamma_n$, then a
694: unique context can be associated to $h$: this context is the union of
695: these contexts.
696:
697: \begin{example}
698: For all $e_1, e_2, e_3 \in \mathbb{D}$,
699: \begin{small}
700: \begin{tabular}{ccc}
701: $\{e_1\} \vdash ($MP$,2)$ & $\{e_2\} \vdash ($MP$,2)$ &
702: $\{e_3\} \vdash ($MP$,2)$ \\
703: \multicolumn{3}{c}{$\hrulefill$} \\
704: \multicolumn{3}{c}{$\{e_1\} \cup \{e_2\} \cup \{e_3\} \vdash ($MP$,2)$} \\
705: \end{tabular}
706: \end{small}
707: is a labeling rule.
708: \end{example}
709:
710: From now on, we consider
711: ${\cal R}_\mathbb{D} = \cup_{h \in \mathbb{D}} {\cal R}_h$.
712:
713: The system of rules ${\cal R}_L \cup {\cal R}_R \cup {\cal
714: R}_\mathbb{D}$ can now be used to build explanations of value
715: withdrawal.
716:
717:
718: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
719: \subsection{Proof trees}
720: \label{Sect:ADP}
721:
722: In this section, proof trees are described from the rules of the
723: previous section. It is proved that there exists such a proof tree for
724: each element which is removed during a computation. And finally, it is
725: shown how to obtain these proof trees.
726:
727: \begin{definition}
728: A \emph{proof tree} with respect to a set of rules
729: ${\cal R}_L \cup {\cal R}_R \cup {\cal R}_\mathbb{D}$ is a finite
730: tree such that, for each node labeled by $\Gamma \vdash h$, if $B$ is
731: the set of labels of its children, then
732: \begin{center}
733: \begin{tabular}{cl}
734: $B$ \\
735: $\hrulefill$
736: & $\in {\cal R}_L \cup {\cal R}_R \cup {\cal R}_\mathbb{D}$. \\
737: $\Gamma \vdash h$ \\
738: \end{tabular}
739: \end{center}
740: \end{definition}
741:
742: Next theorem ensures that there exists a proof tree for each element
743: which is removed during a computation.
744:
745: \begin{theorem}
746: \label{Theoreme:ADPCL}
747: $\Gamma \vdash h$ is the root of a proof tree if and only if
748: $\forall e \in \Gamma, h \not \in CL\downarrow (e,R)$.
749: \end{theorem}
750:
751: \begin{proof}
752: $\Rightarrow$: inductively on each kind of rule:
753: \begin{itemize}
754: \item for local consistency rules, if $\forall i, 1 \le i \le n,
755: h_i \not\in CL\downarrow(e_i,R)$ then $h_i \not\in CL\downarrow(e_1
756: \cap \ldots \cap e_n,R)$ and so (because $h \leftarrow \{h_1,
757: \ldots, h_n\} \in {\cal R}$) $h \not\in CL\downarrow(\{e_1 \cap
758: \ldots \cap e_n\},R)$;
759: \item for restriction rules, $h \not\in e$ so $h \not\in
760: CL\downarrow (e,R)$;
761: \item straightforward for labeling rules.
762: \end{itemize}
763: $\Leftarrow$: if $\forall i, 1 \le i \le n, h \not\in
764: CL\downarrow(e_i,R)$ then (\cite{FerLesTes-RR2001-05})
765: there exists a proof tree rooted by $h$ for each $e_i$. So, with
766: context notion, $\forall i, 1 \le i \le n, \{e_i\} \vdash h$ is the
767: root of a proof tree. Thus, thanks to the labeling rule,
768: $\{e_1, \ldots, e_n\} \vdash h$ is the root of a proof tree.
769: \end{proof}
770:
771: Last part of the section is devoted to show how to obtain these trees
772: from a computation, that is from a search tree.
773:
774: Let us recall that $\cons(h,T)$ is the tree rooted by $h$ and with the
775: set of sub-trees $T$.
776: The traversal of the search tree is in depth first. Each branch can
777: then be considered separately. The descent in each branch can be
778: viewed as an iteration of local consistency operators and restriction
779: operators. During this descent, proof trees are inductively built
780: thanks to the rules associated to these two kind of operators
781: (labeling rules are not necessary for the moment).
782: Each node being identified by its depth, the set of trees associated
783: to the node $(d_p, e_p, f_p, p)$ is denoted by $S^p\da$.
784:
785: These sets are inductively defined as follows:
786: \begin{itemize}
787: \item $S^0\da = \emptyset$;
788: \item if $f_{p+1} \in R$ then:
789:
790: \vspace{-12pt}
791: \hspace{-11pt}
792: \begin{tabular}{rcl}
793: & $\{\root(t) \mid t \in T\}$ & \\
794: $S^{p+1}\da = S^p\da \cup \{ \cons(\{e_p\} \vdash h, T) \mid T
795: \subseteq S^p\da, h \in d_p,$ & $\hrulefill$ & $\in
796: {\cal R}_{f_{p+1}} \}$ \\
797: & $\{e_p\} \vdash h$
798: \end{tabular}
799: \item if $f_{p+1} \in L$ then:
800:
801: \hspace{-11pt}
802: \begin{tabular}{rcl}
803: $S^{p+1}\da = S^p\da \cup \{ \cons(\{e_{p+1}\} \vdash h,
804: \emptyset) \mid h \in d_p,$ & $\hrulefill$ & $\in
805: {\cal R}_{f_{p+1}} \}$ \\
806: & $\{e_{p+1}\} \vdash h$
807: \end{tabular}
808: \end{itemize}
809:
810: To each node $(d, e, f, p)$ is then associated a set of proof tree
811: denoted by $S\da(d, e, f, p)$.
812:
813: A second phase consists in climbing these sets to the root, grouping
814: together the trees rooted by a same element but with different
815: contexts. To each node $(d, e, f, p)$ is associated a new set of
816: proof trees $S\ua(d,e,f,p)$. This set is inductively defined:
817: \begin{itemize}
818: \item if $(d, e, f, p)$ is a leaf then
819: $S\ua(d,e,f,p) = S\da(d,e,f,p)$;
820: \item if $l \in L$ then $S\ua(d, e, f, p) =
821: S\da(d \cup l(d), e, l, p+1)$;
822: \item if $\{ r_i(d) \mid 1 \leq i \leq n \}$ is a partition of
823: $d$ then $S\ua(d,e,f,p) = S \cup S' $ with
824: $S = \cup_{1 \leq i \leq n} S\ua(d \cap r_i(d), e \cap r_i(c),
825: r_i, p+1)$ and
826:
827: \begin{tabular}{ccc}
828: & $\{root(t) \mid t \in T\}$ & \\
829: $S' = \{\cons (\Gamma \vdash h, T) \mid$ & $\hrulefill$ &
830: $\in {\cal R}_\mathbb{D}, T \subseteq S \}$. \\
831: & $\Gamma \vdash h$ &
832: \end{tabular}
833: \end{itemize}
834:
835: \begin{corollary}
836: If the search tree rooted by $(\mathbb{D},\mathbb{D},\bot,0)$ is
837: complete then $\{\root(t) \mid t \in S \ua
838: (\mathbb{D},\mathbb{D},\bot,0)\} = \{\Gamma \vdash h \mid \forall e
839: \in \Gamma, h \not\in CL\downarrow(e,L)\}$.
840: \end{corollary}
841: \begin{proof}
842: by theorem~\ref{Theoreme:ADPCL}.
843: \end{proof}
844:
845: These proof trees are explanations for the removal of their root.
846:
847: \begin{example}
848: An explanation for the withdrawal of the value $2$ from the domain of
849: MP can be:
850: \begin{small}
851: \begin{center}
852: \begin{tabular}{ccccccc}
853: $\hrulefill$ & & $\hrulefill$ \\
854: $\{e_1\} \vdash ($PM$,2)$ & & $\{e_1\} \vdash ($PM$,3)$ \\
855: \multicolumn{3}{c}{$\hrulefill$} & & $\hrulefill$ & & $\hrulefill$ \\
856: \multicolumn{3}{c}{$\{e_1\} \vdash ($AM$,1)$} &
857: & $\{e_2\} \vdash ($PM$,1)$ & & $\{e_3\} \vdash ($PM$,1)$ \\
858: & $\hrulefill$ & & & $\hrulefill$ & & $\hrulefill$ \\
859: & $\{e_1\} \vdash ($MP$,2)$ & & & $\{e_2\} \vdash ($MP$,2)$ & &
860: $\{e_3\} \vdash ($MP$,2)$ \\
861: & \multicolumn{6}{c}{$\hrulefill$} \\
862: & \multicolumn{6}{c}{$\{e_1\} \cup \{e_2\} \cup \{e_3\} \vdash ($MP$,2)$} \\
863: \end{tabular}
864: \end{center}
865: \end{small}
866: with $e_1$, $e_2$ and $e_3$ such that:
867: \begin{itemize}
868: \item $e_1 = \mathbb{D}|_{V \setminus \{PM\}} \cup \{($PM$,1)\}$
869: \item $e_2 = \mathbb{D}|_{V \setminus \{PM\}} \cup \{($PM$,2)\}$
870: \item $e_3 = \mathbb{D}|_{V \setminus \{PM\}} \cup \{($PM$,3)\}$
871: \end{itemize}
872: This tree must be understood as follows: the restriction of the search
873: space to $e_1$ eliminates the values 2 and 3 of PM. Since AM $\neq$
874: PM, the value 1 is removed of AM. And since MP $>$ AM, the value 2 is
875: removed of MP.
876: In the same way, the value 2 is also removed of MP with the
877: restriction $e_2$ and $e_3$. And finally, the root ensures that this
878: value is removed in each of these branches.
879: \hfill$\Box$
880: \end{example}
881:
882: The size of explanations strongly depends on the consistency used, the
883: size of the domains and the type of constraint.
884: For example, if all the local consistency operators are defined from
885: equality constraints with arc-consistency, the size of explanations
886: will be minimal. On the opposite side, if all local consistency
887: operators are defined from inequality constraints including more than
888: two variables, their size will be maximal.
889: Note that even if the width of explanations is large, their height
890: remains correct in general.
891: It is important to recall that these explanations are a theoretical
892: tool. So, an implementation could be more efficient. It is possible
893: for example to group together values of a same variable which are
894: removed by the same reason.
895:
896:
897: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
898: \section{Interest for Programming Environments}
899: \label{Sect:IPE}
900: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
901:
902:
903: The understanding of solvers computation provided by the explanations
904: is an interesting source of information for constraint (logic)
905: programming environments. Moreover, explanations have already been
906: used in several ones. The theoretical model of value withdrawal
907: explanation given in the paper can therefore be an interesting tool
908: for constraint (logic) programming environments.
909:
910: The main application using explanations concerns over-constrained
911: problems. In these problems, the user is interesting in information
912: about the failure, that is to visualize the set of constraints
913: responsible for this failure. He can therefore relax one of them and
914: may obtain a solution.
915:
916: In the PaLM system, a constraint retraction algorithm have been
917: implemented thanks to explanations. Indeed, for each value removed
918: from the environment, there exists an explanation set containing the
919: operators responsible for the removal. So, to retract a constraint
920: consists in two main steps: to re-introduce the values which contain an
921: operator associated to the retracted constraint in their explanation,
922: and to wake up all the operators which can remove a re-introduced
923: value, that is which are defined by a rule having such a value as
924: head.
925: The theoretical approach of the explanations have permitted to prove
926: the correctness of this algorithm based on explanations. There did not
927: exist any proof of it whereas the one we propose is
928: immediate. Furthermore, this approach have proved the correctness of a
929: large family of constraints retraction algorithms used in others
930: constraints environments and not only the one based on explanations.
931:
932: The interest for explanations in debugging is growing. Indeed, to
933: debug a program is to look for something which is not correct in a
934: solver computation. So, the information about the computation given by
935: the explanations can be very precious.
936:
937: They have already been used for failure analysis. In constraint
938: programming, a failure is characterized by an empty domain.
939: A failure explanation is then a set of explanations (one explanation
940: for each value of the empty domain).
941: Note that in the PaLM system, labeling has been replaced by dynamic
942: backtracking based on the combination of failure explanation and
943: constraint retraction.
944:
945: An interesting perspective seems to be the use of explanations for the
946: declarative debugging of constraint programs. Indeed, when a symptom
947: of error (a missing solution) appears after a constraint solving,
948: explanations can help to find the error (the constraint responsible
949: for the symptom). For example, if a user is expected a solution
950: containing the value $v$ for a variable $x$ but does not obtain any
951: such solution, an explanation for the removal of $(x,v)$ is a useful
952: structure to localize the error. The idea is to go up in the tree from
953: the root (the symptom) to a node (the minimal symptom) for which each
954: son is correct. The error is then the constraint which ensures the
955: passage between the node and its sons.
956:
957: The theoretical model given in the paper will, I wish, bring new ideas
958: and solutions for the debugging in constraint programming and other
959: environments.
960:
961: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
962: \section{Conclusion}
963: \label{Sect:Conclusion}
964: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
965:
966: The paper was devoted to the definition of value withdrawal
967: explanations. The previous notions of explanations (theoretically
968: described in \cite{FerLesTes-wflp-02}) only dealt with domain
969: reduction by local consistency notions. Here, the notion of labeling
970: have been fully integrated in the model.
971:
972: A solver computation is formalized by a search tree where each branch
973: is an iteration of operators. These operators can be local consistency
974: operators or restriction operators. Each operator is defined by a set
975: of rules describing the removal of a value as the consequence of the
976: removal of other values. Finally, proof trees are built thanks to
977: these rules. These proof trees are explanations for the removal of a
978: value (their root).
979:
980: The interest in explanations for constraint (logic) programming
981: environment is undoubtedly. The theoretical model proposed here have
982: already validate some algorithms used in some environments and will, I
983: wish, bring new ideas and solutions for constraint (logic) programming
984: environments, in particular debugging of constraint programs.
985:
986: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
987: %\bibliographystyle{abbrv}
988: %\bibliography{/home/lesaint/recherche/biblio}
989: \begin{thebibliography}{10}
990:
991: \bibitem{Aczel-handbook-77}
992: P.~Aczel.
993: \newblock An introduction to inductive definitions.
994: \newblock In J.~Barwise, editor, {\em Handbook of Mathematical Logic},
995: volume~90 of {\em Studies in Logic and the Foundations of Mathematics},
996: chapter C.7, pages 739--782. North-Holland Publishing Company, 1977.
997:
998: \bibitem{Apt-tcs-99}
999: K.~R. Apt.
1000: \newblock The essence of constraint propagation.
1001: \newblock {\em Theoretical Computer Science}, 221(1--2):179--210, 1999.
1002:
1003: \bibitem{CouCou-saipl-77}
1004: P.~Cousot and R.~Cousot.
1005: \newblock Automatic synthesis of optimal invariant assertions mathematical
1006: foundation.
1007: \newblock In {\em Symposium on Artificial Intelligence and Programming
1008: Languages}, volume 12(8) of {\em ACM SIGPLAN Not.}, pages 1--12, 1977.
1009:
1010: \bibitem{DiaCod-acm-00}
1011: D.~Diaz and P.~Codognet.
1012: \newblock The {GNU}-{P}rolog system and its implementation.
1013: \newblock In {\em ACM Symposium on Applied Computing}, volume~2, pages
1014: 728--732, 2000.
1015:
1016: \bibitem{FagFowSol-iclp-95}
1017: F.~Fages, J.~Fowler, and T.~Sola.
1018: \newblock A reactive constraint logic programming scheme.
1019: \newblock In {\em International Conference on Logic Programming}. MIT Press,
1020: 1995.
1021:
1022: \bibitem{FerLesTes-RR2001-05}
1023: G.~Ferrand, W.~Lesaint, and A.~Tessier.
1024: \newblock Theoretical foundations of value withdrawal explanations in
1025: constraints solving by domain reduction.
1026: \newblock Technical Report 2001-05, LIFO, University of Orl\'eans,
1027: Universit{\'e} d'Orl{\'e}ans, BP 6759, F-45067 Orl{\'e}ans Cedex 2, November
1028: 2001.
1029:
1030: \bibitem{FerLesTes-wflp-02}
1031: G.~Ferrand, W.~Lesaint, and A.~Tessier.
1032: \newblock Theoretical foundations of value withdrawal explanations for domain
1033: reduction.
1034: \newblock In M.~Falaschi, editor, {\em 11th International Workshop on
1035: Functional and (Constraint) Logic Programming}, page to appear, Grado, Italy,
1036: June 2002.
1037:
1038: \bibitem{BarJus-trics-00}
1039: N.~Jussien and V.~Barichard.
1040: \newblock The {PaLM} system: explanation-based constraint programming.
1041: \newblock In {\em Proceedings of {TRICS}: {T}echniques fo{R} {I}mplementing
1042: {C}onstraint programming {S}ystems, a post-conference workshop of {CP 2000}},
1043: pages 118--133, 2000.
1044:
1045: \bibitem{Lab-trics-00}
1046: F.~Laburthe and the OCRE~project.
1047: \newblock Choco: implementing a {CP} kernel.
1048: \newblock In {\em TRICS, {T}echniques fo{R} {I}mplementing {C}onstraint
1049: programming {S}ystems, a post-conference workshop of {CP 2000}}, Technical
1050: report TRA9/00, Singapore, 2000.
1051:
1052: \bibitem{Tsang-book-93}
1053: E.~Tsang.
1054: \newblock {\em Foundations of Constraint Satisfaction}.
1055: \newblock Academic Press, 1993.
1056:
1057: \end{thebibliography}
1058:
1059: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1060:
1061: \end{document}
1062: