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.
Type de document :
Article dans une revue
Information and Computation, Elsevier, 2000, 162 (1-2), pp.24-42
Liste complète des métadonnées

Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:51:57
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58


  • HAL Id : inria-00099222, version 1



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〉



Consultations de la notice