1% BEGIN LICENSE BLOCK 2% Version: CMPL 1.1 3% 4% The contents of this file are subject to the Cisco-style Mozilla Public 5% License Version 1.1 (the "License"); you may not use this file except 6% in compliance with the License. You may obtain a copy of the License 7% at www.eclipse-clp.org/license. 8% 9% Software distributed under the License is distributed on an "AS IS" 10% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See 11% the License for the specific language governing rights and limitations 12% under the License. 13% 14% The Original Code is The ECLiPSe Constraint Logic Programming System. 15% The Initial Developer of the Original Code is Cisco Systems, Inc. 16% Portions created by the Initial Developer are 17% Copyright (C) 2006 Cisco Systems, Inc. All Rights Reserved. 18% 19% Contributor(s): 20% 21% END LICENSE BLOCK 22 23\chapter{Propia and CHR} 24\label{chappropiachr} 25%HEVEA\cutdef[1]{section} 26 27\section{Two Ways of Specifying Constraint Behaviours} 28There are two elegant and simple ways of building constraints 29available in \eclipse{}, called {\em Propia} and {\em Constraint 30Handling Rules} (or {\em CHR}'s). 31They are themselves built using the facilities 32described in chapter \ref{chapimpl}. 33 34\index{noclash} 35Consider a simple {\em noclash} constraint requiring that two 36activities cannot be in progress at the same time. 37For the sake of the example, the constraint involves two variables, 38the start times $S1$ and $S2$ 39of the two activities, which both have duration $5$. 40Logically this constraint states that 41{\em noclash} $ \Leftrightarrow (S1 >= S2 + 5 \vee S2 >= S1 + 5)$. 42The same logic can be expressed as two \eclipse{} clauses: 43\begin{code} 44noclash(S1,S2) :- 45 ic:(S1 \$>= S2+5). 46noclash(S1,S2) :- 47 ic:(S2 \$>= S1+5). 48\end{code} 49Constraint propagation elicits information from constraints without 50leaving any choice points. Constraint propagation behaviour can be 51associated with each of the above representations, by CHR's 52and by Propia. 53 54One way to propagate information from {\em noclash} is to wait until 55the domains of the start times are reduced sufficiently that only one 56ordering of the tasks is possible, and then to enforce the constraint 57that the second task not start until the first is finished. 58 59\index{constraints/1} 60This behaviour can be implemented in CHR's as follows: 61\begin{code} 62:- constraints noclash/2. 63noclash(S1,S2) <=> ic:(S2 #< S1+5) | ic:(S1 #>= S2+5). 64noclash(S1,S2) <=> ic:(S1 #< S2+5) | ic:(S2 #>= S1+5). 65\end{code} 66 67Consider the query: 68\begin{quote} 69\begin{verbatim} 70?- ic:([S1,S2]::1..10), 71 noclash(S1,S2), 72 S1 #>= 6. 73\end{verbatim} 74\end{quote} 75In this query {\em noclash} achieves no propagation when it is 76initially posted with the start time domains set to \verb91..109. 77However, after imposing $S1>=6$, 78the domain of $S1$ is reduced to \verb96..109. 79Immediately the {\em noclash} 80constraint wakes, detects that the first 81condition $S1+5 >= S2$ is entailed, 82and narrows the domain of $S2$ to \verb91..59. 83 84The same behaviour can be expressed in Propia, but this time the 85original \eclipse{} representation of {\em noclash} as two clauses is 86used directly. The propagation behaviour is automatically 87extracted from the two clauses by Propia when the {\em noclash} goal 88is annotated as follows: 89\begin{quote} 90\begin{verbatim} 91?- [S1,S2]::1..10, 92 noclash(S1,S2) infers most, 93 S1 #>= 6. 94\end{verbatim} 95\end{quote} 96%For readability \verb0infers0 is declared to be an infix operator, 97%enabling the annotation to be written thus: 98%\begin{quote} 99%\begin{verbatim} 100%?- [S1,S2]::1..10, noclash(S1,S2) infers most, S1 #>= 6 101%\end{verbatim} 102%\end{quote} 103 104\quickref{Building Constraints without Tears}{ 105Propia and CHRs make it easy to turn the logical statement of a 106constraint into code that efficiently enforces that constraint. 107} 108 109\section{The Role of Propia and CHR in Problem Modelling} 110 111\index{modelling} 112To formulate and solve a problem in \eclipse{} the standard pattern is 113as follows: 114\begin{enumerate} 115\item Initialise the problem variables 116\item State the constraints 117\item Specify the search behaviour 118\end{enumerate} 119Very often, however, the constraints involve logical implications or 120disjunctions, as in the case of the {\em noclash} constraint above. 121Such constraints are most naturally formulated in a way that would 122introduce choice points during the constraint posting phase. 123The two \eclipse{} clauses defining {\em noclash}, above, are a case in 124point. 125 126There are two major disadvantages of introducing choice points during 127constraint posting: 128\begin{itemize} 129\item Posting and reposting constraints during search is an 130unnecessary and computationally expensive overhead 131\item Mixing constraint behaviour and search behaviour makes it harder 132to explore and optimize the algorithm executed by the program. 133\end{itemize} 134Propia and CHR's support the separation of constraint setup and search 135behaviour, by allowing constraints to be formulated naturally without 136their execution setting up any choice points. 137 138The effect on performance is illustrated by the following small 139example. 140The aim is to choose a set of $9$ products (\verb0Products0, 141identified by their product number 101-109) to 142manufacture, with a 143limited quantity of raw materials (\verb0Raw10 and \verb0Raw20), 144so as to achieve a profit (\verb0Profit0) of over 145$40$. 146The amount of raw materials (of two kinds) needed to produce 147each product is listed in a table, together with its profit. 148 149\index{product\_plan} 150\index{product} 151\begin{code} 152product_plan(Products) :- 153 length(Products,9), 154 Raw1 #=< 95, 155 Raw2 #=< 95, 156 Profit #>= 40, 157 sum(Products,Raw1,Raw2,Profit), 158 labeling(Products). 159 160product( 101,1,19,1). product( 102,2,17,2). product( 103,3,15,3). 161product( 104,4,13,4). product( 105,10,8,5). product( 106,16,4,4). 162product( 107,17,3,3). product( 108,18,2,2). product( 109,19,1,1). 163 164sum(Products,Raw1,Raw2,Profit) :- 165 ( foreach(Item,Products), 166 foreach(R1,R1List), 167 foreach(R2,R2List), 168 foreach(P,PList) 169 do 170 product(Item,R1,R2,P) 171 ), 172 Raw1 #= sum(R1List), 173 Raw2 #= sum(R2List), 174 Profit #= sum(PList). 175 176\end{code} 177 178The drawback of this program is that the \verb0sum0 constraint calls 179\verb0product0 which chooses an item and leaves a choice point at each 180call. 181Thus the setup of the \verb0sum0 constraint leaves $9$ choice points. 182Try running it, and the program 183fails to terminate within a reasonable amount of time. 184 185Now to make the program run efficiently, we can simply annotate the call 186to \verb0product0 as a Propia constraint making: 187\verb0product(Item,R1,R2,P) infers most0. 188This program leaves no choice points during constraint setup, and 189finds a solution in a fraction of a second. 190 191In the remainder of this chapter we show how to use Propia and CHR's, 192give some 193examples, and outline their implementation. 194 195\quickref{Modelling without Choice Points}{ 196Propia and CHRs can be used to build clear problem models that have no 197(hidden) choice points. 198} 199 200\section{Propia} 201\label{secpropia} 202 203\index{propia} 204\index{generalised propagation} 205Propia is an implementation of {\em Generalised Propagation} 206which is described in the paper \cite{LeProvost93b}. 207 208\subsection{How to Use Propia} 209\index{infers/2} 210In principle Propia propagates information from an annotated goal by 211finding all solutions to the goal and extracting any information that 212is common to all the different solutions. 213(In practice, as we shall see later, Propia does not typically need to 214find all the solutions.) 215 216The ``common'' information that can be extracted depends upon what 217constraint solvers are used when evaluating the underlying 218un-annotated \eclipse{} goal. To illustrate this, consider another 219simple example. 220 221\begin{quote} 222\begin{verbatim} 223p(1,3). 224p(1,4). 225 226?- p(X,Y) infers most. 227\end{verbatim} 228\end{quote} 229If the {\tt ic} library is not loaded when this query is 230invoked, then the information propagated by Propia is that $X=1$. 231If, on the other hand, {\tt ic} is loaded, then more common 232information is propagated. Not only does Propia propagate $X=1$ but 233also the domain of $Y$ is tightened from \verb0-inf..inf0 to 234\verb03..40. (In this case the additional common information is that 235$Y \neq 0$, $Y \neq 1$, $Y \neq 2$ and so on for all values except $3$ 236and $4$!) 237 238\index{most} 239\index{consistent} 240\index{unique} 241\index{ac} 242Any goal \verb0Goal0 in an \eclipse{} program, can be transformed into a 243constraint by annotating it thus: \verb0Goal infers Parameter0. 244Different behaviours can be specified with different parameters, viz: 245\begin{itemize} 246\item \verb0Goal infers most0\\ 247Propagates all common information produced by the loaded solvers 248\item \verb0Goal infers unique0\\ 249Fails if there is no solution, propagates the solution if it is 250unique, and succeeds without propagating further information if there 251is more than one solution. 252\item \verb0Goal infers consistent0\\ 253Fails if there is no solution, and propagates no information otherwise 254\end{itemize} 255 256%\item \verb0Goal infers ic0\\ 257%Tightens the domains of the variables. 258%\item \verb0Goal infers ac0\\ 259%Tightens the domains of the variables: more efficient than \verb0ic0, 260%but can only handle goals with a finite set of ground answers. 261 262\index{crossword} 263These behaviours are nicely illustrated by the crossword demonstration 264program \verb0crossword0 in the examples code directory. 265There are 72 ways to complete the crossword grid with words from the 266accompanying directory. 267For finding all 72 solutions, 268the comparative performance of the different annotations is given in the 269table {\em Comparing Annotations}. 270 271\begin{table}[tb] 272\begin{center} 273\begin{tabular}{|c|c|c|c|} 274\hline 275Annotation & CPU time (secs)\\ 276\hline 277consistent & 13.3 \\ 278unique & 2.5 \\ 279most & 9.8 \\ 280ac & 0.3 \\ 281\hline 282\end{tabular} 283\end{center} 284\caption{Comparing Annotations} 285\end{table} 286 287The example program also illustrates the effect of specifying the waking 288conditions for Propia. By only waking a Propia constraint when it 289becomes instantiated, the time to solve the crossword problem can be 290changed considerably. For example by changing the annotation from 291\verb0Goal infers most0 to 292\verb0suspend(Goal,4,Goal->inst) infers most0 293the time needed to find all solutions goes down from 10 seconds to 294just one second. 295 296For other problems, such as the square tiling problem in the example 297directory, the fastest version is the 298one using \verb0infers consistent0. To find the best Propia 299annotation it is necessary to experiment with the current problem 300using realistic data sets. 301 302\quickref{Transforming Procedures to Constraints}{ 303Propia extracts information from a procedure which may be defined by 304multiple \eclipse{} clauses. 305The information to be extracted is 306controlled by the Propia annotation. 307% (e.g. \verb0consistent0, \verb0unique0, \verb0most0 and \verb0ac0). 308} 309 310\subsection{Propia Implementation} 311In this section we describe how Propia works. 312 313\subsubsection{Outline} 314When a goal is annotated as a Propia constraint, eg. 315\verb0p(X,Y) infers most0, first the goal \verb0p(X,Y)0 is in effect 316evaluated in the normal way by \eclipse{}. 317However Propia does not stop at the first solution, but continues to 318find more and more solutions, each time combining the information from 319the solutions retrieved. 320When all the information has been accumulated, Propia propagates this 321information (either by narrowing the domains of variables in the goal, 322or partially instantiating them). 323 324Propia then suspends the goal again, until the variables become 325further constrained, at which point it wakes, extracts information 326from solutions to the more constrained goal, propagates it, and 327suspends again. 328 329If Propia detects that the goal is entailed (i.e. the goal would 330succeed whichever way the variables were instantiated), then after 331propagation it does not suspend any more. 332 333\subsubsection{Most Specific Generalisation} 334\index{most specific generalisation} 335\index{MSG} 336Propia works by treating its input both as a {\em goal} to be called, 337and as a term which can be manipulated as data. 338As with any \eclipse{} goal, when executed its result is a further 339instantiation of the term. 340For example the first result of calling \verb0member(X,[a,b,c])0 is 341to further instantiate the term yielding \verb0member(a,[a,b,c])0. 342This instantiated term represents the (first) solution to the goal. 343 344Propia combines information from the solutions to a goal using their 345{\em most specific generalisation} ({\em MSG}). 346The MSG of two terms is a term 347that can be instantiated (in different ways) to either of the two 348terms. For example 349$p(a,f(Y))$ is the MSG of $p(a,f(b))$ and $p(a,f(c))$. 350This is the meaning of {\em generalisation}. 351The meaning of {\em most specific} is that any other term that 352generalises the two terms, is more general than the MSG. 353For example, any other term that generalises $p(a,f(b)$ and 354$p(a,f(c))$ can be instantiated to $p(a,f(Y))$. 355The MSG of two terms captures only information that is common to both 356terms (because it generalises the two terms), and it captures all the 357information possible in the two terms (because it is the most specific 358generalisation). 359 360Some surprising information is caught by the MSG. For example the MSG 361of $p(0,0)$ and $p(1,1)$ is $p(X,X)$. 362We can illustrate this being exploited by Propia in the following 363example: 364\begin{code} 365% Definition of logical conjunction 366conj(1,1,1). 367conj(1,0,0). 368conj(0,1,0). 369conj(0,0,0). 370 371conjtest(X,Z) :- 372 conj(X,Y,Z) infers most, 373 X=Y. 374\end{code} 375The test succeeds, recognising that $X$ must take the same truth value 376as $Z$. Running this in \eclipse{} yields: 377\begin{quote} 378\begin{verbatim} 379[eclipse]: conjtest(X,Z). 380X = X 381Z = X 382Delayed goals: 383 conj(X, X, X) infers most 384Yes (0.00s cpu) 385\end{verbatim} 386\end{quote} 387 388If the {\tt ic} library is loaded more information can be extracted, 389because the MSG of $0$ and $1$ is a variable with domain \verb90..19. 390Thus the result of the above example is not only to equate $X$ and $Z$ 391but to associate with them the domain \verb90..19. 392 393The MSG of two terms depends upon what information is expressible in 394the MSG term. As the above example shows, if the term can employ 395variable domains the MSG is more precise. 396 397By choosing the class of terms in which the MSG can be 398expressed, we can capture more or less information in the MSG. 399If, for example, we allow only terms of maximum depth 1 in the class, 400then MSG can only capture functor and arity. 401In this case the MSG of $f(a,1)$ and $f(a,2)$ is simply $f(_,_)$, even 402though there is more shared information at the next depth. 403 404In fact the class of terms can be extended to a lattice, by 405introducing a bottom $\bot$ and a top $\top$. 406$\bot$ is a term carrying no 407information; $\top$ is a term representing inconsistent information; 408the 409meet of two terms is the result of unifying them; and their join is 410their MSG. 411 412\subsubsection{The Propia Algorithm} 413We can now specify the Propia algorithm more precisely. 414The Propia constraint is 415\begin{verbatim}Goal infers Parameter \end{verbatim} 416 417\begin{itemize} 418\item Set $OutTerm := \top$ 419\item Repeat 420\begin{itemize} 421\item Find a solution $S$ to $Goal$ which is {\em not} an instance of 422$OutTerm$ 423\item Find the MSG, in the class specified by \verb0Parameter0, 424of $OutTerm$ and $S$. Call it $MSG$ 425\item Set $OutTerm := MSG$ 426\end{itemize} 427until either $Goal$ is an instance of $OutTerm$, or no such 428solution remains 429\item Return $OutTerm$ 430\end{itemize} 431 432When \verb0infers most0 is being handled, the class of terms admitted 433for the MSG is the biggest class expressible in terms of the currently 434loaded solvers. In case $ic$ is loaded, this includes variable 435domain, but otherwise it includes any \eclipse{} term without variable 436attributes. 437 438The algorithm supports \verb0infers consistent0 by admitting only the 439two terms $\top$ and $\bot$ in the MSG class. 440\verb0infers unique0 is a variation of the algorithm in which the 441first step $OutTerm := \top$ is changed to finding a first solution 442$S$ to $Goal$ and initialising $OutTerm := S$. 443 444Propia's termination is dramatically improved by the check that the 445next solution found is not an 446instance of $OutTerm$. In the absence of domains, there is no 447infinite sequence of terms that strictly generalise each other. 448Moreover, if 449the variables in $Goal$ have finite domains, the same result holds. 450Thus, because of this check, Propia will terminate as long as each 451call of $Goal$ terminates. 452 453For example the Propia constraint 454\verb0member(Var,List) infers Parameter0 will 455always terminate, if each call of \verb0member(Var,List)0 does, even in 456case 457\verb0member(Var,List)0 has infinitely many solutions! 458 459\quickref{Most Specific Generalisation}{ 460Propia computes the Most Specific Generalisation (MSG) of the set of 461solutions to a procedure. It does so without, necessarily, 462backtracking through all the solutions to the procedure. 463The MSG depends upon the annotation of the Propia call. 464} 465 466\subsection{Propia and Related Techniques} 467If the finite domain solver is loaded then \verb0Goal infers most0 prunes 468the variable domains so every value is supported by values in the 469domains of the other variables. If every problem constraint was 470annotated this way, then Propia would enforce arc consistency. 471 472\index{arc consistency} 473Propia generalises traditional arc consistency in two ways. Firstly 474it admits n-ary constraints, and secondly it handles predicates 475defined by rules, as well as ground facts. In the special case that 476the goal can be ``unfolded'' into a finite set of ground solutions, 477this can be exploited by using \verb0infers ac0 to make Propia run 478more efficiently. When called with parameter \verb0infers ac0, 479Propia simply finds all solutions and 480applies n-ary arc-consistency to the resulting tables. 481 482%associates an identifier with each tuple. Arc-consistency is then 483%applied to the binary constraints between the tuple identifiers and 484%tuple values for each attribute, using the \verb0element0 constraint 485%in the {\tt ic} library. 486 487\index{constructive disjunction} 488Propia also generalises {\em constructive disjunction}. Constructive 489disjunction could be applied in case the 490predicate was unfolded into a finite set of solutions, where each 491solution was expressed using {\tt ic} constraints (such as equations, 492inequations etc.). 493Propia can also handle recursively defined predicates, like 494\verb0member0, exampled above, which may have an infinite number of 495solutions. 496 497 498\section{CHR} 499\label{secchr} 500\index{CHR} 501Constraint Handling Rules were originally implemented in \eclipse{}. 502They are introduced in the paper \cite{Fruehwirth}. 503 504\subsection{How to Use CHR} 505\index{simplification rule} 506\index{propagation rule} 507CHR's offer a rule-based programming style to express constraint 508simplification and constraint propagation. 509The rules all have a {\em head}, an explicit or implicit {\em guard}, 510and a {\em body}, and are written either 511\begin{quote} 512\begin{verbatim} 513Head <=> Guard | Body. %Simplification Rule 514\end{verbatim} 515\end{quote} 516or 517\begin{quote} 518\begin{verbatim} 519Head ==> Guard | Body. %Propagation Rule 520\end{verbatim} 521\end{quote} 522When a constraint is posted that is an instance of the head, the guard 523is checked to determine whether the rule can fire. 524If the guard is satisfied (i.e. CHR detects that it is entailed by the 525current search state), the 526rule {\em fires}. 527Unlike \eclipse{} clauses, the rules leave no choice points. 528Thus if several rules share the same head and one fires, the other 529rules are never fired even after a failure. 530 531Normally the guards exclude each other, as in the \verb0noclash0 532example: 533\begin{code} 534:- lib(ech). 535:- constraints noclash/2. 536noclash(S1,S2) <=> ic:(S2 #< S1+5) | ic:(S1 #>= S2+5). 537noclash(S1,S2) <=> ic:(S1 #< S2+5) | ic:(S2 #>= S1+5). 538\end{code} 539Henceforth we will not explicitly load the {\tt ech} library. 540 541The power of guards lies in the behaviour of the rules when they are 542neither entailed, nor disentailed. 543Thus in the query 544\begin{quote} 545\begin{verbatim} 546?- ic:([S1,S2]::1..10), 547 noclash(S1,S2), 548 S1 #>= 6. 549\end{verbatim} 550\end{quote} 551\begin{sloppypar} 552when the \verb0noclash0 constraint is initially posted, neither guard 553is entailed, and CHR simply postpones the handling of the constraint 554until further constraints are posted. 555As soon as a guard becomes entailed, however, the rule fires. 556For simplification rules, of the form 557\verb0Head <=> Guard | Body0, 558the head is replaced by the body. 559In this example, therefore, \verb0noclash(S1,S2)0 is replaced by 560\verb0S1 #>= S2+50. 561\end{sloppypar} 562 563Propagation rules are useful to add constraints, instead of replacing 564them. 565Consider, for example, an application to temporal reasoning. 566If the time $T1$ is before time $T2$, then we can propagate an 567additional $ic$ constraint saying $T1 =< T2$: 568\begin{code} 569:- constraints before/2. 570before(T1,T2) ==> ic:(T1 \$=< T2) 571\end{code} 572This rule simply posts the constraint \verb0T1 $=< T20 to $ic$. 573When a propagation rule fires its body is invoked, but its head 574remains in the constraint store. 575 576\subsection{Multiple Heads} 577 578Sometimes different constraints interact, and more can be deduced 579from the combination of constraints than can be deduced from the 580constraints separately. Consider the following query: 581\begin{quote} 582\begin{verbatim} 583?- ic:([S1,S2]::1..10), 584 noclash(S1,S2), 585 before(S1,S2). 586\end{verbatim} 587\end{quote} 588Unfortunately the {\tt ic} bounds are not tight enough for the 589\verb0noclash0 rule to fire. 590The two constraints can be combined so as to propagate $S2 \ge S1+5$ 591using a two-headed 592CHR: 593\begin{quote} 594\begin{verbatim} 595noclash(S1,S2), before(S1,S2) ==> ic:(S2 #>= S1+5). 596\end{verbatim} 597\end{quote} 598We would prefer to write a set of rules that captured this kind of 599inference in a general way. 600 601\index{simpagation rule} 602This can be achieved by writing a more complete solver for 603\verb0prec0, and combining it with \verb0noclash0. 604$prec(S1,D,S2)$ holds if the time $S1$ precedes the time $S2$ by at 605least $D$ units of time. 606For the following code to work, $S1$ and $S2$ may be numbers or 607variables, but $D$ must be a number. 608\begin{code} 609:- constraints prec/3. 610prec(S,D,S) <=> D=<0. 611prec(S1,0,S2), prec(S2,0,S1) <=> S1=S2. 612prec(S1,D1,S2), prec(S2,D2,S3) ==> D3 is D1+D2, prec(S1,D3,S3). 613prec(S1,D1,S2) \verb.\. prec(S1,D2,S2) <=> D2=<D1 | true. % Simpagation 614 615noclash(S1,S2), prec(S1,D,S2) ==> D > -5 | prec(S1,5,S2). 616noclash(S1,S2), prec(S2,D,S1) ==> D > -5 | prec(S2,5,S1). 617\end{code} 618Note the {\em simpagation} rule, whose head has two parts 619\verb0Head1 \ Head20. 620In a simpagation rule \verb0Head20 is replaced, but \verb0Head10 is 621kept in the constraint store. 622 623\quickref{CHRs}{ 624CHRs are guarded rules which fire without leaving choice points. 625A CHR rule may have one or many goals in the head, and may take the 626following forms: Simplification rule, Propagation rule or Simpagation 627rule. 628%\begin{itemize} 629%\item[{\em Simplification} rule] \verb0Head <=> Guard | Body0 630%\item[{\em Propagation} rule] \verb0Head ==> Guard | Body0 631%\item[{\em Simpagation} rule] \verb0Head1 \ Head2 <=> Guard | Body0 632%\end{itemize} 633 634} 635 636\section{A Complete Example of a CHR File} 637 638Sometimes whole sets of constraints can be combined. 639Consider, for example, a program where disequalities on pairs of 640variables are accumulated during search. 641Whenever a point is reached where any subset of the variables are all 642constrained to be different an \verb0alldifferent0 constraint can be 643posted on that subset, thus supporting more powerful propagation. 644This can be achieved by finding {\em cliques} in the graph whose nodes 645are variables and edges are disequality constraints. 646 647\index{clique} 648We start our code with a declaration to load the {\em ech} library. 649The constraints are then declared, and subsequently defined by rules. 650The CHR encoding starts by generating a clique whenever two variables 651are constrained to be different. 652\begin{code} 653:- lib(ech). 654:- constraints neq/2. 655 656neq(X,Y) ==> 657 sort([X,Y],List), 658 clique(List), 659 neq(Y,X). 660\end{code} 661Each clique is held as a sorted list to avoid any duplication. 662The symmetrical disequality is added to simplify the detection of new 663cliques, below. 664Whenever a clique is found, the \verb0alldifferent0 constraint is 665posted, and the CHRs seek to extend this clique to 666include another variable: 667\begin{code} 668:- constraints clique/1. 669 670clique(List) ==> alldifferent(List). 671clique(List),neq(X,Y) ==> 672 in_clique(Y,List), not in_clique(X,List) | 673 sort([X|List],Clique), 674 extend_clique(X,List,Clique). 675 676in_clique(Var,List) :- 677 member(El,List), El==Var, !. 678\end{code} 679The idea is to search the constraint store for a disequality between 680the new variable \verb0X0 and each other variable in the original 681clique. This is done by recursing down the list of remaining 682variables. 683When there are no more variables left, a new clique has been found. 684\begin{code} 685neq(X,Y) \verb.\. extend_clique(X,[Y|Tail],Clique) <=> 686 extend_clique(X,Tail,Clique). 687extend_clique(_,[],Clique) <=> 688 clique(Clique). 689\end{code} 690 691Finally, we add three optimisations. 692Don't try and find a clique that has already been found, or 693find the same clique twice. If the new variable is equal to a 694variable in the list, then don't try any further. 695\begin{code} 696clique(Clique) \verb.\. extend_clique(_,_,Clique) <=> true. 697extend_clique(_,_,Clique) \verb.\. extend_clique(_,_,Clique) <=> true. 698extend_clique(Var,List,_) <=> in_clique(Var,List) | true. 699\end{code} 700 701\subsection{CHR Implementation} 702CHR's are implemented using the \eclipse{} suspension and waking 703mechanisms. 704A rule is woken if: 705\begin{itemize} 706\item a new goal is posted, which matches one of the goals in its head 707\item a goal which has already been posted earlier becomes further 708instantiated. 709\end{itemize} 710 711\index{entailment} 712The rule cannot fire unless the goal is more instantiated than the 713rule head. Thus the rule 714\verb0p(a,f(Y),Y) <=> q(Y)0 is really a shorthand for the guarded 715rule: 716\begin{quote} 717\begin{verbatim} 718p(A,B,C) <=> A=a, B=f(Y), C=Y | q(Y) 719\end{verbatim} 720\end{quote} 721The guard is ``satisfied'' if, logically, it is entailed by the 722constraints posted already. 723 724In practice the CHR implementation cannot always detect the 725entailment. 726The consequence is that goals may fire later than they could. 727For example consider the program 728\begin{code} 729:- constraints p/2. 730p(X,Y) <=> ic:(X \$> Y) | q(X,Y). 731\end{code} 732and the goal 733\begin{quote} 734\begin{verbatim} 735?- ic:(X $> Y), 736 p(X,Y). 737\end{verbatim} 738\end{quote} 739Although the guard is clearly satisfied, the CHR implementation cannot 740detect this and \verb0p(X,Y)0 does not fire. 741If the programmer needs the entailment of inequalities to be detected, 742it is necessary to express inequalities as CHR constraints, which 743propagate {\tt ic} constraints as illustrated in the example 744\verb0prec(S1,D,S2)0 above. 745 746CHRs can detect entailment via variable bounds, so \verb.p(X,0). 747does fire in the following example: 748\begin{quote} 749\begin{verbatim} 750?- ic:(X $> 1), 751 p(X,0). 752\end{verbatim} 753\end{quote} 754 755The implementation of this entailment test in \eclipse{} is to impose 756the guard as a constraint, and fail (the entailment test) as soon as 757any variable becomes more constrained. 758A variable becomes more constrained if: 759\begin{itemize} 760\item it becomes more instantiated 761\item its domain is tightened 762\item a new goal is added to its suspension list 763\end{itemize} 764 765There are many examples of applications expressed in CHR in the 766\eclipse{} distribution. 767They are held as files in the {\em chr} subdirectory of the standard 768\eclipse{} library directory {\em lib}. 769 770\quickref{CHR Implementation}{ 771CHRs suspend on the variables in the rule head. On waking the CHR 772tests if its guard is entailed by the current constraint store. The 773entailment test is efficient but incomplete, and therefore rules may 774fail to fire as early as they could in theory. 775} 776 777\section{Global Reasoning} 778\index{global reasoning} 779Constraints in {\tt ic} are handled separately and individually. More 780global consistency techniques can be achieved using global 781constraints. 782Propia and CHRs provide alternative methods of achieving more global 783consistency. 784Propia allows any subproblem to be treated as a single constraint. 785CHRs allow any set of constraints to be handled by a single rule. 786Each technique has special strengths. Propia is good for handling 787complicated logical combinations of constraints. CHRs are good for 788combining sets of constraints to extract transitive closures, and 789cliques. 790 791Both are fun to implement and use! 792 793\section{Propia and CHR Exercise} 794 795 796The problem is to implement three constraints, \verb'and', \verb'or' 797and \verb'xor' 798in CHRs and, as a separate exercise, in Propia. 799The constraints are specified as follows: 800All boolean variables have domain $\{0,1\}$: $0$ for 'false' and $1$ 801for 'true'. 802\begin{quotation} 803\noindent and(X,Y,Z) =def (X \& Y) = Z\\ 804or(X,Y,Z) =def (X or Y) = Z\\ 805xor(X,Y,Z) =def ((X \& -Y) or (-X \& Y)) = Z 806\end{quotation} 807 808Suppose your constraints are called 809\verb0cons_and0, \verb0cons_or0 and \verb0cons_xor0 810Now write enter the following procedure: 811\begin{code} 812full_adder(I1,I2,I3,O1,O2) :- 813 cons_xor(I1,I2,X1), 814 cons_and(I1,I2,Y1), 815 cons_xor(X1,I3,O1), 816 cons_and(I3,X1,Y2), 817 cons_or(Y1,Y2,O2). 818\end{code} 819The problem is solved if you enter the query: 820\begin{quote} 821\begin{verbatim} 822?- full_adder(I1,I2,0,O1,1). 823\end{verbatim} 824\end{quote} 825and get the correct answer. 826 827Note: you are not allowed to load the ic library nor to use search and 828backtracking! 829 830%HEVEA\cutend 831