documents/tutorial/propiachr.tex

23 \chapter{Propia and CHR}
29 available in \eclipse{}, called {\em Propia} and {\em Constraint
52 and by Propia.
84 The same behaviour can be expressed in Propia, but this time the
87 extracted from the two clauses by Propia when the {\em noclash} goal
105 Propia and CHRs make it easy to turn the logical statement of a
109 \section{The Role of Propia and CHR in Problem Modelling}
134 Propia and CHR's support the separation of constraint setup and search
186 to \verb0product0 as a Propia constraint making:
191 In the remainder of this chapter we show how to use Propia and CHR's,
196 Propia and CHRs can be used to build clear problem models that have no
200 \section{Propia}
205 Propia is an implementation of {\em Generalised Propagation}
208 \subsection{How to Use Propia}
210 In principle Propia propagates information from an annotated goal by
213 (In practice, as we shall see later, Propia does not typically need to
230 invoked, then the information propagated by Propia is that $X=1$.
232 information is propagated.  Not only does Propia propagate $X=1$ but
288 conditions for Propia.  By only waking a Propia constraint when it
298 one using \verb0infers consistent0.  To find the best Propia
303 Propia extracts information from a procedure which may be defined by
306 controlled by the Propia annotation.
310 \subsection{Propia Implementation}
311 In this section we describe how Propia works.
314 When a goal is annotated as a Propia constraint, eg.
317 However Propia does not stop at the first solution, but continues to
320 When all the information has been accumulated, Propia propagates this
324 Propia then suspends the goal again, until the variables become
329 If Propia detects that the goal is entailed (i.e. the goal would
336 Propia works by treating its input both as a {\em goal} to be called,
344 Propia combines information from the solutions to a goal using their
362 We can illustrate this being exploited by Propia in the following
412 \subsubsection{The Propia Algorithm}
413 We can now specify the Propia algorithm more precisely.
414 The Propia constraint is
444 Propia's termination is dramatically improved by the check that the
450 Thus, because of this check, Propia will terminate as long as each
453 For example the Propia constraint
460 Propia computes the Most Specific Generalisation (MSG) of the set of
463 The MSG depends upon the annotation of the Propia call.
466 \subsection{Propia and Related Techniques}
470 annotated this way, then Propia would enforce arc consistency.
473 Propia generalises traditional arc consistency in two ways.  Firstly
477 this can be exploited by using \verb0infers ac0 to make Propia run
479 Propia simply finds all solutions and
488 Propia also generalises {\em constructive disjunction}.  Constructive
493 Propia can also handle recursively defined predicates, like
782 Propia and CHRs provide alternative methods of achieving more global
784 Propia allows any subproblem to be treated as a single constraint.
786 Each technique has special strengths.  Propia is good for handling
793 \section{Propia and CHR Exercise}
798 in CHRs and, as a separate exercise, in Propia.