Node:Reified Constraints, Previous:A Constraint Satisfaction Problem, Up:CLPFD Interface

Reified Constraints

Instead of merely posting constraints it is often useful to reflect its truth value into a 0/1-variable B, so that:

• the constraint is posted if B is set to 1
• the negation of the constraint is posted if B is set to 0
• B is set to 1 if the constraint becomes entailed
• B is set to 0 if the constraint becomes disentailed

This mechanism is known as reification. Several frequently used operations can be defined in terms of reified constraints, such as blocking implication [Saraswat 90] and the cardinality operator [Van Hentenryck & Deville 91], to name a few. A reified constraint is written:

| ?- Constraint #<=> B.

where Constraint is reifiable. As an example of a constraint that uses reification, consider exactly(X,L,N), which is true if X occurs exactly N times in the list L. It can be defined thus:

exactly(_, [], 0).
exactly(X, [Y|L], N) :-
    X #= Y #<=> B,
    N #= M+B,
    exactly(X, L, M).