6.8 Reified Constraints

There are often cases when, instead of imposing a constraint , we want to speak (and possibly constrain) its truth value. Let's take an example from Chapter 5: the cardinality of a daughter set $\rho(w)$ is at most 1, and it is 1 iff $\rho$ is required by 's valency, i.e if $\rho\in\Feature{comps}(w)$ . Let b_1 stand for the truth value of $|\rho(w)|=1$ and b_2 stand for the truth value of $\rho\in\Feature{comps}(w)$ :

$\begin{array}{l@{\quad\equiv\quad}l} b_1&|\rho(w)|=1\\ b_2&\rho\in\Feature{comps}(w) \end{array}$

The well-formedness condition mentioned above is expressed simply by b_1=b_2 .

For the purpose of this section, we will write $B\equiv C$ to represent a reified constraint, where is a FD variable representing the truth value of constraint : 0 means false, 1 means true. The operational semantics are as follows:

if is entailed then is inferred
if is inconsistent then is inferred
if is entailed, then is imposed
if is entailed, then $\neg C$ is imposed

For example, here is how reified constraints can express that exactly one of C_1 , C_2 , and C_3 must hold:

$\begin{array}{l} B_1\equiv C_1\\ B_2\equiv C_2\\ B_3\equiv C_3\\ B_1+B_2+B_3 = 1 \end{array}$

Similarly, here is how to express $C_1\Rightarrow C_2$ :

$\begin{array}{l} B_1\equiv C_1\\ B_2\equiv C_2\\ B_1\leq B_2 \end{array}$

The astute reader may wonder ``why do we need a new concept? can't we express reified constraints in terms of disjunctive propagators?''. Indeed, $B\equiv C$ can also be written:

or B=1 C [] B=0 ~C end

where somehow ~C is intended to represent the negation of C. What makes reified constraints attractive is that they are much more efficient. A disjunctive propagator needs to create 2 nested spaces, but a reified constraint doesn't need any.

In the libraries of the Mozart system, many constraints are also available as reified constraints (but not all). For example:

{FS.reified.include I S B}

B represents the truth value of {FS.include I S}. If B=0, the reified constraint reduces to {FS.exclude I S}.