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)

It is possible to use Boolean constraints to represent the relationship, but it is more efficient to implement specialized propagators to maintain the relationship. 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 describes a propagator that maintains the relationship:

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

Curious readers might have noticed that ins(Y) is in the event sequence of the first rule but ins(X) is not specified in the second one. The reason for this is that X can never be a variable after the condition of the first rule fails and that of the second rule succeeds.