5.9 0/1 Propagators

Using the mapping from 0 and 1 to the truth values false and true, respectively, logical connectives between finite domain integers are defined. If at most one argument is a free variable, it will be constrained to a finite domain integer in . Such a finite domain integer is also called a 0/1-integer. The propagators exploit equality and may also post equality between variables.

The operational semantics is detailed only for FD.conj. For the remaining propagators, the operational semantics is defined accordingly, exploiting as much information as possible (including coreferences).

conj

{FD.conj $D1 $D2 $D3}

D3 is the conjunction of D1 and D2. The operational semantics can be described by the following code

[D1 D2 D3] ::: 0#1
cond D1=0  then D3=0             
[]   D1=1  then D2=D3            
[]   D2=0  then D3=0             
[]   D2=1  then D1=D3            
[]   D3=1  then D1=1 D2=1    
[]   D1=D2 then D1=D3           
end

disj

{FD.disj $D1 $D2 $D3}

D3 is the disjunction of D1 and D2.

exor

{FD.exor $D1 $D2 $D3}

D3 is the exclusive disjunction of D1 and D2.

nega

{FD.nega $D1 $D2}

D2 is the negation of D1.

impl

{FD.impl $D1 $D2 $D3}

D3 is the implication of D2 by D1 (``'').

equi

{FD.equi $D1 $D2 $D3}

D3 is the equivalence of D1 by D2 (``'').