Reification

One well-used technique in finite-domain constraint programming is called reification, which uses a new Boolean variable, B, in order 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. As an example, consider 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 rule. The reason for this is that X can never be a variable after the condition of the first rule fails and the condition of the second rule succeeds.