1: \NeedsTeXFormat{LaTeX2e}
2:
3: \documentclass[twoside,12pt]{article}
4:
5: \usepackage{amssymb}
6:
7: \def\bbbn{{\rm I\!N}}
8: \def\bbbr{{\rm I\!R}}
9: \def\bbbz{{{\hbox{\sf Z\kern-0.4em Z}}}}
10: \def\var{{\it var}}
11: \def\reduc{{\it reduc}}
12: \def\expl{{\it expl}}
13: \def\ptrule#1#2#3{\begin{tabular}[t]{cl}
14: {#2} & \\
15: \hrulefill & \hspace*{-1em}{\footnotesize {#1}}\\
16: {#3} & \\
17: \end{tabular}}
18: \def\ptrules#1#2#3#4#5{\begin{tabular}[t]{cl}
19: {#3} & \\
20: \hrulefill & \hspace*{-1em}{\footnotesize {#1}}\\
21: {#4} & \\
22: \hrulefill & \hspace*{-1em}{\footnotesize {#2}}\\
23: {#5} & \\
24: \end{tabular}}
25:
26: \newtheorem{defth}{Definition}
27: \newenvironment{definition}{\begin{defth}\parindent=0mm}{\end{defth}}
28: \newtheorem{lemmath}{Lemma}
29: \newenvironment{lemma}{\begin{lemmath}\parindent=0mm}{\end{lemmath}}
30: \newtheorem{corollaryth}{Corollary}
31: \newenvironment{corollary}{\begin{corollaryth}\parindent=0mm}{\end{corollaryth}}
32: \newtheorem{theoremth}{Theorem}
33: \newenvironment{theorem}{\begin{theoremth}\parindent=0mm}{\end{theoremth}}
34: \newenvironment{proof}{\begin{quotation}\noindent\parindent=0mm{\it Proof. }%
35: \begin{rm}}{\hfill$\square$\end{rm}\end{quotation}}
36: \newtheorem{exampleth}{\em Example}
37: \newenvironment{example}[1]{\begin{exampleth}{#1}\parindent=0mm\par\begin{rm}}%
38: {\end{rm}\end{exampleth}}
39: \newenvironment{remark}{\begin{quotation}\noindent\parindent=0mm%
40: {\it Remark. }\begin{rm}}{\end{rm}\end{quotation}}
41: \newenvironment{program}{\begin{displaymath}\begin{array}{l}}%
42: {\end{array}\end{displaymath}}
43:
44: \begin{document}
45: \pagestyle{myheadings}
46: \markboth{AADEBUG 2000}{Value Withdrawal Explanation in CSP}
47: \title{Value Withdrawal Explanation in CSP
48: \footnote{In M. Ducass\'e (ed), proceedings of the Fourth
49: International Workshop on Automated Debugging (AADEBUG 2000), August
50: 2000, Munich. COmputer Research Repository (http://www.acm.org/corr/),
51: cs.SE/0012005; whole proceedings: cs.SE/0010035.}}
52: \author{G\'erard Ferrand \and Willy Lesaint \and Alexandre Tessier\\
53: LIFO, BP 6759, 45067 Orl\'eans Cedex 2, France\\
54: http://www.univ-orleans.fr/SCIENCES/LIFO}
55: \date{}
56: \maketitle
57: \begin{abstract}
58: This work is devoted to constraint solving motivated by the debugging
59: of constraint logic programs a la GNU-Prolog. The paper focuses only
60: on the constraints. In this framework, constraint solving amounts to
61: domain reduction. A computation is formalized by a chaotic
62: iteration. The computed result is described as a closure. This model
63: is well suited to the design of debugging notions and tools, for
64: example failure explanations or error diagnosis. In this paper we
65: detail an application of the model to an explanation of a value
66: withdrawal in a domain. Some other works have already shown the
67: interest of such a notion of explanation not only for failure
68: analysis.
69: \end{abstract}
70:
71:
72: %%%%%%%%%%%
73: \section{Introduction}
74: \label{Sect:Introduction}
75: %%%%%%%%%%%
76:
77: Constraint Logic Programming (CLP) \cite{MarStu-book-98} can be viewed
78: as the reunion of two programming paradigms : logic programming and
79: constraint programming. Declarative debugging of constraints logic
80: programs has been treated in previous works \cite{Tessier-aadebug-97}
81: and tools have been produced for this aim \cite{Tessier-discipl-00}
82: during the DiSCiPl (Debugging Systems for Constraint Programming)
83: ESPRIT Project. But these works deal with the clausal aspects of
84: CLP. This paper focuses on the constraint level alone. The tools used at
85: this level strongly depend on the constraint domain and the way to
86: solve constraints. Here we are interested in a wide field of
87: applications of constraint programming: {\em finite domains} and
88: {\em propagation}.
89:
90: The aim of constraint programming is to solve Constraint Satisfaction
91: Problems (CSP) \cite{Tsang-book-93}, that is to provide an
92: instantiation of the variables which is correct with respect to the
93: constraints.
94:
95: The solver goes towards the solutions combining two different methods.
96: The first one (labeling) consists in partitioning the domains until to
97: obtain singletons and, testing them. The second one (domain reduction)
98: reduces the domains eliminating some values which cannot be correct
99: according to the constraints. Labeling provides exact solutions
100: whereas domain reduction simply approximates them. In general, the
101: labeling alone is very expensive and a good combination of the two
102: methods is more efficient.
103: In this paper labeling is not really treated. We consider only one
104: branch of the search tree: the labeling part is seen as additional
105: constraint to the CSP. In future work, we plan to extend our framework
106: in order to fully take into account labeling and the whole search tree
107: (instead of a single branch).
108:
109: This kind of computation is not easy to debug because CSP are not
110: algorithmic programs \cite{Meier-cp-1995}. The constraints are reinvoked
111: according to the domain reductions until a fix-point is reached. But
112: the order of invocation is not known a priori.
113:
114: The main contribution of this paper is to formalize the domain
115: reduction in order to provide a notion of explanation for the basic
116: event which is ``the withdrawal of a value from a domain''.
117: This notion of explanation is essential for the debugging of CSP
118: programs. Indeed, the disappearance of a value from a domain may be a
119: symptom of an error in the program. But the error is not always where the
120: value has disappeared and an analysis of the explanation of the value
121: withdrawal is necessary to locate the error.
122: \cite{GouBen-ase-99} provides a tool to find symptoms, this paper
123: provides a tool which could be used to find errors from symptoms.
124: Explanations are a tool to help debugging: we extract from a (wide)
125: computation a structured part (the explanation) which will be analyzed
126: more efficiently.
127:
128: We are inspired by a constraint programming language over finite domains,
129: GNU-Prolog \cite{CodDia-jlp-96}, because its glass-box approach allows
130: a good understanding of the links between the constraints and the
131: rules.
132:
133: To be easily understandable, the notion of explanation will be first
134: defined in a framework which includes arc consistency and next in a
135: more general framework which includes hyper-arc consistency and also
136: some weaker consistencies usually used in the implemented constraint
137: solvers.
138:
139: An explanation is a subset of rules used during the computation and
140: which are responsible for the removal of a value from a domain.
141: Several works shown that detailed analysis of explanations have a lot
142: of applications \cite{GueJusPri-ejor-00,Jussien-phd-97}. In dynamic
143: problems, the explanations allow to retract constraints without
144: beginning the computation again. In backtracking algorithms, the
145: explanations avoid to repeatedly perform the same search work. This
146: intelligent backtracking can be applied to scheduling problems. It has
147: been proved efficient for Open-shop applications. They are useful for
148: over-constrained problems too. Explanations provide a set of
149: constraints which can be relaxed in order to obtain a solution. But
150: these applications of explanations are outside the scope of this paper
151: (see \cite{Jussien-phd-97}). Here, our definitions of explanations are
152: motivated by applications to debugging, in particular to error
153: diagnosis.
154:
155: An aspect of the debugging of constraint programs is to understand why
156: we have a failure (i.e. we do not obtain any solution)
157: \cite{Fabris-aadebug-97}. This case appears when a domain becomes
158: empty, that is no value of the domain belongs to a solution. So, an
159: explanation of why these values have disappeared provides an
160: explanation of the failure.
161:
162: Another aspect is error diagnosis. Let us assume an expected semantics
163: for the CSP. Consider we are waiting for a solution containing a
164: certain value for a variable, but this value does not appear in the
165: final domain. An explanation of the value withdrawal help us to find
166: what is wrong in our program.
167: It is important to note that the error is not always the constraint
168: responsible of the value withdrawal. Another constraint may have made
169: a wrong reduction of another domain which has finally produced the
170: withdrawal of the value.
171: The explanation is a structured object in which this information may
172: be founded.
173:
174: The paper is organized as follows. Section~\ref{Sect:Preliminaries}
175: gives some notations and basic definitions for Constraint Satisfaction
176: Problems. Section~\ref{Sect:Model} describes a model for domain
177: reduction. Section~\ref{Sect:Explanations} applies the model to
178: explanations. Next section is a conclusion.
179:
180: %%%%%%%%%%%
181: \section{Preliminaries}
182: \label{Sect:Preliminaries}
183: %%%%%%%%%%%
184:
185: We use the following notations: If $F=(F_i)_{i \in I}$ is a family
186: indexed by $I$, and $J \subseteq I$, we denote by $F|_J$ the family
187: $(F_j)_{j \in J}$ indexed by $J$. If $F=(F_i)_{i \in I}$ is a family
188: of sets indexed by $I$, we denote by $\prod F$ the product $\prod_{i
189: \in I} F_i = \{ (e_i)_{i \in I} \mid \mbox{for each }i \in I, e_i \in
190: F_i \}$.
191:
192: Notations in terms of families and tuples as in \cite{Tsang-book-93}
193: are convenient notations in our framework.
194: They are more readable than notations in terms of cartesian products
195: as in \cite{Apt-tcs-99} for example.
196:
197: \medskip
198:
199: Here we only consider the framework of domain reduction as in
200: \cite{VanHentenryck-book-89,CodDia-jlp-96,Benhamou-alp-96,VanEmden-misc-95}.
201: More general framework is described in \cite{MonRos-ai-91}.
202:
203: A {\em Constraint Satisfaction Problem} (CSP) is made of two parts,
204: the syntactic part:
205: \begin{itemize}
206: \item a finite set of variable symbols (variables in short) $V$;
207: \item a finite set of constraint symbols (constraints in short) $C$;
208: \item a function $\var : C \rightarrow {\cal P}(V)$, which associates
209: with each constraint symbol the set of variables of the constraint;
210: \end{itemize}
211: and the semantic part:
212: \begin{itemize}
213: \item a family of non empty domains indexed by the set of variables
214: $D=(D_x)_{x \in V}$, each $D_x$ is the domain of the variable denoted
215: by $x$ ($D_x \not= \emptyset$);
216: \item a family of relations (sets of tuples) $T = (T_c)_{c \in C}$ indexed by the set of constraints $C$, where for each $c \in C$, $T_c \subseteq
217: \prod D|_{\var(c)}$, the members of $T_c$ are called the {\em solutions} of
218: $c$.
219: \end{itemize}
220:
221: A tuple $t \in \prod D$ is a {\em solution} of the CSP
222: $(V,C,\var,D,T)$ if for each $c \in C$, $t|_{\var(c)} \in T_c$.
223:
224: We introduce some useful notations:
225: ${\cal D} = \prod_{x \in V} {\cal P}(D_x)$ (the search space) and
226: ${\cal D}(W) = \prod_{x \in W} {\cal P}(D_x)$.
227:
228: For a given CSP, one is interested in the computation of the
229: solutions. The simplest method consists in generating all the tuples
230: from the initial domains, then testing them. This {\em generate and
231: test} method is clearly expensive for wide domains. So, one prefers to
232: reduce the domains first (``test'' and generate).
233:
234: Here, we focus on the reduction stage. The computing domains must
235: contain all the solutions and must be as small as possible. So, these
236: domains are ``approximations'' of the set of solutions. We describe
237: now, a model for the computation of such approximations.
238:
239: %%%%%%%%%%%
240: \section{A Model of the Operational Semantics}
241: \label{Sect:Model}
242: %%%%%%%%%%%
243:
244: We consider a fixed CSP $(V,C,\var,D,T)$.
245:
246: We propose here a model of the operational semantics of the
247: computation of approximations which will be well suited to define
248: explanations of basic events useful for debugging. Moreover main
249: classical results \cite{Apt-tcs-99,MonRos-ai-91} are proved again in
250: this model.
251:
252: The goal is to compute an approximation of the solutions.
253: A way to achieve this goal is to associate with the constraints some
254: {\em reduction rules}.
255: A rule works on a subset of the variables of the CSP. It eliminates
256: from one domain (and only one in our framework based on hyper-arc
257: consistency) some values which are inconsistent with respect to the
258: other domains.
259:
260: \begin{definition}
261: A {\em reduction rule} $r$ of type $(W,y)$, where $W \subseteq V$ and
262: $y \in W$, is a function $r : {\cal D}(W) \rightarrow {\cal P}(D_y)$
263: such that: for each $d, d' \in {\cal D}(W)$,
264: \begin{itemize}
265: \item {\em (monotonicity)} $(\mbox{for each } x \in W$, $d_x \subseteq d'_x)
266: \Rightarrow r(d) \subseteq r(d')$;
267: \item {\em (contractance)} $r(d) \subseteq d_y$.
268: \end{itemize}
269: \end{definition}
270:
271: The solver is described by a set of rules associated with the
272: constraints of the CSP. We can choose more or less accurate rules for
273: each constraint (in general, the more accurate are the rules, the more
274: expensive is the computation).
275:
276: Other works consider more general kinds of rules
277: \cite{Benhamou-alp-96,Apt-tcs-99}, their types have the form $(W, Z)$
278: with $Z \subseteq W \subseteq V$.
279:
280: \begin{example}{Hyper-arc consistency}
281: Let $W \subseteq V$, $y \in W$, $T \subseteq \prod D|_W$ and $d \in
282: {\cal D}(W)$. The reduction rule $r$ of type $(W,y)$
283: defined by $r(d)=\{t_y \mid t \in (\prod d) \cap T\}$ is an hyper-arc
284: consistency rule. $r$ removes inconsistent values with respect to the
285: variable domains.
286:
287: When $W$ is $\{x,y\}$ it is the well known {\em arc consistency} framework.
288: \end{example}
289:
290: \begin{example}{GNU-Prolog}
291: In GNU-Prolog, such rules are written $x~in~r$ \cite{CodDia-jlp-96},
292: where $r$ is a range dependent on domains of a set of variables. The
293: rule {\tt x~in~0..max(y)} of type $(\{x,y\},x)$ is the function which
294: computes the intersection between the current domain of $x$ and the domain
295: $\{0,1,\ldots,max(y)\}$ where $max(y)$ is the greatest value in the
296: domain of $y$.
297: \end{example}
298:
299: For the sake of simplicity, for each rule, we define its associated
300: reduction operator. This operator applies to the whole family of
301: domains. A single domain is modified: the domain reduced by the
302: reduction rule.
303:
304: The {\em reduction operator} associated with the rule $r$ of type
305: $(W,y)$ is $\reduc_r : {\cal D} \rightarrow {\cal D}$ defined by: for
306: each $d \in {\cal D}$,
307: \begin{itemize}
308: \item
309: $\reduc_r(d)|_{V \setminus \{y\}} = d|_{V \setminus \{y\}}$;
310: \item
311: $\reduc_r(d)_y = r(d|_W)$.
312: \end{itemize}
313: Note that reduction operators are monotonic and contractant (but they
314: are not necessarily idempotent).
315:
316: A reduction rule $r$ is {\em correct} if, for each $d \in {\cal D}$,
317: for each solution $t \in \prod D$,
318: $t \in \prod d \Rightarrow t \in \prod \reduc_r(d)$.
319:
320: \begin{lemma}
321: A reduction rule $r$ of type $(W,y)$ is correct if and only if, for
322: each solution $t$, $r((\{t_x\})_{x \in W}) = \{t_y\}$.
323: \end{lemma}
324:
325: \begin{proof}
326: $\Rightarrow$: apply the definition with $d$ ``reduced'' to a
327: solution.
328:
329: $\Leftarrow$: because reduction operators are monotonic.
330: \end{proof}
331:
332: In practice, each constraint of the CSP is implemented by a set of
333: reduction rules.
334:
335: Let $c \in C$. A reduction rule $r$ of type $(W,y)$ with $W \subseteq
336: \var(c)$ is {\em correct} with respect to $c$ if, for each $d \in
337: {\cal D}$, for each $t \in T_c$, $t \in \prod
338: d|_{\var(c)} \Rightarrow t \in \prod \reduc_r(d)|_{\var(c)}$.
339:
340: \begin{lemma}
341: A reduction rule $r$ of type $(W,y)$ is correct w.r.t. a constraint
342: $c$ if and only if, for each $t \in T_c$, $r((\{t_x\})_{x \in W}) =
343: \{t_y\}$.
344: \end{lemma}
345:
346: \begin{proof}
347: $\Rightarrow$: apply the definition with $d=(\{t_x\})_{x \in V}$ such
348: that $(t_x)_{x \in \var(c)} \in T_c$.
349:
350: $\Leftarrow$: because reduction operators are monotonic.
351: \end{proof}
352:
353: Note that if a reduction rule $r$ is correct w.r.t. a constraint $c$
354: of the CSP then $r$ is correct. But the converse does not hold.
355:
356: \begin{example}{GNU-Prolog}
357: The rule $r$ : {\tt x~in~0..max(y)} is correct with respect to the
358: constraint $c$ defined by $\var(c)=\{x,y\}$ and $T_c=\{(x \mapsto 0,y
359: \mapsto 0),(x \mapsto 0,y \mapsto 1),(x \mapsto 1,y \mapsto 1)\}$
360: ($D_x = D_y = \{0,1\}$ and $c$ is the constraint $x \leq y$).
361: Indeed,
362: \begin{itemize}
363: \item $r(x \mapsto \{0\},y \mapsto \{0\})=\{0\} \cap \{0\}=\{0\}$;
364: \item $r(x \mapsto \{0\},y \mapsto \{1\})=\{0\} \cap \{0,1\}=\{0\}$;
365: \item $r(x \mapsto \{1\},y \mapsto \{1\})=\{1\} \cap \{0,1\} =\{1\}$.
366: \end{itemize}
367: \end{example}
368:
369: Let $R$ be a set of reduction rules.
370:
371: Intuitively, the solver applies the rules one by one replacing the
372: domains of the variables with those it computes. The computation stops
373: when one domain becomes empty (in this case, there is no solution), or
374: when the rules cannot reduce domains anymore (a common fix-point is reached).
375:
376: We will show that if no reduction rule is ``forgotten'', the resulting
377: domains are the same whatever the order the rules are used.
378:
379: The computation starts from $D$ and tries to reduce as much as
380: possible the domain of each variable using the reduction rules.
381:
382: The {\em downward closure} of $D$ by the set of reduction rules $R$ is
383: the greatest common fix-point of the reduction operators associated
384: with the reduction rules of $R$.
385:
386: The downward closure is the most accurate family of domains which can
387: be computed using a set of correct rules. Obviously, each solution
388: belongs to this family.
389:
390: \medskip
391:
392: Now, for each $x \in V$, the inclusion over ${\cal P}(D_x)$ is assumed
393: to be a well-founded ordering (i.e. each $D_x$ is finite).
394:
395: There exists at least two ways to compute the downward closure of $D$
396: by a set of reduction rules $R$:
397: \begin{enumerate}
398: \item
399: the first one is to iterate the operator
400: ${\cal D} \rightarrow {\cal D}$ defined by
401: $d \mapsto (\bigcap_{r \in R} \reduc_r(d)_x)_{x \in V}$ from $D$ until to
402: reach a fix-point;
403: \item
404: the second one is the {\em chaotic iteration} that we are going to
405: recall.
406: \end{enumerate}
407:
408: The following definition is inspired from Apt \cite{Apt-tcs-99}.
409:
410: A {\em run} is an infinite sequence of operators of $R$. A run is {\em
411: fair} if each $r \in R$ appears in it infinitely often. Let us define
412: an {\em iteration} of a set of rules w.r.t. a run.
413:
414: \begin{definition}
415: The {\em iteration} of the set of reduction rules $R$ from the domain
416: $d \in {\cal D}$ with respect to the run $r_1,
417: r_2, \dots$ is the infinite sequence $d^0, d^1, d^2, \dots$ defined
418: inductively by:
419: \begin{enumerate}
420: \item $d^0 = d$;
421: \item for each $j \in \bbbn$, $d^{j+1} = reduc_{r_{j+1}}(d^j)$.
422: \end{enumerate}
423: A {\em chaotic iteration} is an iteration w.r.t. a fair run.
424: \end{definition}
425:
426: The operator $d \mapsto (\bigcap_{r \in R} \reduc_r(d)_x)_{x \in V}$
427: may reduce several domains at each step. But the computations are more
428: intricate and some can be useless. In practice chaotic iterations are
429: preferred, they proceed by elementary steps, reducing only one domain
430: at each step. The next result of confluence
431: \cite{CouCou-saipl-77} ensure that any chaotic iteration reaches the
432: closure. Note that, because $D$ is a family of finite domains, every
433: iteration from $D$ is stationary.
434:
435: \begin{lemma}\label{lemma:chaotic iteration}
436: The limit of every chaotic iteration of the reduction rules $R$ from
437: $D$ is the {\em downward closure} of $D$ by $R$.
438: \end{lemma}
439:
440: \begin{proof}
441: Let $\Theta$ be the downward closure of $D$ by $R$. Let $d^0, d^1,
442: \dots$ be a chaotic iteration of $R$ from $D$ with respect to $r_1,
443: r_2, \dots$. Let $d^{\omega}$ be the limit of the chaotic iteration.
444: Let $(A_i)_{i \in I} \sqsubseteq (B_i)_{i \in I}$ denotes: for each $i
445: \in I$, $A_i \subseteq B_i$.
446:
447: For each $i$, $\Theta \sqsubseteq d^i$, by induction: $\Theta
448: \sqsubseteq d^0 = D$. Assume $\Theta \sqsubseteq d^i$, by
449: monotonicity, $reduc_{r_{i+1}}(\Theta) = \Theta \sqsubseteq
450: \reduc_{r_{i+1}}(d^i) = d^{i+1}$.
451:
452: $d^{\omega} \sqsubseteq \Theta$: There exists $k \in \bbbn$ such that
453: $d^{\omega}=d^k$ because $\sqsubseteq$ is a well-founded ordering. The
454: run is fair, hence $d^k$ is a common fix-point of the reduction
455: operators, thus $d^k \sqsubseteq \Theta$ (the greatest common
456: fix-point).
457: \end{proof}
458:
459: The fairness of runs is a convenient theoretical notion to state the
460: previous lemma. Every chaotic iteration stabilizes, so in practice the
461: computation ends when a common fix-point is reached. Moreover,
462: implementations of solvers use various strategies in order to
463: determinate the order of invocation of the rules.
464:
465: In practice, when a domain becomes empty, we know that there is no solution,
466: so an optimization consists in stopping the computation before the
467: closure is reached. In that case, we say that we have a {\em failure
468: iteration}.
469:
470: %%%%%%%%%%%
471: \section{Application to Event Explanations}
472: \label{Sect:Explanations}
473: %%%%%%%%%%%
474:
475: Sometimes, when a domain becomes empty or just when a value is removed
476: from a domain, the user wants an explanation of this phenomenon
477: \cite{Jussien-phd-97,Fabris-aadebug-97}. The case of failure is the
478: particular case where all the values are removed. It is the reason why
479: the basic event here will be a value withdrawal. Let us consider an
480: iteration, and let us assume that at a step a value is removed from
481: the domain of a variable. In general, all the rules used from the
482: beginning of the iteration are not necessary to explain the value
483: withdrawal. It is possible to explain the value withdrawal by a subset
484: of these rules such that every iteration using this subset of rules
485: removes the considered value. This subset of rules is an explanation
486: of the value withdrawal.
487: This notion of explanation is declarative (does not depend on the
488: computation).
489: We are going to define a more precise notion
490: of explanation: this subset will be structured as a tree.
491:
492: For the sake of clarity, it will be achieved first in a basic but
493: significant full arc consistency like framework. Next, we extend it to
494: weaker arc consistencies (partial arc consistency), and finally to
495: a framework including hyper-arc consistency as a special case.
496: The full and the partial hyper-arc consistency of GNU-Prolog are
497: instances of this framework.
498:
499: \medskip
500:
501: First, we consider special reduction rules called rules of ``abstract arc
502: consistency''. Such a rule is binary and its type has the form
503: $(\{x,y\}, y)$, that is it reduces the domain of $y$ using the domain
504: of $x$.
505:
506: An {\em abstract arc consistency reduction rule} $r$ is defined by two
507: variables $in_r$ and $out_r$ and a function $arc_r : D_{out_r}
508: \rightarrow {\cal P}(D_{in_r})$.
509:
510: Intuitively, $out_r$ is the variable whose domain is modified according
511: to the domain of the other variable $in_r$, and, for $e \in
512: D_{out_r}$, $arc_r(e)$ is a superset of the values connected to $e$
513: by the constraint associated with $r$ (see for example
514: figure~\ref{Figure:The particular case of arc consistency}).
515:
516: \begin{figure}[t]
517: \begin{center}
518: \setlength{\unitlength}{4144sp}%
519: %
520: \begingroup\makeatletter\ifx\SetFigFont\undefined%
521: \gdef\SetFigFont#1#2#3#4#5{%
522: \reset@font\fontsize{#1}{#2pt}%
523: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
524: \selectfont}%
525: \fi\endgroup%
526: \begin{picture}(2857,2932)(752,-2768)
527: \thinlines
528: \put(1351,-1411){\oval(900,2700)}
529: \put(3151,-1411){\oval(900,2700)}
530: \put(1441,-1681){\oval(450,1080)}
531: \special{ps: gsave 0 0 0 setrgbcolor}\put(1351,-331){\line( 5,-1){1800}}
532: \special{ps: grestore}\special{ps: gsave 0 0 0 setrgbcolor}\put(3151,-691){\line(-1, 0){1800}}
533: \special{ps: grestore}\special{ps: gsave 0 0 0 setrgbcolor}\put(3151,-691){\line(-5,-1){1800}}
534: \special{ps: grestore}\special{ps: gsave 0 0 0 setrgbcolor}\put(3151,-1051){\line(-1, 0){1800}}
535: \special{ps: grestore}\special{ps: gsave 0 0 0 setrgbcolor}\put(3151,-1051){\line(-5, 1){1800}}
536: \special{ps: grestore}\special{ps: gsave 0 0 0 setrgbcolor}\put(1441,-1321){\line( 5,-1){1800}}
537: \special{ps: grestore}\special{ps: gsave 0 0 0 setrgbcolor}\put(3241,-1681){\line(-1, 0){1800}}
538: \special{ps: grestore}\special{ps: gsave 0 0 0 setrgbcolor}\put(3241,-1681){\line(-5,-1){1800}}
539: \special{ps: grestore}\special{ps: gsave 0 0 0 setrgbcolor}\put(1351,-1051){\line( 5,-3){1800}}
540: \special{ps: grestore}\special{ps: gsave 0 0 0 setrgbcolor}\put(3151,-2131){\line(-6,-1){1890}}
541: \special{ps: grestore}\special{ps: gsave 0 0 0 setrgbcolor}\put(1441,-2041){\line( 4,-1){1620}}
542: \special{ps: grestore}\special{ps: gsave 0 0 0 setrgbcolor}\put(3061,-2446){\line(-1, 0){1800}}
543: \special{ps: grestore}\put(1351, 29){\makebox(0,0)[b]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}\special{ps: gsave 0 0 0 setrgbcolor}$D_{in_r}$\special{ps: grestore}}}}
544: \put(3151, 29){\makebox(0,0)[b]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}\special{ps: gsave 0 0 0 setrgbcolor}$D_{out_r}$\special{ps: grestore}}}}
545: \put(2251,-241){\makebox(0,0)[b]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}\special{ps: gsave 0 0 0 setrgbcolor}$T_c$\special{ps: grestore}}}}
546: \put(3286,-1726){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}\special{ps: gsave 0 0 0 setrgbcolor}$e$\special{ps: grestore}}}}
547: \put(1306,-1231){\makebox(0,0)[rb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}\special{ps: gsave 0 0 0 setrgbcolor}$arc_r(e)$\special{ps: grestore}}}}
548: \end{picture}
549: \end{center}
550: \caption{The particular case of arc consistency}
551: \label{Figure:The particular case of arc consistency}
552: \end{figure}
553:
554: Formally, the type of $r$ is $(\{ in_r, out_r\}, out_r)$ and $r(d)=\{
555: e \in d_{out_r} \mid arc_r(e) \cap d_{in_r} \not= \emptyset\}$ for
556: each $d \in {\cal D}(\{in_r, out_r\})$.
557:
558: So we have the obvious lemma:
559:
560: \begin{lemma}
561: For each abstract arc consistency reduction rule $r$ and $e \in
562: D_{out_r}$, and for each $d \in {\cal D}(\{in_r, out_r\})$
563: \[
564: \left( \bigwedge_{f \in arc_r(e)} f \not\in d_{in_r} \right)
565: \Rightarrow e \not\in r(d)
566: \]
567: \end{lemma}
568:
569: In particular, if $arc_r(e) = \emptyset$ then we have $e \not\in r(d)$.
570:
571: \begin{example}{Arc consistency}
572: In the framework of arc consistency, each constraint $c$ is binary,
573: that is $\var(c)=\{x,y\}$, and it provides two rules: $r_1$ of type
574: $(\{x,y\},x)$, $r_1(d) = \{ e \in d_x \mid \exists f \in d_y, (x
575: \mapsto e, y \mapsto f) \in T_c\}$, that is, for each $e \in D_x$,
576: $arc_{r_1}(e) = \{f \in D_y \mid (x \mapsto e, y \mapsto f) \in
577: T_c\}$, and the other rule $r_2$ of type $(\{x,y\},y)$ defined
578: similarly.
579:
580: Note that it is possible to define weaker notions of arc
581: consistency, such that $arc_{r_1}(e) \supseteq \{f \in D_y \mid (x
582: \mapsto e, y \mapsto f) \in T_c\}$. But, it will be dealt later in a more
583: general framework.
584: \end{example}
585:
586: \begin{example}{GNU-Prolog}
587: Let us consider the constraint ``{\tt x~\#<~y}'' in GNU-Prolog.
588: This constraint is implemented by two reduction rules, it is the {\em
589: glass-box} paradigm \cite{CodDia-jlp-96,DevSarVan-draft-91}:
590: \begin{enumerate}
591: \item $r_1$ of type $(\{x,y\},x)$ (i.e. $in_{r_1}=y$, $out_{r_1}=x$),
592: with, for each $e \in D_x$, $arc_{r_1}(e)=\{f \in D_y \mid e < f\}$;
593: \item $r_2$ of type $(\{x,y\},y)$ (i.e. $in_{r_2}=x$, $out_{r_2}=y$),
594: with, for each $e \in D_y$, $arc_{r_2}(e)=\{f \in D_x \mid f < e\}$.
595: \end{enumerate}
596: \end{example}
597:
598: Let us suppose that each $r \in R$ is such an abstract arc consistency
599: reduction rule.
600:
601: Let us consider an iteration $d^0, d^1, \ldots$ of $R$ from $D$ with
602: respect to the run $r_1, r_2, \ldots$. Let us assume that the value
603: $e$ has disappeared from the domain of the variable $out_{r_i}$ at the
604: $i$-th step, that is $e \in d^{i-1}_{out_{r_i}}$ but $e \not\in
605: d^i_{out_{r_i}}$. Note that $d^i_{out_{r_i}} =
606: r_i(d^{i-1}|_{\{in_{r_i},out_{r_i}\}}) = \{ e \in d^{i-1}_{out_{r_i}}
607: \mid arc_{r_i}(e) \cap d^{i-1}_{in_{r_i}} \not= \emptyset \}$. So
608: $arc_{r_i}(e) \cap d^{i-1}_{in_{r_i}} = \emptyset$, i.e. for each $f
609: \in arc_{r_i}(e)$, $f \not\in d^{i-1}_{in_{r_i}}$.
610:
611: According to the previous lemma $e \not\in d^{i}_{out_{r_i}}$ because
612: $\bigwedge_{f \in arc_{r_i}(e)} f \not\in d^{i-1}_{in_{r_i}}$.
613: But if $f \not\in d^{i-1}_{in_{r_i}}$ it is because there exists $j_f
614: < i$ such that $f$ has disappeared at the $j_f$-th step that is $f \in
615: d^{j_{f}-1}_{in_{r_i}}$ but $f \not\in d^{j_{f}}_{in_{r_i}}$
616: (note that $in_{r_i} = out_{r_{j_f}}$).
617:
618: Let us define $p(e,i)=\{(f,j) \mid f \in arc_{r_i}(e), f \not\in
619: d^{j}_{out_{r_j}}, f \in d^{j-1}_{out_{r_j}}\}$.
620:
621: So $e \not\in d^i_{out_{r_i}}$ because $\bigwedge_{(f,j) \in p(e,i)} f \not\in d^{j}_{out_{r_j}}$.
622:
623: We are going to define the notion of explanation by {\em abstracting} $d$:
624:
625: \begin{definition} (compare with the previous lemma)
626: For each reduction rule $r$, for each $e \in D_{out_r}$, we define
627: the {\em deduction rule} named $(e, r)$:
628: \[
629: (e,r) : (e, out_r) \leftarrow \{ (f, in_r) \mid f \in arc_r(e) \}
630: \]
631: $(e, out_r)$ is the head of the rule and $\{ (f, in_r) \mid f \in
632: arc_r(e) \}$ is its body.
633: \end{definition}
634:
635: In particular, when $arc_r(e)=\emptyset$ the body is empty and the
636: deduction rule is reduced to ``the fact'' $(e,r) : (e,out(r))
637: \leftarrow \emptyset$.
638:
639: Intuitively, a deduction rule $(e,r) : (e, out(r)) \leftarrow \{ (f,
640: in_{r}) \mid f \in arc_r(e) \}$ should be understood as follow: if all
641: the $f \in arc_r(e)$ are removed from the domain of $in_r$ then $e$
642: is removed from the domain of $out(r)$.
643:
644: The set of deduction rules $(e,r)$ where $r \in R$ and $e \in
645: D_{out_r}$ is exactly an {\em inductive definition} according to
646: \cite{Aczel-handbook-77}, and a proof tree rooted by $(e,y)$ where
647: $y = out_r \in V$ and $e \in D_y$ will be called an explanation for $(e,y)$.
648: Note that a leaf of an explanation corresponds to a fact $(e,r)$ that
649: is the case where $arc_r(e) = \emptyset$.
650:
651: Intuitively, the proof tree provides an explanation of the reason why
652: $e$ may be removed from the domain of $y$.
653:
654: It is important to note that an explanation is merely a tree made of
655: deduction rules, i.e. the $d^i$ of an iteration are not part of the
656: explanation.
657:
658: \begin{example}{GNU-Prolog}\label{Example:explanation}
659: Let us consider the 3 constraints {\tt x~\#<~y}, {\tt y~\#<~z}, {\tt
660: z~\#<~x} with $D_x = D_y = D_z = \{ 0, 1, 2 \}$. The reduction rules
661: are:
662: \begin{itemize}
663: \item $r_1$ of type $(\{x,y\}, x)$, defined by $r_1(d) = \{ e \in d_x
664: \mid arc_{r_1}(e) \cap d_y \neq \emptyset\}$ where $arc_{r_1}(e)=\{f
665: \in D_y \mid e < f\}$;
666: \item $r_2$ of type $(\{x,y\}, y)$, defined by $r_2(d) = \{ e \in d_y
667: \mid arc_{r_2}(e) \cap d_x \neq \emptyset\}$ where $arc_{r_2}(e)=\{f
668: \in D_x \mid f < e\}$;
669: \item $r_3$ of type $(\{y,z\}, y)$, defined by $r_3(d) = \{ e \in d_y
670: \mid arc_{r_3}(e) \cap d_z \neq \emptyset\}$ where $arc_{r_3}(e)=\{f
671: \in D_z \mid e < f\}$;
672: \item $r_4$, $r_5$, $r_6$ are defined in the same way.
673: \end{itemize}
674:
675: Figure~\ref{Figure:Value Withdrawal Explanations} shows three
676: different explanations for $(0,x)$.
677: For example, the first explanation says: $0$ is removed from the
678: domain of $x$ by the reduction rule $r_1$ because $1$ is removed from
679: the domain of $y$ and $2$ is removed from the domain of $y$.
680: $1$ is removed from the domain of $y$ by the reduction rule $r_3$
681: because $2$ is removed from the domain of $z$, and so on...
682:
683: The first and third explanations correspond to some iterations
684: (see example~\ref{Example:explanationsuite}). But the second one does
685: not correspond to an iteration. This introduces some questions
686: (which are going to be answered by theorem~\ref{Theorem:First}).
687:
688: \begin{figure}[t]
689: \begin{center}
690: \ptrule{$(0,r_1)$}%
691: {$(0,x)$}%
692: {\ptrules{$(1,r_3)$}{$(2,r_5)$}
693: {$(1,y)$}
694: {$(2,z)$}
695: {}%
696: \ptrule{$(2,r_3)$}%
697: {$(2,y)$}%
698: {}%
699: }
700: \hspace*{2em}
701: \ptrule{$(0,r_1)$}%
702: {$(0,x)$}%
703: {\ptrules{$(1,r_2)$}{$(0,r_6)$}
704: {$(1,y)$}
705: {$(0,x)$}
706: {}%
707: \ptrule{$(2,r_3)$}%
708: {$(2,y)$}%
709: {}%
710: }
711:
712: \ptrule{$(0,r_6)$}{$(0,x)$}{}
713: \end{center}
714: \caption{Value Withdrawal Explanations}
715: \label{Figure:Value Withdrawal Explanations}
716: \end{figure}
717: \end{example}
718:
719: Explanations are very declarative but they can be extracted from
720: iterations.
721:
722: We are going to define an explanation associated with the event
723: ``withdrawal of a value from a domain in an iteration''. It is introduced by
724: the following theorem.
725:
726: \begin{theorem}\label{Theorem:First}
727: (There exists an explanation for $(e,y)$) if and only if (there exists
728: a chaotic iteration with limit $d^{\omega}$ such that $e \not\in
729: d^{\omega}_y$) if and only if ($e \not\in \Theta_y$, where $\Theta$ is
730: the downward closure).
731: \end{theorem}
732:
733: \begin{proof}
734: The last equivalence is proved by lemma~\ref{lemma:chaotic iteration}.
735: About the first one:
736:
737: $\Leftarrow$: Let $d^0, d^1, ...$ be the chaotic
738: iteration (with respect to the run $r_1, r_2, \ldots$).
739: There exists $i$ such that $e \in d^{i-1}_{y}$ but $e
740: \not\in d^i_y$.
741:
742: We define a tree $\expl(e, y, i)$ which is an explanation for $(e,y)$.
743: $\expl(e, y, i)$ is inductively defined as follows:
744: \begin{itemize}
745: \item $y = out_{r_i}$;
746: \item the root of the tree $\expl(e, y, i)$ is labeled by $(e, y)$;
747: \item (we have previously observed that $e \not\in d^i_{out_{r_i}} = d^i_y$
748: because $\bigwedge_{(f,j) \in p(e,i)} f \not\in d^{j}_{out_{r_j}}$
749: and, for each $(f,j) \in p(e,i)$, $out_{r_j} = in_{r_i}$)
750: the deduction rule used to connect the root to its children,
751: which are labeled by the $(f,out_{r_j})$, is $(e, r_i) :
752: (e, out_{r_i}) \leftarrow \{ (f,in_{r_i}) \mid f \in arc_{r_i}(e) \}$;
753: \item the immediate subtrees of $\expl(e, y, i)$ are the
754: $\expl(f, in_{r_i}, j)$ for $(f,j) \in p(e,i)$.
755: \end{itemize}
756:
757: $\Rightarrow$:
758: let us consider a numbering $1, \ldots, n$ of the nodes of the
759: explanation such that the traversal according to the numbering from
760: $n$ to $1$ corresponds to a breadth first search algorithm. For each
761: $i \in \{1, \ldots, n\}$, let $(e_i, r_i)$ be the name of the rule
762: which links the node $i$ to its children, and let $d^0, \ldots, d^n$
763: be the prefix of every iteration w.r.t. a run which starts by $r_1,
764: \ldots, r_n$. By induction we show that $e_i \not\in d^i_{out(r_i)}$,
765: so $e \not\in d^{\omega}_y$ for every iteration whose run starts by
766: $r_1, \ldots, r_n$.
767: \end{proof}
768:
769: It is important to note that the previous proof is constructive. The
770: definition of $\expl(e, y, i)$ gives an incremental algorithm to
771: compute explanations.
772:
773: \begin{example}{GNU-Prolog}\label{Example:explanationsuite}
774: (Continuation of example~\ref{Example:explanation})
775:
776: Let us consider the iteration $r_5$, $r_3$, $r_1$.
777: The first explanation of figure~\ref{Figure:Value Withdrawal Explanations}
778: says:
779:
780: At the beginning, $d^0_x=\{0,1,2\}$.
781: $arc_{r_5}(2) = \emptyset$ so $2 \not\in d^1_z$.
782:
783: Then, $d^1_z=\{0,1\}$.
784: $arc_{r_3}(1) = \{2\}$ so $2 \not\in d^1_z \Rightarrow 1 \not\in d^2_y$.
785: $arc_{r_3}(2) = \emptyset$ so $2 \not \in d^2_y$.
786:
787: Then, $d^2_y=\{0\}$.
788: $arc_{r_1}(0) = \{1,2\}$ so $(1 \not\in d^2_y \wedge 2 \not\in d^2_y)
789: \Rightarrow 0 \not\in d^3_x$.
790: \end{example}
791:
792: We extend our formalization in order to include weaker arc consistency
793: rules.
794: In GNU-Prolog, a full arc consistency rule uses the whole domain of
795: the input variable, whereas, a partial arc consistency rule only uses
796: its lower and upper bounds. In that case we need two functions $arc$,
797: one for each bound.
798:
799: An {\em abstract arc consistency reduction rule} $r$ is now defined by
800: two variables $in_r$ and $out_r$ and a set $Arc_r$ of functions
801: $D_{out_r} \rightarrow {\cal P}(D_{in_r})$.
802:
803: The type of $r$ is $(\{in_r, out_r\}, out_r)$ and
804: $r(d)=\{ e \in d_{out_r} \mid \bigwedge_{arc \in Arc_r} (arc(e) \cap
805: d_{in_r} \not= \emptyset)\}$ for each
806: $d \in {\cal D}(\{in_r, out_r\})$.
807:
808: Note that for arc consistency, $Arc_r$ contains only one function
809: (it is the previous framework).
810:
811: Obviously, for each $arc \in Arc_r$ we have:
812: \[
813: \left( \bigwedge_{f \in arc(e)} f \not\in d_{in_r} \right)
814: \Rightarrow e \not\in r(d)
815: \]
816:
817: \begin{example}{GNU-Prolog}
818: Let us consider the constraint ``{\tt x~\#=~y+c}'' in GNU-Prolog where
819: $x$, $y$ are variables and $c$ a constant. This constraint is
820: implemented by two reduction rules: $r_1$ of type $(\{x,y\},x)$
821: (i.e. $in_{r_1}=y$, $out_{r_1}=x$) and $r_2$ of type $(\{x,y\},y)$. In
822: GNU-Prolog, $r_1$ is defined by the partial arc consistency rule
823: {\tt x~in~min(y)+c..max(y)+c}.
824:
825: $r_1(d)=\{e \in d_x \mid arc_{r_1}^1(e) \cap d_y \neq \emptyset \wedge
826: arc_{r_1}^2(e) \cap d_y \neq \emptyset\}$ where
827: $arc_{r_1}^1(e)=\{f \in D_y \mid f+c \leq e\}$ and
828: $arc_{r_1}^2(e)=\{f \in D_y \mid e \leq f+c\}$.
829:
830: $r_2$ of type $(\{x,y\},y)$ is defined in the same way by the
831: rule {\tt y~in~min(x)-c..max(x)-c}.
832: \end{example}
833:
834: Let us suppose that each $r \in R$ is such an abstract arc consistency
835: reduction rule.
836:
837: \begin{definition}
838: For each reduction rule $r$, for each $e \in D_{out_r}$, for each
839: $arc \in Arc_r$, we define the {\em deduction rule} named $(e, r, arc)$:
840: \[
841: (e, r, arc) : (e, out_r) \leftarrow \{ (f, in_r) \mid f \in arc(e) \}
842: \]
843: \end{definition}
844:
845: Again the set of deduction rules $(e, r, arc)$ is an inductive
846: definition and this defines a generalization of our previous notion of
847: explanation.
848:
849: \medskip
850:
851: Now we generalize the reduction rules to {\em hyper-arc consistency}.
852:
853: An {\em abstract hyper-arc consistency reduction rule} $r$ is defined by
854: {\em a set} of variables $in_r$, a variable $out_r$ and a set $Arc_r$
855: of functions $D_{out_r} \rightarrow {\cal P}(\prod_{x \in in_r} D_x)$.
856:
857: The type of $r$ is $(in_r \cup \{out_r\}, out_r)$ and
858: $r(d)=\{ e \in d_{out_r} \mid \bigwedge_{arc \in Arc_r}
859: (arc(e) \cap \prod_{x \in in_r} d_x \not= \emptyset)\}$
860: for each $d \in {\cal D}(in_r \cup \{out_r\})$.
861:
862: Note that for hyper-arc consistency, $Arc_r$ contains only one function.
863:
864: Obviously, for each $arc \in Arc_r$ we have:
865: \[
866: \left( \bigwedge_{f \in arc(e)} (f \not\in \prod_{x \in in_r} d_x) \right)
867: \Rightarrow e \not\in r(d)
868: \]
869:
870: that is
871:
872: \[
873: \left( \bigwedge_{f \in arc(e)} \left( \bigvee_{x \in in_r}
874: f_x \not\in d_x \right) \right) \Rightarrow e \not \in r(d)
875: \hspace*{1cm} \mbox{\large (1)} \hspace*{-1.5cm}
876: \]
877:
878: But
879: \[
880: \left( \bigwedge_{f \in arc(e)} \left( \bigvee_{x \in in_r}
881: f_x \not\in d_x \right) \right)
882: \Leftrightarrow
883: \left( \bigvee_{t : arc(e) \rightarrow in_r} \left( \bigwedge_{f \in arc(e)}
884: f_{t(f)} \not\in d_{t(f)} \right) \right)
885: \hspace*{1cm} \mbox{\large (2)} \hspace*{-1.5cm}
886: \]
887: Intuitively, the $t : arc(e) \rightarrow in_r$ are choice functions
888: and each $t(f)$ is one $x$ such that $f_x \not\in d_x$.
889:
890: So we have, for each $t : arc(e) \rightarrow in_r$,
891: \[
892: \left( \bigwedge_{f \in arc(e)} f_{t(f)} \not\in d_{t(f)} \right)
893: \Rightarrow e \not \in r(d)
894: \hspace*{1cm} \mbox{\large (3)} \hspace*{-1.5cm}
895: \]
896:
897: \begin{example}{Hyper-arc Consistency in GNU-Prolog}
898: Let us consider the constraint ``{\tt x~\#=\#~y+z}'' in GNU-Prolog.
899: Let $D_x=D_y=D_z=\{1,2,3\}$.
900: The constraint is implemented by three reduction rules:
901: \begin{itemize}
902: \item $r_1$ of type $(\{x,y,z\},x)$ defined by
903: $r_1(d) = \{e \in d_x \mid \exists f \in \prod_{v \in \{y,z\}} d_v,
904: e = f_y + f_z\}$;
905: \item $r_2$ of type $(\{x,y,z\},y)$ and $r_3$ of type $(\{x,y,z\},z)$
906: defined in the same way.
907: \end{itemize}
908: Here, $in_{r_1} = \{y, z \}$, $out_{r_1} = x$ and $Arc_{r_1} = \{
909: arc \}$, where
910: $arc(e)=\{f \in \prod_{v \in \{y,z\}} D_{v} \mid
911: e = f_y + f_z \}$.
912:
913: For example, $arc(3) = \{ (y \mapsto 1, z \mapsto 2),
914: (y \mapsto 2, z \mapsto 1) \}$.
915: We have as an instance of $(1)$:
916: $(1 \not\in d_y \vee 2 \not\in d_z) \wedge (2 \not\in d_y \vee 1
917: \not\in d_z) \Rightarrow 3 \not\in r_1(d)$.
918: But $(1 \not\in d_y \vee 2 \not\in d_z) \wedge (2 \not\in d_y \vee 1
919: \not\in d_z)$ is equivalent to
920: $(1 \not\in d_y \wedge 2 \not\in d_y) \vee
921: (1 \not\in d_y \wedge 1 \not\in d_z) \vee
922: (2 \not\in d_z \wedge 2 \not\in d_y) \vee
923: (2 \not\in d_z \wedge 1 \not\in d_z)$
924: This equivalence is the corresponding instance of $(2)$.
925: So we have the following instances of $(3)$:
926: \begin{itemize}
927: \item $1 \not \in d_y \wedge 2 \not \in d_y \Rightarrow 3 \not \in
928: r_1(d)$;
929: \item $1 \not \in d_y \wedge 1 \not \in d_z \Rightarrow 3 \not \in
930: r_1(d)$;
931: \item $2 \not \in d_z \wedge 2 \not \in d_y \Rightarrow 3 \not \in
932: r_1(d)$;
933: \item $2 \not \in d_z \wedge 1 \not \in d_z \Rightarrow 3 \not \in
934: r_1(d)$.
935: \end{itemize}
936: \end{example}
937:
938: Again a more general notion of explanation is defined by abstracting
939: $d$.
940:
941: Let us suppose that each $r \in R$ is such an abstract hyper-arc
942: consistency reduction rule.
943:
944: \begin{definition}
945: For each reduction rule $r$, for each $e \in D_{out_r}$, for each
946: $arc \in Arc_r$, for each $t : arc(e) \rightarrow in_r$,
947: we define the {\em deduction rule} named $(e, r, arc, t)$:
948: \[
949: (e, r, arc, t) : (e, out_r) \leftarrow \{ (f_{t(f)}, t(f))
950: \mid f \in arc(e) \}
951: \]
952: \end{definition}
953:
954: The inductive definition for hyper-arc consistency is larger than for arc
955: consistency because of the number of variables of the rules, but in
956: practice (GNU-Prolog), the rules contain two or three variables.
957:
958: %%%%%%%%%%%
959: \section{Conclusion}
960: \label{Sect:Conclusion}
961: %%%%%%%%%%%
962:
963: This paper has given a model for the operational semantics of CSP
964: solvers by domain reduction.
965:
966: This model is applied to the definition of a notion of explanation.
967: An explanation is a set of rules structured as a tree. An interesting
968: aspect of our definition is that a subtree of an explanation is also
969: an explanation (inductive definition).
970:
971: This model can be applied to usual constraint solvers using
972: propagation, for example it takes into account the full and the
973: partial hyper-arc consistency of GNU-Prolog.
974:
975: As it is written in the introduction, constraint solving combines
976: domain reduction and labeling. A perspective is to really take into
977: account labeling in our model.
978:
979: We plan to use explanations in order to diagnose errors in a CSP
980: (according to an expected semantics), in the style of
981: \cite{Shapiro-phd-82,Ferrand-aadebug-93}.
982:
983: Another perspective is to take advantage of the glass-box model
984: \cite{CodDia-jlp-96} and more generally the S-box model
985: \cite{GouBen-ase-99} and to distinguish different levels of rules
986: ({\tt x in r}, built-in constraints, S-box, ...)
987:
988: \section*{Acknowledgements}
989: Discussions with Patrice Boizumault and Narendra Jussien are
990: gracefully acknowledged.
991: We would also like to thank our anonymous referees for the helpful comments.
992:
993: \begin{thebibliography}{10}
994:
995: \bibitem{Aczel-handbook-77}
996: Peter Aczel.
997: \newblock An introduction to inductive definitions.
998: \newblock In Jon Barwise, editor, {\em Handbook of Mathematical Logic},
999: volume~90 of {\em Studies in Logic and the Foundations of Mathematics},
1000: chapter C.7, pages 739--782. North-Holland Publishing Company, 1977.
1001:
1002: \bibitem{Fabris-aadebug-97}
1003: A.~Aggoun, F.~Bueno, M.~Carro, P.~Deransart, M.~Fabris, W.~Drabent, G.~Ferrand,
1004: M.~Hermenegildo, C.~Lai, J.~Lloyd, J.~Ma{\l}uszy{\'n}ski, G.~Puebla, and
1005: A.~Tessier.
1006: \newblock {CP Debugging Needs and Tools}.
1007: \newblock In Mariam Kamkar, editor, {\em {International Workshop on Automated
1008: Debugging}}, volume~2 of {\em {Link\"oping Electronic Articles in Computer
1009: and Information Science}}, 1997.
1010:
1011: \bibitem{Apt-tcs-99}
1012: Krzysztof~R. Apt.
1013: \newblock {The Essence of Constraint Propagation}.
1014: \newblock {\em Theorical Computer Science}, 221(1--2):179--210, 1999.
1015:
1016: \bibitem{Benhamou-alp-96}
1017: Fr\'ed\'eric Benhamou.
1018: \newblock {Heterogeneous Constraint Solving}.
1019: \newblock In Michael Hanus and Mario Rofr\'{\i}guez-Artalejo, editors, {\em
1020: International Conference on Algebraic and Logic Programming}, volume 1139 of
1021: {\em Lecture Notes in Computer Science}, pages 62--76. Springer-Verlag, 1996.
1022:
1023: \bibitem{CodDia-jlp-96}
1024: Philippe Codognet and Daniel Diaz.
1025: \newblock {Compiling Constraints in {\tt clp(FD)}}.
1026: \newblock {\em Journal of Logic Programming}, 27(3):185--226, 1996.
1027:
1028: \bibitem{CouCou-saipl-77}
1029: Patrick Cousot and Radhia Cousot.
1030: \newblock {Automatic synthesis of optimal invariant assertions mathematical
1031: foundation}.
1032: \newblock In {\em Symposium on Artificial Intelligence and Programming
1033: Languages}, volume 12(8) of {\em ACM SIGPLAN Not.}, pages 1--12, 1977.
1034:
1035: \bibitem{Ferrand-aadebug-93}
1036: G\'erard Ferrand.
1037: \newblock {The Notions of Symptom and Error in Declarative Diagnosis of Logic
1038: Programs}.
1039: \newblock In Peter~A. Fritzson, editor, {\em Automated and Algorithmic
1040: Debugging}, volume 749 of {\em Lecture Notes in Computer Science}, pages
1041: 40--57. Springer-Verlag, 1993.
1042:
1043: \bibitem{Tessier-aadebug-97}
1044: G\'erard Ferrand and Alexandre Tessier.
1045: \newblock {Positive and Negative Diagnosis for Constraint Logic Programs in
1046: terms of Proof Skeletons}.
1047: \newblock In Mariam Kamkar, editor, {\em {International Workshop on Automated
1048: Debugging}}, volume~2 of {\em {Link\"oping Electronic Articles in Computer
1049: and Information Science}}, 1997.
1050:
1051: \bibitem{GouBen-ase-99}
1052: Fr\'ed\'eric Goualard and Fr\'ed\'eric Benhamou.
1053: \newblock A visualization tool for constraint program debugging.
1054: \newblock In {\em International Conference on Automated Software Engineering},
1055: pages 110--117. IEEE Computer Society Press, 1999.
1056:
1057: \bibitem{GueJusPri-ejor-00}
1058: Christelle Gu\'eret, Narendra Jussien, and Christian Prins.
1059: \newblock {Using intelligent backtracking to improve branch and bound methods:
1060: an application to Open-Shop problems}.
1061: \newblock {\em European Journal of Operational Research}, 2000.
1062:
1063: \bibitem{Jussien-phd-97}
1064: Narendra Jussien.
1065: \newblock {\em {Relaxation de Contraintes pour les Probl\`emes dynamiques}}.
1066: \newblock PhD thesis, Universit\'e de Rennes 1, 1997.
1067:
1068: \bibitem{MarStu-book-98}
1069: Kim Marriott and Peter~J. Stuckey.
1070: \newblock {\em {Programming with Constraints: An Introduction}}.
1071: \newblock MIT Press, 1998.
1072:
1073: \bibitem{Meier-cp-1995}
1074: Micha Meier.
1075: \newblock Debugging constraint programs.
1076: \newblock In Ugo Montanari and Francesca Rossi, editors, {\em International
1077: Conference on Principles and Practice of Constraint Programming}, volume 976
1078: of {\em Lecture Notes in Computer Science}, pages 204--221. Springer-Verlag,
1079: 1995.
1080:
1081: \bibitem{MonRos-ai-91}
1082: Ugo Montanari and Francesca Rossi.
1083: \newblock Constraint relaxation may be perfect.
1084: \newblock {\em Artificial Intelligence}, 48:143--170, 1991.
1085:
1086: \bibitem{Shapiro-phd-82}
1087: Ehud~Y. Shapiro.
1088: \newblock {\em {Algorithmic Program Debugging}}.
1089: \newblock ACM Distinguished Dissertation. MIT Press, 1982.
1090:
1091: \bibitem{Tessier-discipl-00}
1092: Alexandre Tessier and G\'erard Ferrand.
1093: \newblock {Declarative Diagnosis in the CLP scheme}.
1094: \newblock In Pierre Deransart, Manuel Hermenegildo, and Jan Ma{\l}uszy{\'n}ski,
1095: editors, {\em {Analysis and Visualisation Tools for Constraint Programming}},
1096: chapter~5. Springer-Verlag, 2000.
1097: \newblock (to appear).
1098:
1099: \bibitem{Tsang-book-93}
1100: Edward Tsang.
1101: \newblock {\em Foundations of Constraint Satisfaction}.
1102: \newblock Academic Press, 1993.
1103:
1104: \bibitem{VanEmden-misc-95}
1105: Maarten~H. {Van Emden}.
1106: \newblock {Value Constraints in the CLP scheme}.
1107: \newblock In {\em International Logic Programming Symposium, post-conference
1108: workshop on Interval Constraints}, 1995.
1109:
1110: \bibitem{VanHentenryck-book-89}
1111: Pascal {Van Hentenryck}.
1112: \newblock {\em {Constraint Satisfaction in Logic Programming}}.
1113: \newblock Logic Programming. MIT Press, 1989.
1114:
1115: \bibitem{DevSarVan-draft-91}
1116: Pascal {Van Hentenryck}, Vijay Saraswat, and Yves Deville.
1117: \newblock {Constraint Processing in {\tt cc(FD)}}.
1118: \newblock Draft, 1991.
1119:
1120: \end{thebibliography}
1121: \end{document}
1122:
1123: