2.1.6. Reification view

Suppose we want to associate a 0-1 domain variable b to a constraint π’ž and maintain the equivalence bβ‰‘π’ž. This is called the reification of π’ž. For most global constraints this can be achieved by reformulating the global constraint as a conjunction of pure functional dependency constraints together with constraints that can be easily reified, e.g.Β linear constraints involving at most two variablesΒ [BeldiceanuCarlssonFlenerPearson13].

We can reify the πšŠπš•πš•πšπš’πšπšπšŽπš›πšŽπš—πš(〈x 1 ,x 2 ,β‹―,x n βŒͺ) constraint by using the idea of sorting its variables (i.e., the pure functional dependency part) and by stating that within the sorted list of variables adjacent variables are in strictly increasing order. This leads to the following expression πšœπš˜πš›πš(〈x 1 ,x 2 ,β‹―,x n βŒͺ,〈y 1 ,y 2 ,β‹―,y n βŒͺ) ∧ (y 1 <y 2 ∧y 2 <y 3 βˆ§β‹―βˆ§y n-1 <y n )≑b.