Solving Simplification Ordering Constraints

Patricia Johann^{⋆} and Rolf Socher-Ambrosius^{⋆⋆}

Abstract. This paper considers the decision problem for the existential fragment of the theory of simplification orderings. A simple, polynomial-time procedure for deciding satisfiability of such constraints is given, and it is also shown that the corresponding problem for the theory of total simplification orderings is NP-complete. This latter result can be interpreted as showing that the problem of deciding whether or not a simplification ordering on first-order terms can be linearized is NP-complete.

1 Introduction

The concept of well-founded ordering is ubiquitous in automated deduction, being fundamental to the development of termination proofs — especially for term rewriting systems and other rewriting-like relations — and of deduction strategies aiming to restrict search spaces in saturation processes. In particular, it plays a central role in describing ordered rewriting, ordered resolution, and ordered superposition.

Determining the existence of critical pairs in ordered completion processes requires, and in some cases corresponds precisely to, deciding solvability of ordering constraints. In such applications, ordering constraints act as a filter prohibiting completion steps allowable in an unordered setting but inconsistent with whatever deduction strategy the particular constraints enforce. To determine that admissible completion inferences remain available, solvability of the relevant constraints must be established.

The basic constraint satisfaction problem is that of deciding, given a signature Σ and a system

Γ ≡ ⟨s_{1} > t_{1}⟩, ..., ⟨s_{n} > t_{n}⟩

of term-pairs over Σ, whether or not there exist a ground substitution σ and a well-founded ordering ≻ such that s_{i}σ ≻ t_{i}σ holds for i = 1, ..., n. Depending on Σ, two subproblems can be distinguished: constraint solving over fixed signatures, in which σ is a Σ-substitution and ≻ is an ordering on Σ-terms, and constraint solving over extended signatures, where σ and ≻ may range over arbitrary extensions of Σ. Significantly, the same system of term-pairs over Σ may manifest vastly different behavior according as it is considered over fixed or extended signatures. Given the

⋆ Fachbereich Informatik, Universität Saarbrücken, D-66123 Saarbrücken, Germany, pjohann@cs.uni-sb.de. On leave from the Department of Mathematics and Computer Science, Hobart and William Smith Colleges, Geneva, NY 14456, (315) 789-5500, johann@hws.bitnet.

⋆⋆ Max-Planck-Institut für Informatik, D-66123 Saarbrücken, Germany, (0681) 302 5367, socher@mpi-sb.mpg.de. Supported by the German Ministry for Research and Technology (BMFT) under grant ITS 9103.

signature consisting of a single constant a, for example, the system Γ ≡ ⟨x, a⟩ is unsolvable when the signature is considered fixed. But over extended signatures, a new constant b may be introduced, so that the substitution {x ↦ b}, together with any ordering ≻ such that a ≻ b, is a solution.

Each specification of a term algebra and an ordering or class of orderings gives rise to an instance of the constraint satisfaction problem. Typically, the ordering ≻ is specified as part of a given problem (so that only an appropriate substitution σ is sought), and the purely existential fragment of the resulting theory is considered (two exceptions are the studies of the Σ_{3} fragment of the theory of the subterm ordering and the Σ_{4} fragment of the theory of an arbitrary but fixed partial recursive path ordering comprising [Ven87] and [Tra90], respectively). Depending on the intended application, ≻ has been interpreted variously as any recursive path ordering (RPO) or lexicographic path ordering (LPO) based on a fixed precedence, as the subterm relation, and as the embedding relation. The satisfiability problems for the existential fragments of the most commonly considered of these theories, namely those for fixed RPOs and LPOs, are known to be decidable ([JO91], [Com90]). Venkataraman ([Ven87]) has shown that the decision problem for the existential fragment of the theory of the subterm ordering is also decidable; recently Boudet and Comon ([BC93]) proved the corresponding result for the positive existential fragment of the embedding relation. All of these decision problems are likely NPcomplete.

Although we treat a more general problem in Section 2.3, in this paper we focus on the simplification ordering (SO) constraint satisfaction problem. That is, we do not specify ≻ as part of our constraint satisfaction problems except to require that it be some arbitrary SO. Efficient techniques for deciding satisfiability of SO constraints have recently been employed to prune completion search spaces associated with theorem proving using ordering constrained clauses ([NR92]). In such settings, clauses with unsatisfiable ordering constraints may be deleted without sacrificing the refutational completeness of the resulting saturated sets of clauses.

Decidability of the SO constraint satisfaction problem over extended signatures is proved in [Pla93] by means of rather complicated techniques also establishing polynomial-time decidability of termination of ground term rewriting systems. We present in Section 2.2 a simple algorithm of the same low polynomial-time complexity as Plaisted’s for deciding solvability of SO constraint problems over extended signatures, although we do not address here the apparently much harder problem of deciding solvability of SO constraint problems over fixed signatures. We further show for the first time that if ≻ is required to be total then the decidability of ground SO constraint satisfaction is NP-complete (so that deciding satisfiability over both fixed and extended signatures is at least as hard), and derive as a corollary to the proof the fact that the problem of deciding constraint satisfaction for an arbitrary LPO is NP-complete. In light of the polynomial-time complexity of deciding SO constraint satisfaction, this result can be interpreted as showing that the problem of deciding whether or not a given SO on first-order terms over a signature can be linearized is NP-complete.

