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
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
When there are no more variables left, a new clique has been found.
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.
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
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
CHRs can detect entailment via variable bounds, so
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.