A constraint is satisfiable iff it has a solution. Not all constraints are satisfiable. For example, the constraint c_{1} c_{2} is unsatisfiable, because for all assignments the denotation of c_{1} will be the feature graph (c_{1},) and the denotation of c_{2} will be (c_{2},) which is not the same graph. Clearly a constraint may also define such a clash indirectly, as in the constraint:
The problem whether a constraint is satisfiable is decidable.
Algorithms deciding satisfiability for more powerful feature logics
(extending the current logic with disjunction and negation) are for
example presented in [39], [89]. The
present algorithm is an adaptation to
of the algorithm
presented in [89]. The algorithm consists of a number
of simplification rules. Rules are applied until no rules can be
applied anymore. In that case the constraint is said to be in normal
form or normal. For normal constraints it is trivial to check
whether the constraint is satisfiable (clash-free). A constraint is
solved iff it is normal and clash-free.
The simplification algorithm is presented here in two steps. Firstly, I show how to remove all complex paths (paths containing more than one label), by the introduction of some new variables. The resulting constraint, which is 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.
A basic constraint is a constraint in which each equation has one of the following forms:
An arbitrarily constraint
can be mapped into a basic constraint
by the introduction of new variables.
is satisfiable
iff
is. We will say that two assignments agree on a set
of variables iff they assign the same elements in
the domain to these variables.
In the following, C is a constraint, [X| s]C is the constraint obtained from C by replacing each occurrence of variable X with s.
Apply any of the rules, until the rules are not applicable:
Each step of the algorithm preserves satisfiability, hence a sequence of steps preserves satisfiability as well. Step 1 of the algorithm changes a constraint into . It is straightforward to show that is V-equivalent with (and hence is satisfiable iff is). Assume that , then let be the assignment which is exactly like , except that the newly introduced X_{i} is mapped to the feature graph (s)^{l1...l}_{n-1}. Clearly, . The other way around is similar. The same reasoning applies for the steps 2 and 3.
This constraint is simplified, according to the rules above, in the
following three steps, using respectively rule 1, 2 and 3:
Given a basic constraint, the following simplification rules rewrite this constraint into its equivalent normal form.
To show that a normal form of a constraint C computed by this algorithm is equivalent to C observe that each of the simplification rules preserves equivalence. In the first rule the variable X is `isolated'; in the rest of the constraint the variable is replaced by the constant or variable it is equated with. Clearly in this case and are equivalent, because, by definition (X) = (s), hence C^{} = C[X| s]^{}. As for the third rule, note that the solutions of {Xl s,Xl t} are those assignments such that the descriptors Xl, s, t have the same denotation. The same is the case for the solutions of {Xl s, s t}. Hence the third rule preserves equivalence. The second rule and the fourth rule clearly preserve equivalence.
Furthermore, the simplification algorithm always terminates, because clearly there cannot be an infinite sequence of simplification rules starting from any basic constraint . To see this, note that there is only a finite number of variables in a given constraint. The first rule `isolates' such a variable, hence this rule can be applied at most once for each variable; furthermore none of the other rules introduce new variables. The second rule can only be applied a finite number of cases because the number of constants is also finite, and not increased by any of the other rules. The third rule can only be applied a finite number of times because it reduces the length of the paths in a constraint; none of the other rules increase this length. The final rule can only be applied a finite number of times because it reduces the number of equations in a constraint, and none of the other rules increases this number.
The simplification algorithm is very similar to the `unification' algorithms based on the simplification rules for a system of term equations as presented for example in [5]. Note though that this system does not contain an `occur check' as I did not exclude cyclic structures.
A normal constraint is clash-free if it does not contain any of the following constraints:
where
is the transitive and reflexive closure of
which is a binary relation on the variables
occurring in :
This constraint can then be rewritten into normal form, for example in the following steps, using the rules 3, 1, 3 and 1 of definition 8. The application of the rules 2 and 4 are performed implicitly in the example (for simplicity).
The principal solution
of this constraint is defined as follows:
The first two assignments (X_{0}) and (X_{1}) can be illustrated as:
The matrix representation of a constraint on a variable is best introduced using an example. For the result of example 9, the matrix representation for the constraints on variable X_{0} looks as follows:
The names of variables only matter in case they are referred to
more than once. In the foregoing example, I therefore omit
the variables and instead write:
As another example of this notation, consider the following constraint:
The matrix representation of the constraints on
X_{0} looks
as follows:
Usually an empty feature structure will not be shown explicitly, but instead only the corresponding
variable will be shown, i.e. instead of
I write
Furthermore, I use a special notation for parts of such matrices that are used to encode lists and difference lists. If no confusion arises I use the HPSG [69] convention of writing a list within angled brackets, where the comma separates elements of the list, and the vertical bar may be used to separate the head from the tail of the list. In path equations the elements of such lists are referred to with attributes f and r (for first and rest), the empty list is represented with the constant . In case of difference lists I moreover write the `out' part of the difference list right after the `in'-part, separated by `-'. The attributes in and out are used in path equations to refer to these parts. Moreover, in case of a difference list where the tail of the `in' part is reentrant with the `out' part, I simply write the `in' list within `` ''. As an example I write ``letters from mexico get lost'' for letters, from, mexico, get, lost|X_{1} - X_{1}.
As a further abbreviation I sometimes use the functor-argument notation for semantic structures, as introduced in section 1.2.3. Using these abbreviations, the foregoing constraint is written as: