4.3.1 Well-Formedness Constraints

Consider a solution tree for a description $\phi$ . Further consider the node $\NODE{x}$ , in that tree, interpreting variable occurring in $\phi$ . When observed from the vantage point of this node, the nodes of the tree (hence the variables that they interpret) are partitioned into 4 regions: $\NODE{x}$ itself, all nodes above, all nodes below, and all nodes to the side (i.e. in disjoint subtrees).

The variables of $\phi$ are correspondingly partitioned: all variables that are also interpreted by $\NODE{x}$ , all variables interpreted by the nodes above, resp. below or to the side. We introduce 4 variables to denote these sets:

$\EQV{x}, \UPV{x}, \DOWNV{x}, \SIDEV{x}$

Clearly, is one of the variables interpreted by $\NODE{x}$ :

$x\in \EQV{x}$

Furthermore, as described above, these sets must form a partition of the variables occurring in $\phi$ :

$\VARS(\phi) = \EQV{x}\uplus\UPV{x}\uplus\DOWNV{x}\uplus\SIDEV{x}$

Characteristic Set Constraints

Well-Formedness Clauses

Disjunctive Propagator