Skip to Main content Skip to Navigation
Journal articles

Unification Algorithms Cannot Be Combined in Polynomial Time

Miki Hermann 1 Phokion G. Kolaitis 2
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We establish that there is no polynomial-time general combination algorithm for unification in finitary equational theories, unless the complexity class #P of counting problems is contained in the class FP of function problems solvable in polynomial-time. The prevalent view in complexity theory is that such a collapse is extremely unlikely for a number of reasons, including the fact that the containment of #P in FP implies that P = NP. Our main result is obtained by establishing the intractrability of the counting problem for general AG-unification, where AG is the equational theory of Abelian groups. More specifically, we show that computing the cardinality of a minimal complete set of unifiers for general AG-unification is a #P-hard problem. In contrast, AG-unification with constants is known to be solvable in polynomial time. Since an algorithm for general AG-unification can be obtained as a combination of a polynomial-time algorithm for AG-unification with constants and a polynomial-time algorithm for syntactic unification, it follows that no polynomial-time general combination algorithm exists, unless #P is contained in FP. This implication of our main results holds not only for the combination of unification algorithms, but for the combination of constraint solvers as well. We also show that the counting problem for Boolean ring unification is #P-hard; this gives a lower bound on the performance of all algorithms for general BR-unification.
Document type :
Journal articles
Complete list of metadata

https://hal.inria.fr/inria-00099222
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 8:51:57 AM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM

Identifiers

  • HAL Id : inria-00099222, version 1

Collections

Citation

Miki Hermann, Phokion G. Kolaitis. Unification Algorithms Cannot Be Combined in Polynomial Time. Information and Computation, Elsevier, 2000, 162 (1-2), pp.24-42. ⟨inria-00099222⟩

Share

Metrics

Record views

151