That solvability of SO constraints can be decided quickly represents the main advantage of using them, rather than more structured and specific constraints, in automated deduction. Indeed, our algorithm for extended signatures executes in a time proportional to the cube of the number of symbol occurrences in the input problem (the complexity of the SO constraint satisfaction problem over fixed signatures is not yet clear). On the other hand, SO constraint solving techniques handle many orderings simultaneously and so admit rewrite or completion steps if there is any SO permitting them, and as a result, longer sequences are possible than for RPOs and LPOs. Nonetheless, the efficiency of deciding solvability of SO constraint problems (at least over extended signatures) may in practice more than compensate for the added generality in the orderings considered and, as Plaisted observes, SO constraint solving techniques may prove useful for theorem proving applications which require the existence of a single SO consistent with all choices (as evidenced by the constraints currently under consideration) made thus far in a particular theorem proving session or rewrite sequence.

A second argument in favor of choosing SO constraints over RPO or LPO constraints in automated deduction applications is their utility in proving termination of term rewriting systems. Termination of term rewriting systems is undecidable in general, even under very restrictive assumptions on the system. A sufficient condition for a term rewriting system R to be terminating is the existence of an SO ≻ such that sσ ≻ tσ holds for all ground instances sσ → tσ of rules s → t in R. It is indeed possible that this condition is satisfied even though there exists no RPO or LPO with the required property. In such cases, the question, “Is R terminating?” can be answered in the affirmative by appealing to more general SOs.

2 Constraint Solving in Extended Signatures

Although in this paper we focus primarily on SO constraint satisfaction problems comprising pairs of the form ⟨s > t⟩, in Section 2.3 we also consider problems involving somewhat more general types of constraint pairs. Section 2.2 treats the basic SO constraint satisfaction problem discussed in the introduction. We emphasize that we are only interested in deciding SO constraint satisfaction, as opposed to finding explicit solutions for these constraint problems.

2.1 The Basic Problem

We briefly recall the basic notation used in the text. For notations not explicitly given here the reader is referred to [DJ90].

A signature is a finite set Σ of (ranked) function symbols. For each k ≥ 0, the set of function symbols in Σ of rank k is denoted Σ_{k}; the elements of Σ_{0} are called constants. A signature Σ′ is an extension of the signature Σ if Σ ⊆ Σ′, and a proper extension of Σ if Σ is a proper subset of Σ′.

Fix a countably infinite set V of variables. For each signature Σ, the set of terms (over Σ) is the smallest algebra T (Σ, V) containing V and closed under the term formation rule: from f ∈ Σ_{k} and t_{1}, ..., t_{k} ∈ T (Σ, V) infer f(t_{1}, ..., t_{k}) ∈ T (Σ, V). We write V (t) for the set of variables occurring in the term t, and denote by T (Σ) the subalgebra of ground terms (over Σ), i.e., of terms t ∈ T (Σ, V) such that V (t) = ∅. Syntactic identity between terms is denoted by ≡.

A SO (over Σ) is an ordering ≻ on the algebra T (Σ) of ground terms over Σ satisfying – i) the subterm property f(...s...) ≻ s and

– ii) the monotonicity property f(...s...) ≻ f(...t...) whenever s ≻ t

for all f(...s...), f(...t...) ∈ T (Σ). Note that SOs need not be total.

We will use transformation-based methods to solve SO constraint problems and so will represent such problems, as well as their solutions, in terms of constraint systems. Transformation-based methods attempt to reduce systems to so-called solved systems which represent their own solutions. We make these notions precise below.

A SO constraint (over Σ) is an ordered term-pair of the form ⟨s > t⟩ for s, t ∈ T (Σ, V), and an equational constraint (over Σ) is an unordered term-pair of the form ⟨s = t⟩ for s, t ∈ T (Σ, V). A constraint (over Σ) is either an SO constraint or an equational constraint over Σ; a constraint system (over Σ) is either the trivial system ⊥ or a finite set of constraints over Σ. A constraint system is pure if all of its constraints are SO constraints. We write Γ, C rather than Γ ∪ {C} if Γ is a constraint system and C is a constraint. But because such a decomposition is ambiguous — Γ may or may not contain the constraint pair C — we write Γ; C to indicate that C does not appear in Γ.

A term t ∈ T (Σ, V) occurs in Γ if it is a component of a constraint in Γ; write T (Γ) for the set of terms occurring in Γ. By V (Γ) we denote ⋃{V (t) | t ∈ T (Γ)}.

If Σ is any signature and t is any term in T (Σ, V), denote by [t] the (ordered) list (t_{1}, ..., t_{k}) of immediate subterms of t. If Γ is a constraint system, write (s_{1}, ..., s_{k}) >_{Γ} (t_{1}, ..., t_{k}) to indicate that for i = 1, ..., k either ⟨s_{i} > t_{i}⟩ ∈ Γ or s_{i} ≡ t_{i}, and that (s_{1}, ..., s_{k}) ≢ (t_{1}, ..., t_{k}).

A substitution (over Σ) is a finitely supported map from V into T (Σ, V). Any substitution σ induces a map from T (Σ, V) into itself in a natural way; we abuse notation and write σ for this extended map as well. If σ maps into T (Σ) rather than all of T (Σ, V) then σ is a ground substitution (over Σ). Substitutions are postfixed, so that tσ is the result of applying the substitution σ to the term t. By Γ σ we denote the constraint system comprising all pairs ⟨sσ ρ tσ⟩ for ⟨s ρ t⟩ ∈ Γ, ρ ∈ {>, =}.

Let Γ be a constraint system over Σ, σ be a ground substitution over Σ, and ≻ be an SO over Σ. The pair ⟨σ, ≻⟩ is a solution for Γ (over Σ) if sσ ≡ tσ for all equational constraints ⟨s = t⟩ ∈ Γ and s ≻ t for all SO constraints ⟨s > t⟩ in Γ. We define the trivial constraint system ⊥ to have no solutions.

Note that any constraint system over Σ is also a constraint system over Σ′ for any extension Σ′ of Σ, and likewise for SOs, substitutions, and hence solutions of Γ over Σ.

The following easy lemma shows that the processes of solving SO constraints and solving equational constraints can be effectively divorced.

Lemma 2.1 Let Γ be a constraint system over a signature Σ whose SO constraints and equational constraints comprise subsystems Δ and Π, respectively. If σ is a most general unifier of Π, then Γ is satisfiable iff Δσ is.

We may therefore restrict attention to pure SO constraint problems when considering the basic SO constraint satisfaction problem. We describe in Section 2.2 a procedure for solving such constraint systems over possibly extended signatures. The question our procedure answers can be stated thusly: Given a signature Σ and a (pure) constraint system Γ over Σ, do there exist a ground substitution σ over some extension Σ′ of Σ and an SO ≻ on T (Σ′) containing Γ σ?

2.2 The Procedure

We give below a set of transformations capable of transforming any (pure) constraint system Γ into a trivial or solved system and, in the latter case, determining a fragment of a SO on a finite set of terms containing appropriate instantiations of those in Γ. The key step in proving the correctness of our decision procedure for SO constraint satisfaction problems is then to see that any such fragment can be extended to a proper SO providing a solution for Γ.

Definition 2.2 The set T comprises the following transformations on constraint systems:

1. subterm

Γ ⟹ Γ; ⟨s > t⟩

if s occurs in Γ, t ∈ [s], and ⟨s > t⟩ ∉ Γ.

2. trans

Γ ⟹ Γ; ⟨s > t⟩

if there exist terms s, t and u such that ⟨s > u⟩, ⟨u > t⟩ ∈ Γ and ⟨s > t⟩ ∉ Γ.

3. lift

Γ ⟹ Γ; ⟨s > t⟩

if s and t both occur in Γ, [s] >_{Γ} [t], and ⟨s > t⟩ ∉ Γ.

Theorem 2.3 Every sequence of T -reductions terminates.

Proof. Let μ(Γ) be the number of (unordered) pairs (s, t) of distinct subterms of terms in T (Γ) which do not appear in any constraint ⟨s > t⟩ in Γ. If Γ ⟹ Γ′ by subterm, trans, or lift, then μ(Γ′) < μ(Γ). □

It is easy to check that if Γ ⟹ Γ′ by a transformation in T , then Γ is a constraint system over Σ iff Γ′ is. The soundness of the transformations in T is likewise immediate.

Lemma 2.4 The transformations in T are sound, i.e., if Γ′ is a constraint system over Σ, Γ ⟹ Γ′, and ⟨σ, ≻⟩ is a solution over an extension Σ′ of Σ for Γ′, then ⟨σ, ≻⟩ is also a solution over Σ′ for Γ.

Definition 2.5 A constraint system Γ is consistent provided it contains no constraint of the form ⟨s > s⟩, and inconsistent otherwise. A constraint system is solved if it is consistent and irreducible by T .

Every sequence of T -reductions must, by definition, terminate in a constraint system which is either solved or inconsistent. It is clear that if Γ is any inconsistent constraint system over Σ and Σ′ is any extension of Σ, then Γ has no solution over Σ′. In particular, an inconsistent constraint system Γ over Σ has no solution over Σ itself. The remainder of this subsection is devoted to showing that any solved constraint system has a solution over extended signatures.

Although an SO over Σ is by definition an ordering on the set T (Σ) of all ground terms over Σ, in the following we will have occasion to talk about SO “fragments,” i.e., orderings which are SOs when restricted to some finite set of ground terms. Call an ordering ≻ on a finite set S ⊆ T (Σ) a SO on S if i) f(...s...) ≻ s and ii) s ≻ t implies f(...s...) ≻ f(...t...) for all terms f(...s...), f(...t...) ∈ S. If ≻ is an SO on S and S′ ⊆ S, then ≻ is an SO on S′ as well.

A solved constraint system Γ determines a SO on (appropriate instantiations of) the set T (Γ) of terms occurring in Γ in a natural way:

Lemma 2.6 If Σ is a signature and Γ is a solved constraint system over Σ, then there exists an extension Σ′ of Σ, a ground substitution σ over Σ′, and an SO ≻_{Γ} on T (Γ σ) containing Γ σ.

Proof. Let Γ be a solved constraint system over Σ, let c_{x} be a new constant for every x ∈ V (Γ), and let Σ′ be the signature Σ ∪ {c_{x} | x ∈ V (Γ)}. If σ is the substitution with components {x ↦ c_{x}} for each x ∈ V (Γ), then the constraint system Γ σ is solved since Γ is, and induces a simplification ordering ≻_{Γ} on T (Γ σ). □

The next sequence of lemmas, culminating in Theorem 2.15, shows how — in the notation of Lemma 2.6 — the ordering ≻_{Γ} can be extended to an SO on all of T (Σ′). The subterm and monotonicity properties given earlier in this section extend to arbitrary binary relations in a straightforward fashion.

Definition 2.7 Let ≻ be an SO on the finite subterm closed set S ⊆ T (Σ), and suppose u ∈ T (Σ) \ S is such that [u] ⊆ S. Write ≻_{u} for the smallest transitive binary relation on S ∪ {u} containing ≻ and satisfying the subterm property and the monotonicity property. We call ≻_{u} a simple extension of ≻ by u.

For any term u, ≻ is a subrelation of ≻_{u}. We would like to see that ≻_{u} is in fact an SO. To prove this, it will be helpful to know that if s, t ∈ S and s ≻_{u} t, then s ≻ t. The next few lemmas are dedicated to obtaining this result.

Throughout the remainder of this subsection, let ≻_{u} be a simple extension of the SO ≻ on a finite subterm closed set S ⊆ T (Σ). Define a ≻_{u}-proof (from ≻) for s ≻_{u} t to be a tree P constructed according to the rules Subterm, Trans, and Lift of the inference system IT obtained by replacing all occurrences of the formal symbol > in transformations in T by the SO ≻_{u} and regarding each transformation, after this modification, as an inference rule. The nodes of P are labelled with systems of judgements of the form s ≻_{u} t, while the leaves of P are labelled with systems of judgements of the form s ≻_{u} t for which the judgements s ≻ t also hold. The tree P is constructed from its nodes by proof steps, i.e., by applications of inference rules from IT . A proof step p is critical if u occurs in some premise of p but does not appear in any of the pairs introduced by p.

Lemma 2.8 If P is any ≻_{u}-proof, then any critical step of P is of the form

Γ; ⟨s ≻_{u} u⟩; ⟨u ≻_{u} t⟩
(∗)
Γ, ⟨s ≻_{u} u⟩, ⟨u ≻_{u} t⟩, ⟨s ≻_{u} t⟩

Proof. By definition, a critical proof step cannot be a Subterm step. If the critical step p is a Lift step, then since u occurs in the premise of p, u must be a subterm of one of the terms introduced by p, contradicting the fact that that p is critical. Thus p must be a Trans step, and so it is easy to see that p must be of the form (∗). □

Definition 2.9 The proof transformation system P on ≻_{u}-proof trees is given by the rules of Figure 1.

\frac{\frac{s ≻ t  t ≻ u}{s ≻ u}  u ≻ v}{s ≻ v}  ⟹ \begin{aligned}s ≻ t  \frac{t ≻ u  u ≻ v}{t ≻ v} \\ & (P_{1}) \\ s ≻ v \end{aligned}

\frac{s ≻ u  \frac{u ≻ t  t ≻ v}{u ≻ v}}{s ≻ v} ⟹ \begin{aligned}\frac{s ≻ u  u ≻ t}{s ≻ t}  t ≻ v \\ & (P_{2}) \\ s ≻ v \end{aligned}

\frac{\frac{[s] ≻ [u]}{s ≻ u}  u ≻ t}{s ≻ t}  ⟹  \begin{aligned}s ≻ v  v ≻ t \\ & (P_{3}) \\ s ≻ t \end{aligned}

\frac{\frac{[s] ≻ [u]}{s ≻ u}  u ≻ t}{s ≻ t}  ⟹  \frac{(P_{4})}{s ≻ t}

\frac{\frac{[s] ≻ [u]}{s ≻ u} \frac{[u] ≻ [t]}{u ≻ t}}{s ≻ t}  ⟹ \frac{[s] ≻ [u]  [u] ≻ [t]}{[s] ≻ [t]} ; (P_{5}) ; s ≻ t

if t ∈ [u], t ≻ v, and v ∈ [s].

if t ∈ [u] and t ∈ [s].

Fig. 1. The proof transformation system P.

Lemma 2.10 Every sequence of applications of rules from P terminates.

Proof. Each application of a rule from P to a ≻_{u}-proof P decreases the number of occurrences of u in the tree P. □

Lemma 2.11 If the ≻_{u}-proof P is irreducible under the transformation system P, then P does not contain any critical steps.

Proof. Let P be irreducible under P and suppose contains a critical step, i.e., a step of the form (∗). The inferences s ≻_{u} u and u ≻_{u} t must both be conclusions of the inference rules Subterm, Trans, and Lift in IT ; we derive a contradiction by cases according to the rules of which they are the conclusions. If s ≻_{u} u is the conclusion of Trans, then P is reducible by P_{1}, and if u ≻_{u} t is the conclusion of Trans, then P is reducible by P_{2}. Since s ≻_{u} u cannot be the conclusion of Subterm, the only other possibility is that it is the conclusion of Lift. Since u ≻_{u} t must be the conclusion of either Lift or Subterm, two cases obtain. In the first, P is reducible by P_{5}. In the second, t must be an element of [u] and, since P contains the inference [s] ≻_{u} [u], either t is an element of [s] so that P_{4} applies to P, or else there is a subterm s′ of s such that s′ ≻_{u} t so that P_{3} applies to P. Since these considerations exhaust all possibilities, we conclude that P, being irreducible under P, can contain no critical step. □

Lemma 2.12 If ≻ is an SO on a finite subterm closed set S ⊆ T (Σ) and s, t ∈ S, then s ≻_{u} t implies s ≻ t.

Proof. We show that if s, t ∈ T (Σ) are such that s ≢ u, t ≢ u, and there exists a ≻_{u}-proof from ≻ of s ≻_{u} t, then there exists a ≻_{u}-proof from ≻ of s ≻_{u} t in which u does not appear. The result then follows easily.

If P is a ≻_{u}-proof from ≻ of s ≻_{u} t, then since P is terminating, there must exist a ≻_{u}-proof P′ from ≻ of s ≻_{u} t which is irreducible by P. By Lemma 2.11, P′ can contain no critical steps, so that s ≢ u and t ≢ u together imply that P′ does not contain any occurrence of u. □

It is now a simple matter to see that ≻_{u} is an SO:

Lemma 2.13 Let ≻ be a (total) SO on a finite subterm closed set S ⊆ T (Σ) and let u ∈ T (Σ) \ S be such that [u] ⊆ S. Then ≻_{u} is a (total) SO on S ∪ {u}.

Proof. Let ≻_{u} be the simple extension of ≻ by the term u, and assume to the contrary that ≻_{u} is not an SO. Since ≻_{u} satisfies the subterm, transitivity, and monotonicity properties, the only way ≻_{u} can fail to be a SO is if there exists a term s such that s ≻_{u} s.

If s ≢ u, then Lemma 2.12 implies that s ≻ s, which contradicts the fact that ≻ is an SO. So suppose u ≻ u and let P be a ≻_{u}-proof from ≻ of u ≻_{u} u. Clearly u ≻_{u} u cannot be the conclusion of Subterm. If it is the conclusion of Lift, then there is an immediate subterm u′ of u such that u′ ≻ u′. Since u′ ≢ u, Lemma 2.12 implies that u′ ≻ u′, again contradicting the fact that ≻ is a SO. Finally, if u ≻_{u} u is the conclusion of Trans, then there exists a term t ≢ u such that u ≻_{u} t and t ≻_{u} u. Then since ≻ satisfies the transitivity property, we must have t ≻_{u} t and hence t ≻ t, so that this case is dispensed with as above.

Finally, if ≻ is total, then the smallest ordering containing ≻_{u} and the relation t ≻_{u} u, where t is the immediate successor of the least upper bound of the elements of [u] with respect to ≻, and satisfying the transitivity and monotonicity properties, is a total SO on S ∪ {u}. □

We now see how repeated simple extensions of an SO on a finite set of ground terms can be used to specify a SO on the set of all ground terms.

Lemma 2.14 Let ≻ be a (total) SO on a finite subterm closed set S ⊆ T (Σ). Then ≻ can be extended to a (total) SO on T (Σ).

Proof. We can enumerate the elements of T (Σ) \ S in a form t_{1}, t_{2}, ... such that [t_{i}] ⊆ S ∪ {t_{1}, ..., t_{i−1}}. Define a sequence ≻_{0}, ≻_{1}, ... of SOs such that ≻_{0} is precisely ≻ and each ≻_{i}, i > 0, is the simple extension by t_{i} of the SO ≻_{i−1} on S∪{t_{1}, ..., t_{i−1}}. Finally, define a relation ≻′ on T (Σ) by declaring s ≻′ t to hold precisely when s ≻_{i} t holds for some i ≥ 0.

That ≻′ is indeed an SO can be verified as follows. If s ≻′ t and t ≻′ u for some s, t, u ∈ T (Σ), then s ≻_{i} t and t ≻_{j} u hold for some i, j ≥ 0. Thus s ≻_{k} t, t ≻_{k} u, and hence s ≻_{k} u hold, where k = max(i, j), and so s ≻′ u holds as well. Also, if s ≻′ s holds, then s ≻_{i} s holds for some i, contradicting the fact that ≻_{i} is an ordering. Thus ≻′ is itself an ordering. Similar argumentation establishes that ≻′ satisfies the subterm and monotonicity properties, and the proof that totality of ≻ implies totality of ≻′ is also straightforward. □

Theorem 2.15 For any signature Σ, any solved constraint system over Σ has a solution over some extension of Σ.

Proof. Let Γ be a solved constraint systems over Σ. Then by Lemma 2.6, there exist an extension Σ′ of Σ, a ground substitution σ over Σ′, and an SO ≻_{Γ} on T (Γ σ) ⊆ T (Σ′). By Lemma 2.14, ≻_{Γ} can be extended to an SO ≻ on all of T (Σ′) containing Γ σ. Thus ⟨σ, ≻⟩ is a solution over Σ′ for Γ. □

The results of this section yield a simple procedure for solving SO constraint problems over extended signatures. Given a constraint system Γ over Σ, we may obtain a T -irreducible system by repeated application of inference rules from T . If the resulting system Γ′ is inconsistent, then it has no solution (over fixed or extended signatures). But if Γ′ is in fact consistent, then it is by definition solved, and Theorem 2.15 guarantees the existence of a solution ⟨σ, ≻⟩ for Γ′ over some extension Σ′ of Σ. By repeated application of Lemma 2.4 we see that ⟨σ, ≻⟩ is also a solution over Σ′ for Γ.

2.3 A More General Problem

In this section we sketch some modifications that can be made to the procedure of Section 2.2 to accommodate constraint systems containing pairs of the form

⟨s ≥ t⟩, ⟨s ≯ t⟩, ⟨s ≱ t⟩, and ⟨s ≠ t⟩

in addition to those of the form ⟨s = t⟩ and ⟨s > t⟩ considered there. Although constraints of the form ⟨s ≥ t⟩ can ostensibly be handled by trading them for disjunctive constraint systems of the form ⟨s > t⟩ ∨ ⟨s = t⟩ and then transforming the resulting systems into disjunctive normal forms, such a naive approach can lead to constraint systems which grow exponentially. More importantly, it is not possible to reduce constraints of the form ⟨s ≯ t⟩ or ⟨s ≱ t⟩ to constraints involving only the equality and SO constraints of Section 2.2 if we do not require that solution orderings for SO constraint satisfaction problems be total.

We will make use of the following terminology in this subsection. An equational constraint ⟨s = t⟩ ∈ Γ is said to be solved in Γ if (at least) one of s and t is a variable occurring only once in Γ. If ⟨x = t⟩ is solved in Γ, we say that x is a solved variable of Γ. Although any pair ⟨x, y⟩ both of whose component variables appear only once in Γ determines two solved variables, we will assume that there is a uniform way of choosing which one will be considered solved, and we will consider the other to be unsolved. Any substitution θ then determines a system of solved equational constraints in a natural way; we write [θ] for such a constraint system.

A solution (over Σ) for a generalized constraint system Γ over Σ is a pair ⟨σ, ≻⟩, where σ is a ground substitution over Σ and ≻ is an SO over Σ such that

– sσ ≡ tσ holds for each pair ⟨s = t⟩ ∈ Γ,

– sσ ≻ tσ holds for each pair ⟨s > t⟩ ∈ Γ,

– sσ ≻ tσ or sσ ≡ tσ holds for each pair ⟨s ≥ t⟩ ∈ Γ,

– sσ ≢ tσ holds for each pair ⟨s ≠ t⟩ ∈ Γ,

– sσ ≻ tσ does not hold for each pair ⟨s ≯ t⟩ ∈ Γ, and

– neither sσ ≻ tσ nor sσ ≡ tσ hold for each pair ⟨s ≱ t⟩ ∈ Γ.

To appropriately modify the set T of transformations for this more general setting, we begin by defining a total ordering on the constraint symbols >, ≥, and = by declaring > to be strictly larger than ≥, which is in turn strictly larger than =. If Γ is a (generalized) constraint system over a signature Σ, then write (s_{1}, ..., s_{k}) ρ_{Γ} (t_{1}, ..., t_{k}) to indicate that

– ρ_{i} ∈ {>, ≥, =} for i = 1, ..., k,

– for some i ∈ {1, ..., k}, ρ_{i} is different from =,

– (s_{1}, ..., s_{k}) ≢ (t_{1}, ..., t_{k}), and no solved variables in Γ appear in these lists,

– either ⟨s_{i} ρ_{i} t_{i}⟩ ∈ Γ or s_{i} ≡ t_{i} for i = 1, ..., k, and

– ρ_{Γ} = max{ρ_{i} | i = 1, ..., k}.

For example, if ⟨a > b⟩, ⟨c ≥ d⟩, and ⟨e = f⟩ are in Γ, then (a, c) >_{Γ} (b, d), (c, e) ≥_{Γ} (d, f), and (a, e) >_{Γ} (b, f).

The transformation subterm requires no modification in the more general setting, but trans requires an additional clause stating that if ⟨s ρ_{1} u⟩ and ⟨u ρ_{2} t⟩ are in Γ, for ρ_{1}, ρ_{2} ∈ {>, ≥}, but ⟨s ρ_{Γ} t⟩ is not, then ⟨s ρ_{Γ} t⟩ can be added to Γ. Finally, all occurrences of “>” and “>_{Γ} ” in lift must be replaced by “ρ_{Γ}.”

By contrast with Lemma 2.1, we cannot separate equality and SO constraints in the generalized setting, due to the possibility of “cycling.” For example, ordering constraints ⟨s ≥ t⟩ and ⟨t ≥ s⟩ require that sσ ≡ tσ for any solution ⟨σ, ≻⟩ for a constraint system containing them. Moreover, certain combinations of constraints in a system Γ, e.g., ⟨s > t⟩ and ⟨s ≱ t⟩, guarantee that Γ will have no solution. We therefore introduce “bookkeeping” transformations

\begin{aligned}Γ; ⟨s > s⟩ & ⟹ & ⊥, \\ Γ; ⟨s ≠ s⟩ & ⟹ & ⊥, \\ Γ; ⟨s ≱ s⟩ & ⟹ & ⊥, \\ Γ; ⟨s > t⟩; ⟨s ≱ t⟩ & ⟹ & ⊥, \\ Γ; ⟨s ≥ t⟩; ⟨t > s⟩ & ⟹ & ⊥, \\ Γ; ⟨s ρ t⟩; ⟨s ρ̸ t⟩ & ⟹ & ⊥, \end{aligned}

where ρ is any constraint symbol. Together with T and the transformations delete, cycle, clash and unify given below, these comprise the set GT .

The transformation delete is given by

Γ; ⟨s ≥ s⟩ ⟹ Γ,

while cycle is defined by

Γ ⟹ Γ; ⟨s = t⟩,

where ⟨s ≥ t⟩ and ⟨t ≥ s⟩, or ⟨s ≥ t⟩ and ⟨s ≯ t⟩, are both in Γ, and ⟨s = t⟩ is not in Γ. unify is given by

Γ; ⟨s = t⟩ ⟹ Γ θ, [θ],

where θ is a most general unifier of s and t and ⟨s = t⟩ is not a solved pair in Γ. And clash is given by

Γ; ⟨s = t⟩ ⟹ ⊥,

where s and t are not unifiable.

