15.7 Reified Constraints

A reified constraint consists of a constraint and a variable which denotes its truth value. For instance, is equivalent to . Refied constraints are useful for for expressing propositional formulas over constraints. Most typically, they are used for expressing implications or equivalences between arbitrary constraints and .

Oz provides reified versions of most finite domain constraints and some set constraints directly. Reified versions of arbitrary constraints can be user defined in Oz by or-propagators. The only restriction is that the negation has to be available.

  truth(C)=N    iff  N :: 0#1
                     thread 
                        or C    N=1  
                        [] NotC N=0  
                        end 
                     end

Propagation of reified constraints is bidirectional. For instance, propagates into the global constraint store, whereas propagates . Syntactically, reification is written in Oz by paranthesis only. It looks like as if the word were ommited. A typical example it the implication which can be written as follows.

declare B A  
[B A]::: 1#27
(B =: 1) =<: (A :: 2#4)
 
{Browse [B A]}
/*
B=1
*/

Alternatively, you may also use the special procedure FD.impl which expresses implication for Boolean variables.

declare B A  
[B A]::: 1#27
{FD.impl (B =: 1) (A :: 2#4)}
 
{Browse [B A]}
/*
B=1
*/

Via reification and arithmetics, one can express disjunctions between arbitrary constraints for which reification is provided. The logical content of the disjunctive propagator and the reified constraint are equal. Operationally however, both propagators differ significantly. Reification tests all constraints in isolation for satisfiablity with respect to the global constraint store, whereas the corresponding disjunctive propagator tests the whole conjunctions .