6.1.4 Defining Solved Forms

Defining Solved Forms

Summing up, we say that a constraint graph is in solved form if it has certain properties that guarantee its satisfiability and make it trivial to enumerate its solutions. The solved forms of a constraint are constraints in solved form that each represent a class of solutions of the original constraint that have only "irrelevant" differences. Every solution of the original constraint is a solution of one of the solved forms; and vice versa.

Let us now define what a solved form is. A constraint graph is in solved form if:

1. It has no cycles that use only solid and dominance edges.

2. It has no node with two incoming edges that are solid or dominance.

You can easily verify that if you disregard the binding edges, every graph in solved form is a tree. As it is forbidden that a node with a node label has an outgoing dominance edge in a constraint graph, you get a tree that consists of the little tree fragments of the original constraint, with dominance edges going from (unlabeled) leaves to roots.

From Solved Forms to Solutions

Now how do we get from a solved form to an actual solution? As we have already said, this step is going to be quite trivial. In general, there are two cases we have to distinguish:

1. If we're lucky, the solved form will not contain any nodes with two outgoing dominance edges anyway. In this case, we can simply identify the endpoints of each dominance edge, and we obtain a minimal -structure that satisfies the solved form. As it happens, all of the solved forms we'll get for underspecified semantics will belong to this class.

2. Otherwise, we could do the same operation as in Section 5.2.9: For each node with more than one outgoing dominance edge, we add an arbitrary node label, and make the dominance children real children over solid edges.

As you can see, it's always possible to construct a rather small solution to a solved form very easily. In particular, you know that solved forms are always satisfiable.