2.1.6. Reification view

Suppose we want to associate a 0-1 domain variable $b$ to a constraint $𝒞$ and maintain the equivalence $b\equiv 𝒞$. 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 $\mathrm{𝚊𝚕𝚕𝚍𝚒𝚏𝚏𝚎𝚛𝚎𝚗𝚝}$$\left(\langle x_1,x_2,\cdots ,x_n\rangle \right)$ 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 $\mathrm{𝚜𝚘𝚛𝚝}$$(\langle x_1,x_2,\cdots ,x_n\rangle ,\langle y_1,y_2,\cdots ,y_n\rangle )\wedge (y_1<y_2\wedge y_2<y_3\wedge \cdots \wedge y_{n-1}<y_n)\equiv b$.