Reification

One well-used technique in finite-domain constraint programming is called reification, which uses a new Boolean variable B to indicate the satisfiability of a constraint C. C must be satisfied if and only if B is equal to 1. This relationship is denoted as:

    C <=> (B #= 1)

Reification is useful for implementing various global constraints, such as cardinality constraints.

It is straightforward to implement reification by using delay clauses. Consider, as an example, the reification:

    (X #= Y) <=> (B #= 1)

where X and Y are domain variables, and B is a Boolean variable. The following procedure describes the relationship:

    delay reification(X,Y,B):-
          dvar(B),dvar(X),X\==Y : {ins(X),ins(Y),ins(B)}.
    delay reification(X,Y,B):-
          dvar(B),dvar(Y),X\==Y : {ins(Y),ins(B)}.
    reification(X,Y,B):-dvar(B) : (X==Y -> B=1; B=0).
    reification(X,Y,B):-true : (B==0 -> X #\= Y; X #= Y).

Curious readers might have noticed that ins(Y) is a trigger in the first clause but ins(X) is not a trigger in the second clause. The reason is simply that ins(Y) affects the condition of the first clause but ins(X) has no effect on the condition of the second clause. X is guaranteed to be an integer when the condition of the second clause is satisfied.