1: \documentclass{acm_proc_article-sp}
2:
3: \sloppy
4:
5:
6: %% definitions needed for ACM proceedings
7: \newtheorem{theorem}{Theorem}
8: \newtheorem{lemma}{Lemma}
9: \newdef{definition}{Definition}
10: \newdef{note}{Note}
11:
12: \begin{document}
13:
14: %% ACM declarations
15: \conferenceinfo{SAC}{'03 Melbourne, Florida, USA}
16: \CopyrightYear{2003}
17:
18: \title{Schedulers for Rule-Based Constraint Programming}
19:
20: \numberofauthors{2}
21:
22: \author{
23: \alignauthor Krzysztof R.~Apt%
24: \titlenote{Currently on leave at School of Computing, National University of
25: Singapore}\\
26: \affaddr{CWI, P.O. Box 94079}\\
27: \affaddr{1090 GB Amsterdam, the Netherlands}\\
28: \affaddr{and University of Amsterdam, the Netherlands}\\
29: \email{K.R.Apt@cwi.nl}
30: \alignauthor Sebastian Brand\\
31: \affaddr{CWI, P.O. Box 94079}\\
32: \affaddr{1090 GB Amsterdam, the Netherlands}\\
33: \email{S.Brand@cwi.nl}
34: }
35:
36: \maketitle
37:
38:
39: \newcommand{\friends} {\ensuremath{\mathit{friends}}}
40: \newcommand{\obviated} {\ensuremath{\mathit{obviated}}}
41: \newcommand{\update} {\ensuremath{\mathit{update}}}
42: \newcommand{\holds} {\ensuremath{\mathit{Holds}}}
43: \newcommand{\nholds} {\ensuremath{\neg\mathit{Holds}}}
44:
45: \newcommand{\GIclassalgo}[1] {\texttt{#1}}
46: \newcommand{\GIalgo} {\GIclassalgo{GI}}
47: \newcommand{\RGIalgo} {\GIclassalgo{RGI}}
48: \newcommand{\Ralgo} {\GIclassalgo{R}}
49: \newcommand{\FOalgo} {\GIclassalgo{F~\&~O}}
50: \newlength{\figalgogap}\setlength{\figalgogap}{-4.1ex}
51:
52: \newcommand{\eclipse} {ECL$^i$PS$^e$}
53:
54: \newcommand{\ra}{\mbox{$\:\rightarrow\:$}}
55: \newcommand{\C}[1]{\mbox{$\{{#1}\}$}}
56: \newcommand{\LL}{\mbox{$\ldots$}}
57: \newcommand{\po}{\mbox{$\ \sqsubseteq\ $}}
58: \newcommand{\HB}{\hfill{$\Box$}}
59: \newcommand{\A}{\mbox{$\ \wedge\ $}}
60: \newcommand{\fa}{\mbox{$\forall$}}
61: \newcommand{\ES}{\mbox{$\emptyset$}}
62: \newcommand{\Or}{\mbox{$\ \vee\ $}}
63: \newcommand{\sse}{\mbox{$\:\subseteq\:$}}
64: \newcommand{\te}{\mbox{$\exists$}}
65: \newcommand{\p}[2]{\langle #1 \ ; \ #2 \rangle}
66:
67:
68:
69: \def\ts{\textstyle}
70: \def\smallromani{\renewcommand{\theenumi}{\roman{enumi}}
71: \renewcommand{\labelenumi}{(\theenumi)}}
72: \def\smallromaniprime{\renewcommand{\theenumi}{\roman{enumi}\mbox{$'$}}
73: \renewcommand{\labelenumi}{(\theenumi)}}
74: \def\smallromanir{\renewcommand{\theenumi}{\roman{enumi}}
75: \renewcommand{\labelenumi}{\theenumi)}}
76: \def\smallromanii{\renewcommand{\theenumii}{\roman{enumii}}
77: \renewcommand{\labelenumii}{(\theenumii)}}
78: \def\parentarabici{\renewcommand{\theenumi}{\arabic{enumi}}
79: \renewcommand{\labelenumi}{(\theenumi)}}
80: \def\parentarabicii{\renewcommand{\theenumii}{\arabic{enumii}}
81: \renewcommand{\labelenumii}{(\theenumii)}}
82: \def\eqnum{\renewcommand{\theequation}{\arabic{equation}}
83: \renewcommand{\labelequation}{(\theequation)}}
84:
85: \def\parentalphi{\renewcommand{\theenumi}{\alph{enumi}}
86: \renewcommand{\labelenumi}{(\theenumi)}}
87:
88:
89:
90: \begin{abstract}
91: We study here schedulers for a class of rules that naturally arise
92: in the context of rule-based constraint programming. We
93: systematically derive a scheduler for them from a generic iteration
94: algorithm of Apt \cite{Apt00a}. We apply this study to so-called
95: membership rules of Apt and Monfroy \cite{AM01}. This leads to an
96: implementation that yields for these rules a considerably better
97: performance than their execution as standard \texttt{CHR} rules.
98: \end{abstract}
99:
100: \keywords{Constraint propagation, rule-based programming}
101:
102: \section{Introduction}
103: \label{sec:introduction}
104:
105:
106: In this paper we are concerned with schedulers for a class of rules
107: that naturally arise in the context of constraint programming
108: represented by means of rule-based programming. An example
109: of such rules are so-called \emph{membership rules}, introduced in Apt
110: and Monfroy \cite{AM01}.
111: Their relevance stems from the following observations there made for
112: constraint satisfaction problems (CSP's) with finite domains:
113: \begin{itemize}
114:
115: \item constraint propagation can be naturally achieved by repeated
116: application of the membership rules;
117:
118: \item in particular the notion of hyper-arc consistency can be characterized in
119: terms of the membership rules;
120:
121: \item for constraints explicitly defined on small finite domains all
122: valid membership rules can be automatically generated (For a most
123: recent reference on the subject of such an automatic rule generation
124: see Abdennadher and Rigotti \cite{AR01}.);
125:
126: \item many rules of the \texttt{CHR} language (Constraint Handling
127: Rules) of Fr\"{u}hwirth \cite{FruehwirthJLP98} that are used
128: in specific constraint solvers are in fact membership rules. Now,
129: in the logic programming approach to constraint programming
130: \texttt{CHR} is the language of choice to write constraint solvers.
131: \end{itemize}
132:
133: In the resulting approach to constraint programming the computation
134: process is limited to a repeated application of the rules intertwined
135: with splitting (labeling).
136: So the viability of this approach crucially depends on the
137: availability of efficient schedulers for such rules. This motivates
138: the work here reported. We provide an abstract framework for such
139: schedulers and use it as a basis for an implementation.
140:
141: The abstract framework is based on an appropriate modification of the
142: generic approach to constraint propagation algorithms introduced in
143: Apt \cite{Apt99b} and Apt \cite{Apt00a}. In this framework one
144: proceeds in two steps. First, a generic iteration algorithm on
145: partial orderings is introduced and proved correct in an abstract
146: setting. Then it is instantiated with specific partial orderings and
147: functions to obtain specific constraint propagation algorithms.
148: In this paper, as in Apt \cite{Apt00a},
149: we take into account information
150: about the scheduled functions. Here we consider functions in the form
151: of the rules $b \ra g$, where $b$ and $g$ satisfy a number of natural
152: conditions. We call such functions \emph{good rules}. The relevant
153: observation is that membership rules are good rules. Then we propose
154: a specific scheduler in the form of an algorithm {\Ralgo},
155: appropriate for good rules.
156:
157: The implementation is provided as an \eclipse{} program that accepts
158: as input a set of membership rules and constructs an \eclipse{}
159: program that is the instantiation of the {\Ralgo} algorithm for this
160: set of rules. As membership rules can be naturally represented as
161: \texttt{CHR} propagation rules, one can assess this implementation by
162: comparing it with the performance of the standard implementation of
163: membership rules in the \texttt{CHR} language. We found by means of
164: various benchmarks that our implementation is considerably faster than
165: \texttt{CHR}.
166:
167:
168: \texttt{CHR} is available in a number of languages including the
169: \eclipse{} and the Sicstus Prolog systems.
170: In both cases \texttt{CHR} programs are compiled into the source language.
171: There is also a recent implementation in Java, see \cite{AKSS01}.
172: A great deal of effort was spent on implementing \texttt{CHR}
173: efficiently. For an account of the most recent implementation see
174: Holzbaur et al. \cite{Holzbaur:2001:OCC}. Since, as already
175: mentioned above, many \texttt{CHR} rules are membership rules,
176: our approach provides a better implementation of a subset of \texttt{CHR}.
177: While being stricly smaller than full \texttt{CHR},
178: the actual class of relevant rules is wider than the class of membership rules.
179: The essential properties, such as monotonicity of condition and conclusion,
180: are enjoyed by many rules that describe constraint propagation.
181: This, hopefully, may lead to new insights into design and
182: implementation of languages appropriate for writing constraint
183: solvers.
184:
185: It is important to stress that the discussed implementation was obtained by
186: starting from ``first principles'' in the form of a generic iteration
187: algorithm on an arbitrary partial ordering. This shows the practical
188: benefits of studying the constraint propagation process on an abstract
189: level.
190:
191: \section{Revisions of the Generic Iteration Algorithm}
192: \label{sec:revised}
193:
194: \subsection{The Original Algorithm}
195:
196: Let us begin our presentation with recalling the generic algorithm of
197: Apt \cite{Apt00a}. We slightly adjust the presentation to our purposes
198: by assuming that the considered partial ordering also has the
199: greatest element $\top$.
200:
201: So we consider a partial ordering $(D, \po )$ with the
202: least element $\bot$ and the greatest element $\top$,
203: and a set of functions $F := \C{f_1, \LL , f_k}$
204: on $D$. We are interested in functions that satisfy
205: the following two properties.
206: \begin{definition}
207: \mbox{}\\[-5mm]
208:
209: \begin{itemize}
210: \item $f$ is called {\em inflationary\/}
211: if $x \po f(x)$ for all $x$.
212:
213: \item $f$ is called {\em monotonic\/}
214: if $x \po y$ implies
215: $f(x) \po f(y)$ \\for all $x, y$.
216: \HB
217: \end{itemize}
218: \end{definition}
219:
220: Then the following algorithm is used to compute the least common
221: fixpoint of the functions from $F$.
222:
223: \begin{figure}[ht]
224: \begin{tabbing}
225: \= $d := \bot$; \\
226: \> $G := F$; \\
227: \> {\bf while} $G \neq \ES$ {\bf and} $d \neq \top$ {\bf do} \\
228: \> \quad choose $g \in G$; \\
229: \> \quad $G := G - \C{g}$; \\
230: \> \quad $G := G \cup \update(G,g,d)$; \\
231: \> \quad $d := g(d)$ \\
232: \> {\bf end}
233: \end{tabbing}
234: \vspace{\figalgogap}
235: \caption{Generic Iteration Algorithm ({\GIalgo})}
236: \label{gialgo}
237: \end{figure}
238:
239: where for all $G,g,d$ the set of functions
240: $\update(G,g,d)$ from $F$ is such that
241: %
242: \begin{description}
243: \item[{\bf A}] $\C{f \in F - G \mid f(d) = d \A f(g(d)) \neq g(d)} \sse
244: \update(G,g,d)$,
245:
246: \item[{\bf B}] $g(d) = d$ implies that $\update(G,g,d) = \ES$,
247:
248: \item[{\bf C}] $g(g(d)) \neq g(d)$ implies that $g \in \update(G,g,d)$.
249: \end{description}
250:
251: Intuitively, assumption {\bf A} states that $\update(G,g,d)$
252: contains at least all the functions from $F - G$ for which the ``old value'',
253: $d$, is a fixpoint but the ``new value'', $g(d)$, is not. So at each
254: loop iteration such functions are added to the set $G$. In turn,
255: assumption {\bf B} states that no functions are added to $G$ in case
256: the value of $d$ did not change. Assumption {\bf C} provides
257: information when $g$ is to be added back to $G$ as this information is
258: not provided by {\bf A}.
259: On the whole, the idea is to keep in $G$ at least all functions $f$
260: for which the current value of $d$ is not a fixpoint.
261:
262: The use of the condition $d \neq \top$, absent in the original
263: presentation, allows us to leave the \textbf{while} loop earlier.
264: Our interest in the {\GIalgo} algorithm is clarified by the
265: following result.
266:
267: \begin{theorem}[Correctness] \label{thm:GI}
268: Suppose that all functions in $F$ are inflationary and monotonic and
269: that $(D, \po)$ is finite and has the least element $\bot$ and the
270: greatest element $\top$. Then every execution of the {\GIalgo}
271: algorithm terminates and computes in $d$ the least common fixpoint
272: of the functions from $F$.
273: \end{theorem}
274: %
275: \begin{proof}
276: (Sketch). The following statement is an invariant of the \textbf{while}
277: loop of the algorithm:
278: \[
279: (\fa f \in F - G \ f(d) = d) \A (\fa f \in F \ f(\top) = \top).
280: \]
281: This implies that the algorithm computes in $d$ a common fixpoint
282: of the functions from $F$. The fact that this is the least common
283: fixpoint follows from the assumption that all functions are monotonic.
284:
285: In turn, termination is established by considering
286: the lexicographic ordering of the strict partial orderings
287: $(D, \sqsupset)$ and $({\cal N}, <)$,
288: defined on the elements of $D \times {\cal N}$ by
289: \[
290: (d_1, n_1) <_{lex} (d_2, n_2)\ {\rm iff} \ d_1 \sqsupset d_2
291: \ {\rm or}\ ( d_1 = d_2 \ {\rm and}\ n_1 < n_2).
292: \]
293: Then with each {\bf while} loop iteration of the algorithm the pair
294: $(d, card \: G)$, where $card \: G$ is the cardinality of the set $G$,
295: strictly decreases in the ordering $<_{lex}$.
296: \end{proof}
297:
298: \subsection{Removing Functions}
299:
300: We now revise the {\GIalgo} algorithm by modifying dynamically the set
301: of functions that are being scheduled. The idea is that, whenever
302: possible, we remove functions from the set $F$. This will allow us to
303: exit the loop earlier which speeds up the execution of the algorithm.
304:
305: To realize this idea we proceed as follows.
306: First, we introduce the following property that will be satisfied by
307: the considered functions.
308:
309: \begin{definition}
310: Suppose $d \in D$ and $f \in F$.
311: We say that $f$ is {\em stable above $d$\/}
312: if $d \po e$ implies $f(e) = e$. We then say that $f$ is {\em stable}
313: if it is stable above $f(d)$, for all $d$.
314: \HB
315: \end{definition}
316:
317: That is, $f$ is stable if for all $d$ and $e$, $f(d) \po e$ implies
318: $f(e) = e$. So stability implies idempotence, which means that
319: $f(f(d)) = f(d)$, for all $d$.
320: Moreover, if $d$ and $f(d)$ are comparable
321: for all $d$, then stability implies inflationarity.
322: Indeed, if d \po $f(d)$, then the claim holds vacuously.
323: And if $f(d) \po d$, then by stability $f(d) = d$.
324:
325: Next, we assume that for each function $g \in F$ and each element $d
326: \in D$, two lists of functions from $F$ are given, $\friends(g,d)$ and
327: $\obviated(g,d)$ that satisfy the following condition
328: \begin{eqnarray}
329: && \fa d \: \fa e \sqsupseteq g \circ g_1 \circ \LL \circ g_k(d)%
330: \nonumber\\&&\quad
331: \fa f \in \friends(g,d) \cup \obviated(g,d) \: (f(e) = e)
332: \hspace{3em}
333: \label{eq:stable}
334: \end{eqnarray}
335: where $\friends(g,d) = [g_1, \LL, g_k]$.
336:
337: That is, for all $d$, each function $f$ in $\friends(g,d) \cup \obviated(g,d)$
338: is stable
339: above $g \circ g_1 \circ \LL \circ g_k(d)$.
340:
341: Now, we modify the {\GIalgo}
342: algorithm in such a way that each application of $g$ to $d$ will be
343: immediately followed by the applications of all functions from
344: $\friends(g,d)$ and by a removal of the functions from $\friends(g,d)$
345: and from $\obviated(g,d)$ both from $F$ and $G$.
346: This modified algorithm is shown in Fig.~\ref{rgialgo}.
347: To keep the notation uniform we identified at some places the
348: lists $\friends(g,d)$ and $\obviated(g,d)$ with the sets.
349:
350: \begin{figure}[ht]
351: \begin{tabbing}
352: \= $d := \bot$; \\
353: \> $F_0 := F$; \\
354: \> $G := F$; \\
355: \> {\bf while} $G \neq \ES$ {\bf and} $d \neq \top$ {\bf do} \\
356: \> \quad choose $g \in G$; \\
357: \> \quad $G := G - \C{g}$; \\
358: \> \quad $F := F - (\friends(g,d) \cup \obviated(g,d))$; \\
359: \> \quad $G := G - (\friends(g,d) \cup \obviated(g,d))$; \\
360: \> \quad $G$ \= $:= G \cup \update(G,h,d)$, \\
361: \> \> where $h = g \circ g_1 \circ \LL \circ g_k$ and $\friends(g,d)
362: = [g_1, \LL, g_k]$; \\
363: \> \quad $d :=h(d)$ \\
364: \> {\bf end}
365: \end{tabbing}
366: \vspace{\figalgogap}
367: \caption{Revised Generic Iteration Algorithm ({\RGIalgo})}
368: \label{rgialgo}
369: \end{figure}
370:
371: The following result then shows correctness of this algorithm.
372:
373: \begin{theorem}
374: Suppose that all functions in $F$ are inflationary and monotonic and
375: that $(D, \po)$ is finite and has the least element $\bot$ and the
376: greatest element $\top$. Additionally, suppose that for each
377: function $g \in F$ and $d \in D$ two lists of functions from $F$ are
378: given, $\friends(g,d)$ and $\obviated(g,d)$ such that condition
379: (\ref{eq:stable}) holds.
380:
381: Then the Correctness Theorem \ref{thm:GI} holds with the {\GIalgo} algorithm
382: replaced by the {\RGIalgo} algorithm.
383: \end{theorem}
384: %
385: \begin{proof}
386: In view of condition (\ref{eq:stable}) the following statement is an
387: invariant of the \textbf{while} loop:
388: \begin{eqnarray}
389: &\fa f \in F - G \: (f(d) = d) \;\A\; \fa f \in F \ (f(\top) = \top) \;\A%
390: \nonumber\\
391: &\fa f \in F_0 - F \ \fa e \sqsupseteq d \ (f(e) = e).
392: \label{eq:del}
393: \end{eqnarray}
394: So upon termination of the algorithm the conjunction of this invariant with
395: the negation of the loop condition, i.e.,
396: \[
397: G = \ES \;\Or\; d = \top
398: \]
399: holds, which implies that $\fa f \in F_0 \: (f(d) = d)$.
400:
401: The rest of the proof is the same.
402: \end{proof}
403:
404: In the next section we shall focus on functions that are in a special
405: form. For these functions we shall show how to construct specific lists
406: $\friends(g,d)$ and $\obviated(g,d)$.
407:
408: \subsection{Functions in the Form of Rules}
409:
410: In what follows we consider the situation when the scheduled functions
411: are of a specific form $b \ra g$, where $b$ is a \emph{condition} and
412: $g$ a function, that we call a \emph{body}. We call such functions
413: \emph{rules}.
414:
415: First, we explain how rules are applied. Given an element $d$ of $D$,
416: a condition $b$ evaluates in $d$ to either true or false,
417: denoted $\holds(b,d)$ and $\nholds(b,d)$, resp.
418:
419:
420: Given a rule $b \ra g$ we define then its application as follows:
421: \[
422: (b \ra g)(d) :=
423: \left\{
424: \begin{array}{ll}
425: g(d) & \mbox{if } \holds(b,d) \\
426: d & \mbox{if } \nholds(b,d) \enspace.
427: \end{array}
428: \right.
429: \]
430:
431: The rules introduced in the next section will be of a specific type.
432:
433: \begin{definition}
434: Consider a partial ordering $(D, \po )$.
435: \begin{itemize}
436:
437: \item We say that a condition $b$ is \emph{monotonic} if
438: $\holds(b,d)$ and $d \po e$ implies $\holds(b,e)$,
439: for all $d, e$.
440:
441: \item We say that a condition $b$ is \emph{precise} if
442: the least $d$ exists such that $\holds(b,d)$.
443: We call then $d$ the \emph{witness} for $b$.
444:
445: \item We call a rule $b \ra g$ \emph{good} if $b$ is monotonic and precise
446: and $g$ is stable.
447: \HB
448: \end{itemize}
449: \end{definition}
450:
451: When all rules are good, we can modify the {\RGIalgo} algorithm by
452: taking into account that an application of a rule is a two step
453: process: testing of the condition followed by a conditional
454: application of the body. This will allow us to construct the lists
455: $\friends(g,d)$ and $\obviated(g,d)$ before the execution of the
456: algorithm, without using the parameter $d$. Moreover, the list
457: $\friends(g)$ can be constructed in such a way that the conditions of
458: its rules do not need to evaluated at the moment they are applied, as
459: they will all hold. The details of a specific construction that we
460: shall use here will be given in a moment, once we identify the
461: condition that is crucial for the correctness.
462: This revision of the {\RGIalgo} algorithm is given in
463: Fig.~\ref{ralgo}.
464:
465: \begin{figure}[ht]
466: \begin{tabbing}
467: \= $d := \bot$; \\
468: \> $F_0 := F$; \\
469: \> $G := F$; \\
470: \> {\bf while} $G \neq \ES$ {\bf and} $d \neq \top$ {\bf do} \\
471: \> \quad choose $f \in G$; suppose $f$ is $b \ra g$; \\
472: \> \quad $G := G - \C{b \ra g}$; \\
473: \> \quad {\bf if} $\holds(b, d)$ {\bf then} \\
474: \> \quad \quad $F := F - (\friends(b \ra g) \cup \obviated(b \ra g))$; \\
475: \> \quad \quad $G := G - (\friends(b \ra g) \cup \obviated(b \ra g))$; \\
476: \> \quad \quad $G$ \= $:= G \cup \update(G,h,d)$, \\
477: \> \> where $h = g \circ g_1 \circ \LL \circ g_k$\\
478: \> \> and $\friends(b \ra g) = [b_1 \ra g_1, \LL, b_k \ra g_k]$;
479: \\
480: \> \quad \quad $d :=h(d)$ \\
481: \> \quad {\bf else} \\
482: \> \quad \quad {\bf if} $\forall e \sqsupseteq d \; \nholds(b, e)$ {\bf then}\\
483: \> \quad \quad \quad $F := F - \{ b \ra g \}$ \\
484: \> \quad \quad {\bf end} \\
485: \> \quad {\bf end} \\
486: \> {\bf end}
487: \end{tabbing}
488: \vspace{\figalgogap}
489: \caption{Rules Algorithm ({\Ralgo})}
490: \label{ralgo}
491: \end{figure}
492:
493:
494:
495: Again, we are interested in identifying conditions under which the
496: Correctness Theorem \ref{thm:GI} holds with the {\GIalgo} algorithm
497: replaced by the {\Ralgo} algorithm. To this end, given a rule $b \ra g$
498: in $F$ and $d \in D$, define as follows:
499:
500: $
501: \begin{array}{l}
502: \friends(b \ra g, d) :=
503: \left\{%
504: \begin{array}{ll}
505: \friends(b \ra g) & \mbox{if } \holds(b, d)\\{}
506: [ \ ] & \mbox{if } \nholds(b, d)
507: \end{array}%
508: \right.
509: \\\\
510: %
511: \obviated(b \ra g, d) :=
512: \left\{%
513: \begin{array}{ll}
514: \obviated(b \ra g) & \mbox{if } \holds(b, d)\\{}
515: [ b \ra g ] & \parbox{30mm}{if $\forall e \sqsupseteq d$\\\qquad\
516: $\nholds(b, e)$}\\{}
517: [ \ ] & \mbox{otherwise}
518: \end{array}%
519: \right.
520: \end{array}
521: $
522:
523: We now have the following counterpart of the Correctness Theorem~\ref{thm:GI}.
524: \begin{theorem}[Correctness] \label{thm:R}
525: Suppose that all functions in $F$ are good rules of the form $b \ra
526: g$, where $g$ is inflationary and monotonic, and that $(D, \po)$ is
527: finite and has the least element $\bot$ and the greatest element
528: $\top$. Further, assume that for each rule $b \ra g$ the lists
529: $\friends(b \ra g,d)$ and $\obviated(b \ra g,d)$ defined as above
530: satisfy condition~(\ref{eq:stable}) and the following condition:
531: \begin{eqnarray}
532: &\fa d (b' \ra g' \in \friends(b \ra g) \quad\A\quad \\%
533: &\holds(b, d) \ra \fa e \sqsupseteq g(d) \ \holds(b', e) \enspace.
534: \nonumber
535: \label{eq:friends}
536: \end{eqnarray}
537: Then the Correctness Theorem \ref{thm:GI} holds with the {\GIalgo}
538: algorithm replaced by the {\Ralgo}~algorithm.
539: \end{theorem}
540: \begin{proof}
541: It suffices to show that the {\Ralgo} algorithm is an instance of the
542: {\RGIalgo} algorithm.
543: On the account of condition (\ref{eq:friends}) and the fact that the
544: rule bodies are inflationary functions, $\holds(b, d)$
545: implies that
546: \[
547: ((b \ra g) \circ (b_1 \ra g_1) \circ \LL \circ (b_k \ra g_k))(d) = (g \circ g_1
548: \circ \LL \circ g_k)(d),
549: \]
550: where $\friends(b \ra g) = [b_1 \ra g_1, \LL, b_k \ra g_k]$.
551: This takes care of the situation when if $\holds(b, d)$.
552:
553: In turn, the definition of $\friends(b \ra g,d)$ and $\obviated(b \ra g,d)$
554: and assumption \textbf{B} take care of the situation when if $\nholds(b, d)$.
555: When the condition $b$ fails for all $e \sqsupseteq d$, then we can
556: conclude that for all such $e$ we have $(b \ra g)(e)=e$. This allows
557: us to remove at that point of the execution the rule $b \ra g$ from
558: the set $F$. This amounts to adding $b \ra g$ to the set
559: $\obviated(b \ra g, d)$ at runtime. Note that
560: condition~(\ref{eq:stable}) is then satisfied.
561: \end{proof}
562:
563: We now provide an explicit construction of the lists $\friends$ and
564: $\obviated$ for a rule $b \ra g$ in the form of the
565: algorithm in Fig.~\ref{foalgo}. $\mathtt{GI}(d)$ stands here for the {\GIalgo}
566: algorithm activated with $\bot$ replaced by $d$ and the considered set
567: of rules as the set of functions $F$.
568: Further, given an execution of $\mathtt{GI}(e)$,
569: we call here a rule $g$ \emph{relevant} if at some point $g(d) \neq d$ holds
570: after the ``choose $g \in G$'' action.
571:
572: \begin{figure}[ht]
573: \begin{tabbing}
574: \= $e := \mbox{witness of } b$;\\
575: \> $e := \mathtt{GI}(g(e))$; \\
576: \> $\friends(b \ra g) :=$ \=list of the relevant rules $h \in F$\\\>\> in the
577: execution of $\mathtt{GI}(g(e))$;\\
578: \> $\obviated(b \ra g) := [\ ]$; \\
579: \> {\bf for each} $(b' \ra g') \in F - \friends(b \ra g)$ {\bf do} \\
580: \> \quad {\bf if} $g'(e) = e$ {\bf or} $\fa e' \sqsupseteq e \ \nholds(b',
581: e')$ {\bf then} \\
582: \> \quad \quad $\obviated(b \ra g) := [b' \ra g' | \obviated(b \ra g)]$ \\
583: \> \quad {\bf end} \\
584: \> {\bf end}
585: \end{tabbing}
586: \vspace{\figalgogap}
587: \caption{Friends and Obviated Algorithm ({\FOalgo})}
588: \label{foalgo}
589: \end{figure}
590:
591: Note that $b \ra g \not\in \friends(b \ra g)$
592: since $b \ra g$ is a good rule,
593: while \mbox{$b \ra g \in \obviated(b \ra g)$} since
594: by the stability of~$g$ $g(e) = e$ holds.
595:
596:
597: The following observation now shows the adequacy of the {\FOalgo} algorithm
598: for our purposes.
599:
600: \begin{lemma}
601: Upon termination of the {\FOalgo} algorithm
602: conditions (\ref{eq:stable}) and (\ref{eq:friends}) hold,
603: where the lists $\friends(b \ra g,d)$ and $\obviated(b \ra g,d)$
604: are defined as before Theorem \ref{thm:R}.
605: \HB
606: \end{lemma}
607:
608: Let us summarize now the findings of this section that culminated in
609: the {\Ralgo} algorithm. Assume that all functions are of the form of
610: the rules satisfying the conditions of the Correctness Theorem
611: \ref{thm:R}. Then in the {\Ralgo} algorithm, each time the evaluation
612: of the condition $b$ of the selected rule $b \ra g$ succeeds,
613:
614: \begin{itemize}
615: \item the rules in the list $\friends(b \ra g)$ are applied
616: directly without testing the value of their conditions,
617:
618: \item the rules in $\friends(b \ra g) \cup \obviated(b \ra g)$
619: are permanently removed from the current set of functions $G$
620: and from $F$.
621: \end{itemize}
622:
623: \subsection{Recomputing of the Least Fixpoints}
624:
625: Another important optimization takes place when the {\Ralgo} algorithm is
626: repeatedly applied to compute the least fixpoint. More specifically,
627: consider the following sequence of actions:
628: \begin{itemize}
629: \item we compute the least common fixpoint $d$ of the functions from $F$,
630:
631: \item we move from $d$ to an element $e$ such that $d \po e$,
632:
633: \item we compute the least common fixpoint above $e$ of
634: the functions from $F$.
635: \end{itemize}
636: Such a sequence of actions typically arises in the framework of CSP's,
637: further studied in Section
638: \ref{sec:concrete}. The computation of the least common fixpoint $d$
639: of the functions from $F$ corresponds there to the constraint
640: propagation process for a constraint $C$. The moving from $d$ to
641: $e$ such that $d \po e$ corresponds to splitting or constraint
642: propagation involving another constraint, and the computation of the
643: least common fixpoint above $e$ of the functions from $F$ corresponds
644: to another round of constraint propagation for $C$.
645:
646: Suppose now that we computed the least common fixpoint $d$ of the
647: functions from $F$ using the {\RGIalgo} algorithm or its modification
648: {\Ralgo} for the rules. During its execution we permanently removed
649: some functions from the set $F$. Then these
650: functions are not needed for computing the least common fixpoint above
651: $e$ of the functions from $F$. The precise statement is provided in
652: the following simple, yet crucial, theorem.
653:
654: \newcommand{\Ffin} {\ensuremath{F_{\mathit{fin}}}}
655: \begin{theorem} \label{thm:repeated}
656: Suppose that all functions in $F$ are inflationary and monotonic and
657: that $(D, \po)$ is finite. Suppose that the least common fixpoint
658: $d_0$ of the functions from $F$ is computed by means of the
659: {\RGIalgo} algorithm or the {\Ralgo} algorithm. Let \Ffin\ be the
660: final value of the variable $F$ upon termination of the {\RGIalgo}
661: algorithm or of the {\Ralgo} algorithm.
662:
663: Suppose now that $d_0 \po e$. Then the least common fixpoint $e_0$ above $e$
664: of the functions from $F$ coincides with the least common fixpoint
665: above $e$ of the functions from \Ffin.
666: \end{theorem}
667: %
668: \begin{proof}
669: Take a common fixpoint $e_1$ of the functions from \Ffin\
670: such that $e \po e_1$. It suffices to prove that $e_1$ is common
671: fixpoint of the functions from $F$. So take $f \in F - \Ffin$.
672: Since condition (\ref{eq:del}) is an invariant of the main
673: \textbf{while} loop of the {\RGIalgo} algorithm and of the {\Ralgo}
674: algorithm, it holds upon termination and consequently $f$ is stable
675: above $d_0$. But $d_0 \po e$ and $e \po e_1$, so we conclude that
676: $f(e_1) = e_1$.
677: \end{proof}
678:
679: Intuitively, this result means that if after splitting we relaunch the
680: same constraint propagation process we can disregard the removed
681: functions.
682:
683: In the next section we instantiate the {\Ralgo} algorithm by a set
684: of rules that naturally arise in the context of constraint
685: satisfaction problems with finite domains. In Section
686: \ref{sec:implementation} we assess the practical impact of the
687: discussed optimizations.
688: \section{Concrete Framework}
689: \label{sec:concrete}
690:
691: We now proceed with the main topic of this paper, the schedulers for
692: the rules that naturally arise in the context of constraint
693: satisfaction problems. First we recall briefly the necessary
694: background on the constraint satisfaction problems.
695:
696: \subsection{Constraint Satisfaction Problems}
697:
698: Consider a sequence of variables $X := x_1, \LL, x_n$
699: where $n \geq 0$, with respective domains $D_1, \LL, D_n$
700: associated with them. So each variable $x_i$ ranges over the domain
701: $D_i$. By a {\em constraint} $C$ on $X$ we mean a subset of $D_1
702: \times \LL \times D_n$.
703: Given an element $d := d_1, \LL, d_n$ of $D_1 \times \LL \times D_n$
704: and a subsequence $Y := x_{i_1}, \LL, x_{i_\ell}$ of $X$ we denote by
705: $d[Y]$ the sequence $d_{i_1}, \LL, d_{i_{\ell}}$. In particular, for a
706: variable $x_i$ from $X$, $d[x_i]$ denotes $d_i$.
707:
708: Recall that a {\em constraint satisfaction problem}, in short CSP, consists of
709: a finite sequence of variables $X$ with respective domains ${\cal
710: D}$, together with a finite set $\cal C$ of constraints, each on a
711: subsequence of $X$. We write it as
712: \mbox{$\p{{\cal C}}{x_1 \in D_1, \LL, x_n \in D_n}$},
713: where $X := x_1, \LL, x_n$ and ${\cal D} :=
714: D_1, \LL, D_n$.
715:
716: By a {\em solution\/} to $\p{{\cal C}}{x_1 \in D_1, \LL, x_n \in D_n}$
717: we mean an element $d \in D_1 \times \LL \times D_n$ such that for
718: each constraint $C \in {\cal C}$ on a sequence of variables $X$ we
719: have $d[X] \in C$. We call a CSP {\em consistent\/} if it has a
720: solution. Two CSP's with the same sequence of variables are called
721: {\em equivalent\/} if they have the same set of solutions.
722:
723: \subsection{Partial Orderings}
724:
725: With each CSP ${\cal P} := \p{{\cal C}}{x_1 \in D_1, \LL, x_n \in
726: D_n}$ we associate now a specific partial ordering. Initially we
727: take the Cartesian product of the partial orderings
728: \mbox{$({\cal P}(D_1), \supseteq ), \LL, ({\cal P}(D_n), \supseteq)$}.
729: So this ordering is of the form
730: \[
731: ({\cal P}(D_1) \times \LL \times {\cal P}(D_n), \supseteq)
732: \]
733: where we interpret $\supseteq$ as the
734: the Cartesian product of the reversed subset ordering.
735: The elements of this partial ordering are sequences
736: $(E_1, \LL, E_n)$ of respective subsets of $(D_1, \LL, D_n)$ ordered
737: by the componentwise reversed subset ordering. Note that in this
738: ordering $(D_1, \LL, D_n)$ is the least element while
739: \[
740: \underbrace{(\ES, \LL, \ES)}_{\mbox{$n$ times}}
741: \]
742: is the greatest element. However, we would like to identify with the
743: greatest element all sequences that contain as an element the empty
744: set. So we divide the above partial ordering by the equivalence
745: relation $R_{\ES}$ according to which
746: %
747: \begin{eqnarray*}
748: &(E_1, \LL, E_n) \ R_{\ES} \ (F_1, \LL, F_n) \qquad\mbox{iff}\\
749: &(E_1, \LL, E_n) = (F_1, \LL, F_n)
750: \mbox{ or } (\te i \: E_i = \ES
751: \mbox{ and } \te j \: F_j = \ES).
752: \end{eqnarray*}
753: It is straightforward to see that $R_{\ES}$ is indeed an equivalence relation.
754:
755: In the resulting quotient ordering there are two types of elements: the
756: sequences $(E_1, \LL, E_n)$ that do not contain the empty set as an
757: element, that we continue to present in the usual way with the
758: understanding that now each of the listed sets is non-empty, and one
759: ``special'' element equal to the equivalence class consisting of all
760: sequences that contain the empty set as an element. This equivalence
761: class is the greatest element in the resulting ordering, so we denote
762: it by $\top$. In what follows we denote this partial ordering by
763: $(D_{\cal P}, \po )$.
764:
765: \subsection{Membership Rules}
766:
767: Fix now a specific CSP ${\cal P} := \p{{\cal C}}{x_1 \in D_1, \LL, x_n \in D_n}$
768: with finite domains. We now recall the
769: rules introduced in Apt and Monfroy \cite{AM01}.%
770: %
771: \footnote
772: {In our presentation we slightly relax the original syntactic restrictions.}
773: %
774: They are called {\em membership rules} and are of the form
775: \[
776: y_1 \in S_1, \LL, y_k \in S_k \ra z_1 \neq a_1, \LL, z_m \neq a_m,
777: \]
778: where
779: %
780: \begin{itemize}
781: \item $y_1, \LL, y_k$ are pairwise different variables from the set $\C{x_1,
782: \LL, x_n}$
783: and $S_1, \LL, S_k$ are subsets of the respective variable domains,
784:
785: \item $z_1, \LL, z_m$ are variables from the set $\C{x_1, \LL, x_n}$
786: and $a_1, \LL, a_m$ are elements of the respective variable domains.
787: %
788: \end{itemize}
789: Note that we do not assume that the variables $z_1, \LL, z_m$
790: are pairwise different.
791:
792: The computational interpretation of such a rule is:
793: %
794: \begin{quote}
795: if for $i \in [1..k]$ the current domain of the variable $y_i$
796: is included in the set $S_i$, then
797: for $j \in [1..m]$ remove the element $a_i$ from the
798: domain of $z_i$.
799: \end{quote}
800: %
801: When each set $S_i$ is a singleton, we call a membership rule an \emph{equality
802: rule}.
803: %
804:
805: Let us reformulate this interpretation so that it fits the framework
806: considered in the previous section.
807: To this end we need to clarify how to evaluate a condition, and how to
808: interpret a conclusion.
809: %
810: We start with the first item.
811: %
812: \begin{definition}
813: Given a variable $y$ with the domain $D_y$ and $E, S \supseteq D_y$ we define
814: \begin{tabbing}
815: \qquad $\holds(y \in S, E)$ \quad iff \quad $E \sse S$,
816: \end{tabbing}
817: and extend the definition to the elements of the considered ordering
818: $(D_{\cal P}, \po )$ by putting
819: \begin{tabbing}
820: \qquad $\holds(y \in S, (E_1, \LL, E_n))$ \quad iff \quad $E_k \sse S$,\\
821: \qquad\qquad\qquad where we assumed that $y$ is $x_k$,
822: \\\\
823: \qquad $\holds(y \in S, \top)$.
824: \end{tabbing}
825:
826: Then we interpret a sequence $y_1 \in S_1, \LL, y_k \in S_k$ of conditions as a
827: conjunction,
828: so by putting
829: \begin{tabbing}
830: \qquad $\holds(y_1 \in S_1, \LL, y_k \in S_k, (E_1, \LL, E_n))$
831: \quad iff \\
832: \qquad $\holds(y_i \in S_i, (E_1, \LL, E_n))$ for $i \in [1..k]$,
833: \\\\and\\\\
834: \qquad $\holds(y_1 \in S_1, \LL, y_k \in S_k, \top)$.
835: \qquad\qquad\quad\qquad\HB
836: \end{tabbing}
837: \end{definition}
838:
839: Concerning the second item we proceed as follows.
840: \begin{definition}
841: Given a variable $z$ with the domain $D_z$ we interpret the
842: atomic formula $z \neq a$ as a function on ${\cal P}(D_z)$,
843: defined by:
844: \[
845: (z \neq a)(E) := E - \C{a}.
846: \]
847: %
848: Then we extend this function to
849: the elements of the considered ordering $(D_{\cal P}, \po )$ as follows:
850: \begin{itemize}
851: \item on the elements of the form $(E_1, \LL, E_n)$
852: we use ``padding'', that
853: is we interpret it as the identity on the other components.
854: If the resulting sequence contains the empty set, we replace it by $\top$,
855: \item on the element $\top$ we put
856: $(z \neq a)(\top) := \top$
857: \end{itemize}
858: Finally, we interpret a sequence $z_1 \neq a_1, \LL, z_m \neq a_m$
859: of atomic formulas by interpreting each of them in turn.
860: \HB
861: \end{definition}
862:
863:
864: In view of the Correctness Theorem \ref{thm:R} the following
865: observation allows us to apply the {\Ralgo} algorithm when each
866: function is a membership rule and when for each rule
867: $b \ra g$ the lists $\friends(b \ra g)$ and $\obviated(b \ra g)$ are
868: constructed by the {\FOalgo} algorithm.
869:
870: \begin{note}
871: Consider the partial ordering $(D_{\cal P}, \po )$.
872: \begin{enumerate}\smallromani
873: \item
874: Each membership rule is good.
875:
876: \item
877: Each function $z_1 \neq a_1, \LL, z_m \neq a_m$ on $D_{\cal P}$ is
878: \begin{itemize}
879: \item inflationary,
880:
881: \item monotonic.
882: \HB
883: \end{itemize}
884: \end{enumerate}
885: \end{note}
886:
887: To be able to instantiate the algorithm {\Ralgo}
888: with the membership rules we still need to define the set
889: $\update(G,g,d)$. In our implementation we chose the following
890: simple definition:
891: \[
892: \update(G,b \ra g,d) :=
893: \left\{%
894: \begin{array}{ll}
895: F-G & \mbox{if } \holds(b, d) \A g(d) \neq d\\
896: \ES & \mbox{otherwise.}
897: \end{array}%
898: \right.
899: \]
900:
901: To illustrate the intuition behind the use of the lists $\friends(b \ra g)$
902: and $\obviated(b \ra g)$ take the CSP~$\cal P :=$
903: \[
904: \p{{\cal C}}{x_1 \in \C{a,b,c}, x_2 \in \C{a,b,c}, x_3 \in \C{a,b,c}, x_4 \in
905: \C{a,b,c}}
906: \]
907: and consider the membership rules
908: \begin{eqnarray*}
909: r_1 &:=& x_1 \in \C{a,b} \;\ra\; x_2 \neq a, x_4 \neq b,\\
910: r_2 &:=& x_1 \in \C{a,b}, x_2 \in \C{b,c} \;\ra\; x_3 \neq a,\\
911: r_3 &:=& x_2 \in \C{b} \;\ra\; x_3 \neq a, x_4 \neq b.
912: \end{eqnarray*}
913: Then upon application of rule $r_1$ rule $r_2$ can
914: be applied without evaluating its condition and subsequently
915: rule $r_3$ can be deleted without applying it.
916: So we can put rule $r_2$ into $\friends(r_1)$ and rule $r_3$ into
917: $\obviated(r_1)$,
918: and this in fact is what the {\FOalgo} algorithm does.
919:
920:
921:
922: \section{Implementation}
923: \label{sec:implementation}
924:
925: In this section we discuss the implementation of the {\Ralgo}
926: algorithm for the membership rules and compare it by means of various
927: benchmarks with the \texttt{CHR} implementation in the \eclipse{} system.
928:
929:
930: \subsection{Modelling of the Membership Rules in \texttt{\large CHR}}
931:
932: Following Apt and Monfroy \cite{AM01} the membership rules are
933: represented as \texttt{CHR} propagation rules with one head. Recall
934: that the latter ones are of the form
935: \[
936: H ==> G_1, \ldots, G_l ~|~ B_1, \ldots, B_m.
937: \]
938: where
939: \begin{itemize}
940: \item $l \geq 0$, $m > 0$,
941:
942: \item the atom $H$ of the \emph{head} refers to
943: the defined constraints,
944:
945: \item the atoms of the \emph{guard} $G_1, \ldots,
946: G_l$ refer to Prolog relations or built-in constraints,
947:
948: \item the atoms of the \emph{body} $B_1, \ldots, B_m$ are arbitrary atoms.
949: \end{itemize}
950:
951: Further, recall that the \texttt{CHR} propagation rules with one head are
952: executed as follows. First, given a query (that represents a CSP) the
953: variables of the rule are renamed to avoid variable clashes. Then an
954: attempt is made to match the head of the rule against the first atom
955: of the query. If it is successful and the guard of the instantiated version
956: of the rule succeeds, the instantiated version of the body of the rule is
957: executed. Otherwise the next rule is tried.
958:
959: Finally, let us recall the representation of a membership rule as
960: a \texttt{CHR} propagation rule used in Apt and Monfroy \cite{AM01}.
961: Consider the membership rule
962: \[
963: y_1 \in S_1, \LL, y_k \in S_k \ra z_1 \neq a_1, \LL, z_m \neq a_m.
964: \]
965: related to the constraint \texttt{c} on the variables $X_1, \LL, X_n$.
966: We represent it as a \texttt{CHR} rule with the single head atom
967: $c(X_1, \LL, X_n)$ and guard atoms $\mathtt{in}(y_i, S_i)$
968: where the \texttt{in/2} predicate is defined by
969: \texttt{in(X,L) :- dom(X,D), subset(D,L)}.
970: The body consists of atomic calls $z_i\, \verb?##? \,a_i$.
971:
972:
973: In general, the application of a membership rule as defined in Section
974: \ref{sec:concrete} and the execution of its representation as a
975: \texttt{CHR} propagation rules coincide. Moreover, by the semantics of
976: \texttt{CHR}, the \texttt{CHR} rules are repeatedly applied until a
977: fixpoint is reached. So a repeated
978: application of a finite set of membership rules coincides with the
979: execution of the \texttt{CHR} program formed by the representations of
980: these membership rules as propagation rules.
981:
982:
983: \subsection{Benchmarks}
984:
985: In our approach the repeated application of a finite set of
986: membership rules is realized by means of the {\Ralgo} algorithm of
987: Section \ref{sec:revised} implemented in \eclipse{}.
988: The compiler consists of about 1500 lines of code.
989: It accepts as input a set of membership rules, each represented as a
990: \texttt{CHR} propagation rule, and constructs an \eclipse{} program
991: that is the instantiation of the {\Ralgo} algorithm for this set of
992: rules. As in \texttt{CHR}, for each constraint the set of rules that
993: refer to it is scheduled separately.
994:
995: For each considered constraint we use rules
996: generated by a program discussed in \cite{AM01}.
997: Our compiler constructs then for each rule $g$ the lists
998: $\friends(g)$ and $\obviated(g)$ by executing the \FOalgo~algorithm
999: (essentially computing a fixpoint for each rule).
1000: Time spent on this construction is comparable with rule generation time.
1001:
1002:
1003: We chose benchmarks that embody several successive propagation steps,
1004: i.\,e., propagation interleaved with domain splitting or labelling.
1005: %
1006: In Table \ref{tab:fixpoints} we list the results for selected single
1007: constraints. For each such constraint, say $C$ on a sequence of
1008: variables $x_1, \LL, x_n$ with respective domains $D_1, \LL, D_n$, we
1009: consider the CSP $\p{C}{x_1 \in D_1, \LL, x_n \in D_n}$ together with
1010: randomized labelling. That is, the choices of a variable, value, and an
1011: assignment or a removal of the value, are random.
1012: The computation of only the solutions yields times that are insignificant,
1013: so the test program computes also all intermediate fixpoints,
1014: where some domains are not singleton sets.
1015: Branching at these recorded points takes place only once, that is,
1016: backtracking occurs immediately if a recorded point is encountered again.
1017: %
1018: In Table \ref{tab:atpg} we report the results for CSP's that formalize
1019: sequential automatic test pattern generation for digital circuits
1020: (ATPG). These are rather large CSP's that employ the \texttt{and}
1021: constraints of Table \ref{tab:fixpoints} and a number of other
1022: constraints. They are taken from a recent study by the first author
1023: that will be reported elsewhere.
1024:
1025: We measured the execution times for three rule schedulers:
1026: the standard \texttt{CHR} representation of the rules,
1027: the generic chaotic iteration algorithm {\GIalgo},
1028: and its improved derivative~{\Ralgo}.
1029: The codes of the latter two algorithms are both produced by
1030: our compiler and are structurally equal, hence allow a direct
1031: assessment of the improvements embodied in~{\Ralgo}.
1032:
1033: An important point in the implementations is the question of when to
1034: remove solved constraints from the constraint store. The standard
1035: \texttt{CHR} representation of membership rules
1036: does so by containing, beside the propagation
1037: rules, one \texttt{CHR} simplification rule for each tuple in
1038: the constraint definition. Once its variables are
1039: assigned values that correspond to a tuple, the constraint is solved,
1040: and removed from the store by the corresponding simplification rule.
1041: This `solved' test takes place interleaved with propagation.
1042: %
1043: The implementations of {\GIalgo} and {\Ralgo}
1044: check after closure under the propagation rules. The constraint is
1045: considered solved if all its variables are fixed, or, in the case of
1046: {\Ralgo}, if the set $F$ of remaining rules is empty.
1047:
1048: In the tables we provide for each constraint or CSP the ratio of
1049: the execution times in seconds between,
1050: first, {\Ralgo} and {\GIalgo}, and second,
1051: {\Ralgo} and \texttt{CHR}. This is followed by the
1052: absolute times for {\Ralgo} and {\GIalgo} / \texttt{CHR}.
1053:
1054: \newcommand{\xs}[1] {{\small #1}}
1055: \newcommand{\xp}[2] {{\small {#1}\%/{#2}\%}}
1056:
1057: \begin{table}[ht]
1058: \begin{tabular*}{\columnwidth}{@{\extracolsep{\fill}}l@{}c@{}c@{}c@{}c@{}c@{}}%
1059: \hline\hline\\[-3mm]
1060: {\bfseries Const.}
1061: & \texttt{rcc8}
1062: & \texttt{fork}
1063: & \texttt{and3}
1064: & \texttt{and9}
1065: & \texttt{and11}
1066: \\\hline
1067: \textsc{mem}\\
1068: \ rel.
1069: & \xp{26}{11}
1070: & \xp{43}{40}
1071: & \xp{58}{47}
1072: & \xp{13}{6}
1073: & \xp{13}{3}
1074: \\
1075: \ abs.
1076: & \xs{109}
1077: & \xs{0.23}
1078: & \xs{0.22}
1079: & \xs{70}
1080: & \xs{55.6}
1081: \\
1082: & \xs{419/950}
1083: & \xs{0.54/0.58}
1084: & \xs{0.38/0.47}
1085: & \xs{534/1096}
1086: & \xs{427/2077}
1087: \\
1088: \textsc{equ}\\
1089: \ rel.
1090: & \xp{95}{100}
1091: & \xp{95}{89}
1092: & \xp{82}{74}
1093: & \xp{94}{97}
1094: & \xp{89}{94}
1095: \\[1mm]
1096: \ abs.
1097: & \xs{323}
1098: & \xs{18.9}
1099: & \xs{0.31}
1100: & \xs{286}
1101: & \xs{299}
1102: \\
1103: & \xs{341/324}
1104: & \xs{19.9/21.2}
1105: & \xs{0.38/0.42}
1106: & \xs{303/294}
1107: & \xs{335/318}
1108: \\\hline\hline\\
1109: \end{tabular*}
1110: \vspace{\figalgogap}
1111: \caption{Randomized search trees for constraints} %% single
1112: \label{tab:fixpoints}
1113: \centering
1114: \end{table}
1115:
1116: \iffalse
1117: \ abs.
1118: & \xs{109/419/950}
1119: & \xs{0.23/0.54/0.58}
1120: & \xs{0.22/0.38/0.47}
1121: & \xs{70/534/1096}
1122: & \xs{55.6/427/2077}
1123:
1124: \ abs.
1125: & \xs{323/341/324}
1126: & \xs{18.9/19.9/21.2}
1127: & \xs{0.31/0.38/0.42}
1128: & \xs{286/303/294}
1129: & \xs{299/335/318}
1130: \fi
1131:
1132: \newcommand{\xgg} {\hspace{1mm}}
1133:
1134: \begin{table}[ht]
1135: \begin{tabular*}{\columnwidth}
1136: {@{\extracolsep{\fill}}l@{}c@{}c@{}c@{\extracolsep{0mm}}c}
1137: \hline\hline\\[-3mm]
1138: {\bfseries Logic}
1139: & 3-valued
1140: & 9-valued
1141: & 11-valued
1142: 7 \\[1mm]\hline
1143: \textsc{mem}\\
1144: \ relative
1145: & 64\% / 35\%
1146: & 71\% / 24\%
1147: & 85\% / 86\%
1148: \\
1149: \ absolute
1150: & \xs{1.39 \xgg 2.16/4.01}
1151: & \xs{124 \xgg 175/509}
1152: & \xs{797 \xgg 933/3120}
1153: \\
1154: \textsc{equ}\\
1155: \ relative
1156: & 63\% / 70\%
1157: & 44\% / 59\%
1158: & 39\% / 48\%
1159: \\ %[1mm]
1160: \ absolute
1161: & \xs{0.72 \xgg 1.15/2.58}
1162: & \xs{2.40 \xgg 5.50/4.09}
1163: & \xs{12.3 \xgg 31.6/25.7}
1164: \\\hline\hline\\
1165: \end{tabular*}
1166: \vspace{\figalgogap}
1167: \caption{CSP's formalizing sequential ATPG}
1168: \label{tab:atpg}
1169: \centering
1170: \end{table}
1171:
1172:
1173: \subsection{Recomputing of the Least Fixpoints}
1174:
1175: Finally, let us illustrate the impact of the permanent removal of the
1176: rules during the least fixpoint computation, achieved here by the use
1177: of the lists $\friends(g)$ and $\obviated(g)$. Given a set $F$ of
1178: rules call a rule $g \in F$ \emph{solving} if $\friends(g) \cup
1179: \obviated(g) = F$.
1180:
1181: Take now as an example the equivalence relation $\equiv$ from three valued logic
1182: of
1183: Kleene \cite{Kle52}[page 334] that consists of three values, t (true),
1184: f (false) and u (unknown).
1185: It is defined by the truth table
1186: \[
1187: \begin{array}{|c|ccc|} \hline
1188: \equiv & $t$ & $f$ & $u$ \\ \hline
1189: $t$ & $t$ & $f$ & $u$ \\
1190: $f$ & $f$ & $t$ & $u$ \\
1191: $u$ & $u$ & $u$ & $u$ \\
1192: \hline
1193: \end{array}
1194: \]
1195: %
1196: The program of Apt and Monfroy \cite{AM01} generates for it 26 minimal
1197: valid membership rules. Out of them 12 are solving rules. For the
1198: remaining rules the sizes of the set $\mathit{friends} \cup
1199: \mathit{obviated}$ are: 17 (for 8 rules), 14 (for 4 rules), and 6 (for
1200: 2 rules).
1201:
1202: In the {\Ralgo} algorithm a selection of a solving rule leads
1203: directly to the termination ($G = \ES$) and to a reduction of the set
1204: $F$ to $\ES$. For other rules also a considerable simplification in the
1205: computation takes place. For example, one of the 8 rules with 17 rules in
1206: its set $\mathit{friends} \cup \mathit{obviated}$ is
1207: \[
1208: r:= x \in \{0\}, z \in \{0, u\} \ra y \not= 0.
1209: \]
1210: Consider the CSP
1211: $\p{\equiv}{x \in \{0\}, y \in \{0,1,u\}, z \in \{0,u\}}$.
1212: In the {\Ralgo} algorithm the selection
1213: of $r$ is followed by the application of the rules in
1214: $\friends$ and the removal of the rules in $\friends \cup \obviated$.
1215: This brings the number of the considered rules down to $26 - 17 =
1216: 9$. The {\Ralgo}~algorithm subsequently discovers that none of these
1217: nine rules is applicable at this point, so this set $F$ remains upon
1218: termination. Then in a subsequent constraint propagation phase,
1219: launched after splitting or after constraint propagation involving
1220: another constraint, the fixpoint computation by means of the
1221: {\Ralgo} algorithm involves only these nine rules instead of the
1222: initial set of 26 rules. For solving rules, this fixpoint computation
1223: immediately terminates.
1224:
1225: Interestingly, as Table \ref{tab:solving} shows, the solving rules
1226: occur quite frequently. We list there for each constraint and each
1227: type of rules the number of solving rules divided by the total number
1228: of rules, followed in a new line by the average number of rules in the
1229: set $\friends(g) \cup \obviated(g)$.
1230:
1231: \begin{table}[hb]
1232: \begin{tabular*}{\columnwidth}{@{\extracolsep{\fill}}l@{}c@{}c@{}c@{}c@{}c@{}c@{}c@{}}%
1233: \hline\hline
1234: %{\bfseries Constraints}
1235: & \texttt{and2}
1236: & \texttt{and3}
1237: & \texttt{and9}
1238: & \texttt{and11}
1239: & \texttt{fork}
1240: & \texttt{rcc8}
1241: & \texttt{allen}
1242: \\\hline\\[-2mm]
1243: \textsc{equ} %equality
1244: & 6/6
1245: & 13/16
1246: & 113/134
1247: & 129/153
1248: & 9/12
1249: & 183/183
1250: & 498/498
1251: \\
1252: & 6
1253: & 14
1254: & 130
1255: & 148
1256: & 11
1257: & 183
1258: & 498
1259: \\[0mm]
1260: \textsc{mem} %membership
1261: & 6/6
1262: & 4/13
1263: & 72/1294
1264: & 196/4656
1265: & 0/24
1266: & 0/912
1267: & -/26446 %% Allen: too many rules
1268: \\
1269: & 6
1270: & 7
1271: & 810
1272: & 3156
1273: & 9
1274: & 556
1275: & - %% Allen: too many rules
1276: \\[0mm]
1277: \hline\hline\\
1278: \end{tabular*}
1279: \vspace{\figalgogap}
1280: \caption{Solving rules}
1281: \label{tab:solving}
1282: \end{table}
1283:
1284: The \texttt{fork} constraint is taken from the Waltz language for the
1285: analysis of polyhedral scenes. The \texttt{rcc8} is the composition
1286: table for the Region Connection Calculus with 8 relations from
1287: Egenhofer \cite{Ege91}. It is remarkable that all its 183 minimal
1288: valid equality rules are solving. While none of its 912 minimal valid
1289: membership rule for \texttt{rcc8} is solving, on the average the set
1290: $\friends(g) \cup \obviated(g)$ contains 556 membership
1291: rules. Also all 498 minimal valid equality rules for the
1292: \texttt{allen} constraint, that represents the composition table for
1293: Allen's qualitative temporal reasoning, are solving.
1294: \balancecolumns
1295: The number of
1296: minimal valid membership rules exceeds 26,000 and consequently they
1297: are too costly to analyze.
1298:
1299: %\balancecolumns
1300:
1301: The savings obtained by means of the lists $\friends(g)$ and $\obviated(g)$
1302: are orthogonal to the ones obtained by a transformation of the \texttt{CHR}
1303: propagation rules into the simplification rules discussed in
1304: Abdennadher and Rigotti \cite{AR01}.
1305: We think that there is a relation between two approaches that we plan to
1306: study closer.
1307:
1308:
1309:
1310: \section*{Acknowledgments}
1311:
1312: We thank Christian Holzbaur and Eric Monfroy for helpful discussions
1313: on the implementation and on an early version of this paper,
1314: and the referees for useful comments.
1315:
1316:
1317: %\bibliographystyle{alpha}
1318: \bibliographystyle{plain}
1319:
1320: \bibliography{/ufs/apt/book-ao-2nd/apt,/ufs/apt/esprit/esprit,
1321: /ufs/apt/esprit/chapter3,/ufs/apt/bib/clp2,/ufs/apt/bib/clp1,
1322: /ufs/apt/book-lp/man1,/ufs/apt/book-lp/man2,/ufs/apt/book-lp/man3,
1323: /ufs/apt/book-lp/ref1,/ufs/apt/book-lp/ref2,/ufs/apt/bib/99}
1324:
1325: \end{document}
1326: