4.3.2 Problem-Specific Constraints

The well-formedness constraints guarantee that our solved forms correspond to trees. We now need additional constraints to guarantee that these trees actually satisfy our description $\phi$ . We shall achieve this by translating each literal in $\phi$ into a constraint as explained below.

If the constraint is of the form $x\mathbin{R}y$ , then the translation is trivial in terms of the variable $R_{xy}$ that we introduced earlier to denote the relationship between and :

$R_{xy}\in R$

If the constraint is $x:f(x_1,\ldots,x_n)$ , then it is translated into the constraints below:

$\begin{array}{r@{{}={}}l} \DOWNV{x}&\EQDOWNV{x_1}\uplus\ldots\uplus\EQDOWNV{x_n}\\ \EQUPV{x}&\UPV{x_i}\qquad\text{forall }1\leq i\leq n\\ \DTRSV{x}&f(\NODE{x_1},\ldots,\NODE{x_n}) \end{array}$

Particularly important is the first constraint which states that the trees rooted at the daughters are pairwise disjoint and that they exhaustively account for the variables below .