Previous Up Next

15.5  A Complete Example of a CHR File

Sometimes whole sets of constraints can be combined. Consider, for example, a program where disequalities on pairs of variables are accumulated during search. Whenever a point is reached where any subset of the variables are all constrained to be different an alldifferent constraint can be posted on that subset, thus supporting more powerful propagation. This can be achieved by finding cliques in the graph whose nodes are variables and edges are disequality constraints.

We start our code with a declaration to load the ech library. The constraints are then declared, and subsequently defined by rules. The CHR encoding starts by generating a clique whenever two variables are constrained to be different. 

:- lib(ech).
:- constraints neq/2.

neq(X,Y) ==>
    sort([X,Y],List),
    clique(List),
    neq(Y,X).

Each clique is held as a sorted list to avoid any duplication. The symmetrical disequality is added to simplify the detection of new cliques, below. Whenever a clique is found, the alldifferent constraint is posted, and the CHRs seek to extend this clique to include another variable: 

:- constraints clique/1.

clique(List) ==> alldifferent(List).
clique(List),neq(X,Y) ==>
    in_clique(Y,List), not in_clique(X,List) |
    sort([X|List],Clique),
    extend_clique(X,List,Clique).

in_clique(Var,List) :-
    member(El,List), El==Var, !.

The idea is to search the constraint store for a disequality between the new variable X and each other variable in the original clique. This is done by recursing down the list of remaining variables. When there are no more variables left, a new clique has been found. 

neq(X,Y) \ extend_clique(X,[Y|Tail],Clique) <=>
    extend_clique(X,Tail,Clique).
extend_clique(_,[],Clique) <=> 
    clique(Clique).

Finally, we add three optimisations. Don’t try and find a clique that has already been found, or find the same clique twice. If the new variable is equal to a variable in the list, then don’t try any further. 

clique(Clique) \ extend_clique(_,_,Clique) <=> true.
extend_clique(_,_,Clique) \ extend_clique(_,_,Clique) <=> true.
extend_clique(Var,List,_) <=> in_clique(Var,List) | true.

15.5.1  CHR Implementation

CHR’s are implemented using the ECLiPSe suspension and waking mechanisms. A rule is woken if:

The rule cannot fire unless the goal is more instantiated than the rule head. Thus the rule p(a,f(Y),Y) <=> q(Y) is really a shorthand for the guarded rule: 

p(A,B,C) <=> A=a, B=f(Y), C=Y | q(Y)

The guard is “satisfied” if, logically, it is entailed by the constraints posted already.

In practice the CHR implementation cannot always detect the entailment. The consequence is that goals may fire later than they could. For example consider the program 

:- constraints p/2.
p(X,Y) <=> ic:(X $> Y) | q(X,Y).

and the goal 

?-  ic:(X $> Y),
    p(X,Y).

Although the guard is clearly satisfied, the CHR implementation cannot detect this and p(X,Y) does not fire. If the programmer needs the entailment of inequalities to be detected, it is necessary to express inequalities as CHR constraints, which propagate ic constraints as illustrated in the example prec(S1,D,S2) above.

CHRs can detect entailment via variable bounds, so p(X,0) does fire in the following example: 

?-  ic:(X $> 1),
    p(X,0).

The implementation of this entailment test in ECLiPSe is to impose the guard as a constraint, and fail (the entailment test) as soon as any variable becomes more constrained. A variable becomes more constrained if:

There are many examples of applications expressed in CHR in the ECLiPSe distribution. They are held as files in the chr subdirectory of the standard ECLiPSe library directory lib.

CHRs suspend on the variables in the rule head. On waking the CHR tests if its guard is entailed by the current constraint store. The entailment test is efficient but incomplete, and therefore rules may fail to fire as early as they could in theory.
Figure 15.6: CHR Implementation
Previous Up Next