A criterion for intractability of E-unification with free function symbols and its relevance for combination of unification algorithms

Abstract

All applications of equational unification in the area of term rewriting and theorem proving require algorithms for general E-unification, i.e., E-unification with free function symbols. On this background, the complexity of general E-unification algorithms has been investigated for a large number of equational theories. For most of the relevant cases, the problem of deciding solvability of general E-unification problems was found to be NP-hard. We offer a partial explanation. A criterion is given that characterizes a large class K of equational theories E where general E-unification is always NP-hard. We show that all regular equational theories E that contain a commutative or an associative function symbol belong to K. Other examples of equational theories in K concern non-regular cases as well. The combination algorithm described in [BS92] can be used to reduce solvability of general E-unification algorithms to solvability of E- and free (Robinson) unification problems with linear constant restrictions. We show that for E ∈ K there exists no polynomial optimization of this combination algorithm for deciding solvability of general E-unification problems, unless P = NP. This supports the conjecture that for E ∈ K there is no polynomial algorithm for combining E-unification with constants with free unification.