next up previous contents
Next: Readable Notation Up: The Constraint Language Previous: Feature Graphs

Interpretation of Constraints

An interpretation tex2html_wrap_inline10723 of consists of a domain DI which is the set of all feature graphs, and an interpretation function .I (see definition 1). Variables and constants will denote feature graphs, relative to some assignment.

The denotation of a variable X with respect to an assignment tex2html_wrap_inline11287 is simply tex2html_wrap_inline11289 . The denotation of a constant C is the feature graph (c, tex2html_wrap_inline11121 ) (for any assignment). The denotation of a descriptor sp is the subgraph at path p of the graph denoted by s.

An interpretation tex2html_wrap_inline10723 satisfies an atomic constraint tex2html_wrap_inline10987 relative to an assignment tex2html_wrap_inline11287 , if the descriptors are both defined and the same, i.e., tex2html_wrap_inline11309 tex2html_wrap_inline10987 iff tex2html_wrap_inline11313 = tex2html_wrap_inline11315

A constraint is called satisfiable if it has a solution, and two constraints tex2html_wrap_inline10669 and tex2html_wrap_inline10795 are called equivalent if they have the same solutions, i.e., if tex2html_wrap_inline11321 . Clearly, not all constraints are satisfiable. For example, the constraint tex2html_wrap_inline11323 is not satisfiable, since both denote different graphs for all assignments.

The problem of whether a constraint is satisfiable is decidable. For example in [Smolka1992] an algorithm for a more powerful feature logic is presented. In [VanNoord1993] a decidable algorithm for the constraint language is presented, which we briefly summarize in the next paragraph.

Satisfiability of a constraint tex2html_wrap_inline10669 is shown by transforming tex2html_wrap_inline10669 into a constraint of a specific form, called the normal form. This transformation is performed in two steps. Firstly, all complex paths (paths containing more than one label) are removed by introduction of some new variables. The resulting constraint (also called basic) is shown to be satisfiable iff the original constraint was. The next step then rewrites constraints without complex path expressions into normal form.

If the resulting normal constraint is clash free, i.e., if it does not contain any constraints of the following form:

then it is called a solved clause. A solved clause C is of the form tex2html_wrap_inline11335 or tex2html_wrap_inline11337 .




next up previous contents
Next: Readable Notation Up: The Constraint Language Previous: Feature Graphs

Guenter Neumann
Mon Oct 5 14:01:36 MET DST 1998