It is not hard to see that every sequence of GT -reductions terminates. Let μ = ⟨μ_{1}, μ_{2}, μ_{3}, μ_{4}, μ_{5}⟩ be the well-founded lexicographic ordering on constraint systems where μ_{1}(Γ) is the number of unsolved variables in V (Γ), μ_{2}(Γ) is the number of (unordered) pairs (s, t) of distinct subterms of terms in T (Γ) not appearing in any constraint ⟨s = t⟩, μ_{3}(Γ) is the number of (unordered) pairs (s, t) of distinct subterms of terms in T (Γ) not appearing in any constraint ⟨s > t⟩ in Γ, μ_{4}(Γ) is the number of (unordered) pairs of distinct subterms (s, t) of terms in T (Γ) not appearing in any constraint ⟨s ≥ t⟩ in Γ, and μ_{5}(Γ) is the number of pairs in Γ. Then

– subterm does not increase μ_{1} or μ_{2} and decreases μ_{3},

– trans and lift do not increase μ_{1} or μ_{2}, and either decrease μ_{3} or else do not increase μ_{3} and decrease μ_{4},

– cycle does not increase μ_{1} and decreases μ_{2},

– unify decreases μ_{1}, and

– delete, clash, and the bookkeeping transformations do not increase μ_{1}, μ_{2}, μ_{3}, or μ_{4}, and decrease μ_{5}.

The GT transformations clearly preserve solutions, in the sense that if Γ ⟹ Γ′ then ⟨σ, ≻⟩ is a solution over Σ for Γ′ iff it is a solution over Σ for Γ.

A constraint system is said to be solved if it is GT -irreducible and non-trivial. Any sequence of GT -reductions out of a constraint system Γ necessarily terminates in either the trivial system or in a solved system. If the resulting GT -irreducible system is trivial, then by the previous paragraph, Γ has no solution. If the resulting GT -irreducible system is solved, then we would like to see that it, and therefore Γ, has a solution. This is precisely the upshot of the next theorem.

Theorem 2.16 Any GT -irreducible and non-trivial constraint system over a signature Σ has a solution over some extension of Σ.

Proof. Let Γ be a GT -irreducible and non-trivial constraint system over Σ, let τ be a substitution assigning to each unsolved variable x in Γ a distinct constant c_{x}, let Σ′ = Σ ∪ {c_{x} | x is unsolved in Γ }, and let

σ = τ ∪ {x ↦ tτ | ⟨x = t⟩ ∈ Γ }.

Note that Γ is solved iff Γ σ is, and that for any term s which is not a solved variable of Γ, sσ ≡ sτ. Denote by ≻_{Γ} the smallest binary relation containing sσ ≻ tσ for all pairs of terms occurring in constraints ⟨sσ > tσ⟩ or ⟨sσ ≥ tσ⟩ in Γ σ, and satisfying the subterm, monotonicity, and transitivity properties. Then since Γ σ is solved, ≻_{Γ} is an ordering on the terms occurring in pairs ⟨sσ > tσ⟩ and ⟨sσ ≥ tσ⟩ in Γ σ.

That ≻_{Γ} is an SO on the terms occurring in pairs ⟨sσ > tσ⟩ and ⟨sσ ≥ tσ⟩ in Γ σ follows from the fact that Γ σ is solved and therefore GT -irreducible.

Now, since ≻_{Γ} is an SO on the terms occurring in pairs ⟨sσ > tσ⟩ and ⟨sσ ≥ tσ⟩ in Γ σ, by the results of Section 2.2, ≻_{Γ} can be extended to a SO ≻ on all of T (Σ′). We need only show that ⟨σ, ≻⟩ is a solution over Σ′ for Γ.

– sσ ≻ tσ holds by definition of ≻ if ⟨s > t⟩ or ⟨s ≥ t⟩ is in Γ.

– if ⟨s = t⟩ ∈ Γ, then one of s and t is a solved variable in Γ and the other is a term none of whose variables are solved in Γ. If s ≡ x for some solved variable x, then tσ ≡ tτ, and therefore sσ ≡ tτ ≡ tσ.

– ⟨s ≯ t⟩ ∈ Γ (resp., ⟨s ≱ t⟩ ∈ Γ), then since Γ is GT -irreducible, ⟨sσ > tσ⟩ ∉ Γ σ (resp., ⟨sσ ≥ tσ⟩ ∉ Γ σ). Thus sσ ≻_{Γ} tσ cannot hold. On the other hand, sσ ≻ tσ cannot hold by definition of ≻ by Lemma 2.12.

– if ⟨s ≠ t⟩ ∈ Γ, then since Γ is GT -irreducible, s ≡ t cannot hold. By definition of σ, then, sσ ≢ tσ.

□

3 Complexity

In [Pla93], Plaisted shows that a procedure similar to ours for deciding satisfiability of (basic) SO constraint problems over extended signatures is of complexity O(n^{3}), n being the total number of function symbol and variable occurrences in the input constraint system. Given his proof, it is not hard to see that our procedure has precisely the same time complexity.

On the other hand, Plaisted does not at all consider the behavior of SO constraint satisfaction problems when the SOs over which they are to solved are required to be total. We prove below that the problem of deciding satisfiability of ground constraints by total SOs, whether over fixed or extended signatures, is NP-complete.

Theorem 3.1 The following problem (Total SO Constraint Solving) is NPcomplete: Given a signature Σ and a ground constraint system

Γ ≡ ⟨s_{1} > t_{1}⟩, ..., ⟨s_{n} > t_{n}⟩

over Σ, does there exist a total SO ≻ over Σ containing Γ?

Proof. The problem is easily seen to be in NP. A non-deterministic algorithm need only guess an enumeration u_{1}, u_{2}, ..., u_{m} of the set of all subterms of terms in T (Γ). Then by the results of Section 2.2, satisfiability of the ground system

