Instead of merely posting constraints it is often useful to reflect its truth value into a 0/1-variable B, so that:
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
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).