6.2.2 Normalization

A cleaning up step.

Cleaning up

The Choice Rule is the driving force behind the enumeration process: It resolves one node that keeps the constraint from being in solved form by adding additional dominance edges. However, the Choice Rule can't operate on its own. It needs some helpers that clean up after it has done its job. This cleaning work is what we call normalization .

Parent Normalization

The first kind of normalization we need to apply is necessary because X and Y above are generally leaves of bigger tree fragments. This means that an application of the Choice Rule gets us into a situation where e.g. Y has an incoming dominance edge and an incoming solid edge -- which is not allowed in a solved form:

Fortunately, we can resolve this configuration easily. The key observation is that X and Y cannot be mapped to the same node in a solution, as their parents must be different. Thus we can infer that X must dominate not just Y, but the parent of Y:

We can continue with this kind of inference; the sequence of inference steps will stop when we have deduced that X dominates the root of Y's fragment, which now doesn't have an incoming solid edge any more. We call this step parent normalization .

Redundant Edges

The other kind of normalization we need removes redundant dominance edges. A redundant dominance edge is one which we can remove from a constraint graph without losing information. For example, if we add the edge from X to Y in the Choice Rule, the old dominance edge from X to Z becomes redundant: Even when we remove it, the graph still expresses that there must be a path from X to Y and a path from Y to Z, so there must of course also be a path from X to Z. Here are the solutions of our example constraint without the unnecessary edges:

We call the operation of removing unnecessary dominance edges redundancy elimination . Redundancy elimination can be done quite efficiently using a standard graph algorithm called transitive reduction.

?- Question!

It's important that we always apply parent normalization before redundancy elimination. Can you tell why?


Aljoscha Burchardt, Stephan Walter, Alexander Koller, Michael Kohlhase, Patrick Blackburn and Johan Bos
Version 1.2.5 (20030212)