Γ′ ≡ ⟨u_{1} > u_{2}⟩, ⟨u_{2} > u_{3}⟩, ..., ⟨u_{m−1} > u_{m}⟩

can be determined in polynomial time. If Γ′ is satisfiable and Γ is a subsystem of Γ′, then the results of Section 2.2 guarantee that Γ′ induces a total SO ≻ on T (Σ) containing Γ. Otherwise, the SO on T (Σ) induced by Γ′ does not provide a solution for Γ.

The rest of the proof of NP-completeness is achieved by a reduction of “Monotone 3-SAT” ([GJ79]), which is the problem of deciding satisfiability of a set C of propositional clauses of length three such that every clause C in C is positive (i.e., has only positive occurrences of propositional symbols) or negative (i.e., has only negative occurrences of propositional symbols).

The following table gives a transformation from a clause set C satisfying the assumptions of Monotone 3-SAT over the set X of propositional variables into a constraint system Γ over the signature Σ = X ∪ {f, g, 1}, where the elements of X are regarded as constants, f and g are ternary function symbols, and 1 is also a constant:

\begin{aligned}¬x ∨ ¬y ∨ ¬z & ⟹ & f(1, 1, 1) > f(x, y, z) \\ x ∨ y ∨ z & ⟹ & g(x, y, z) > g(1, 1, 1) \end{aligned}

We prove that the clause set C is satisfiable iff the constraint system Γ is satisfiable by some total SO.

First, suppose that Γ is satisfiable, i.e., that there exists a total SO ≻ over Σ containing Γ. Since ≻ is total, either x ≻ 1 or 1 ≻ x holds for every x ∈ X. Define

I = {x ∈ X | x ≻ 1}.

We show that I is an interpretation satisfying C, i.e., that if C ∈ C is positive then it contains at least one variable in I, and that if C ∈ C is negative, then it contains at least one variable not in I. If C = x ∨ y ∨ z is positive, then g(x, y, z) ≻ g(1, 1, 1). If x, y, and z are all not in I, then from 1 ≻ x, 1 ≻ y, and 1 ≻ z it follows that g(1, 1, 1) ≻ g(x, y, z), which is a contradiction. The case when C is negative is similar.

On the other hand, suppose that C is satisfiable by some interpretation I ⊆ X. Then every positive clause C in C contains an atom x ∈ I. We reorder each clause C in such a way that x is the leftmost variable of C, i.e., that C = x ∨ y ∨ z with x ∈ I. Similarly, if D is a negative clause, we write D in the form D = ¬x ∨ ¬y ∨ ¬z with x ∉ I.

Now let ≻ be a lexicographic path ordering over Σ based on any total precedence ordering ≻′ satisfying

– f ≻′ x ≻′ 1 for all x ∈ I, and

– g ≻′ 1 ≻′ y for all y ∉ I.

Such a precedence clearly exists, and it is easy to verify that for all C ∈ C the ordering ≻ satisfies the constraint system corresponding to C. Moreover, any LPO based on a total precedence is itself total on ground terms. Thus we have seen that every Monotone 3-SAT problem can be polynomially reduced to a total SO constraint satisfaction problem, and this proves the SO constraint satisfaction problem to be NP-complete. □

In light of the polynomial time complexity of the constraint satisfaction problem for arbitrary SOs, Theorem 3.1 can be interpreted as showing that the problem of deciding whether or not a given SO on a set T (Σ) of terms can be linearized — i.e., embedded into a total SO on T (Σ) — is NP-complete.

The proof of Theorem 3.1 also shows that the following similar problem (LPO Constraint Solving) is NP-complete: Given a signature Σ and a constraint system Γ over Σ, does there exist a precedence on Σ and an LPO ≻ over this precedence containing Γ? Note that this problem differs from the one treated in [Com90] and [NR92] in that in both of these papers an arbitrary but fixed precedence on Σ is assumed.

References

[BC93] A. Boudet and H. Comon. About the Theory of Tree Embedding. In Springer-Verlag LNCS 668, M.-C. Gaudel and J.-P. Jouannaud, eds., pp. 376 – 390, 1993.

[Com90] H. Comon. Solving Inequations in Term Algebras. In Proceedings of the 5th IEEE Symposium on Logic in Computer Science, pp. 62 – 29, 1990.

[DJ90] N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In Handbook of Theoretical Computer Science B, J. van Leeuwen, ed., North-Holland, 1990.

[GJ79] M. R. Garey and D. S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman and Company, 1979.

[JO91] J.-P. Jouannaud and M. Okada. Satisfiability of Systems of Ordinal Notations with the Subterm Property is Decidable. In Springer-Verlag LNCS 510, J. L. Albert, B. Monien, and M. R. Artalejo, eds., pp. 455 – 468, 1991.

[NR92] R. Nieuwenhuis and A. Rubio. Theorem Proving with Ordering Constrained Clauses. In Springer-Verlag LNCS 607, D. Kapur, ed., pp. 477 – 491, 1992.

[Pla93] D. A. Plaisted. Polynomial Time Termination and Constraint Satisfaction Tests. In Springer-Verlag LNCS 690, C. Kirchner, ed., pp. 405 – 420, 1993.

[Tra90] R. Treinen. A New Method for Undecidability Proofs for First-order Theories. Technical Report A-09/90, Universität des Saarlandes, 1990.

[Ven87] K. N. Venkataraman. Decidability of the Purely Existential Fragment of the Theory of Term Algebras. JACM 34, pp. 492 – 510, 1987.