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 x and y:

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 x.


Denys Duchier
Version 1.2.0 (20010221)