Unification Algorithms Cannot Be Combined in Polynomial Time
Identifieur interne : 005044 ( Hal/Corpus ); précédent : 005043; suivant : 005045Unification Algorithms Cannot Be Combined in Polynomial Time
Auteurs : Miki Hermann ; Phokion G. KolaitisSource :
- Information and Computation [ 0890-5401 ] ; 2000.
English descriptors
- mix :
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.
Url:
Links to Exploration step
Hal:inria-00099222Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Unification Algorithms Cannot Be Combined in Polynomial Time</title><author><name sortKey="Hermann, Miki" sort="Hermann, Miki" uniqKey="Hermann M" first="Miki" last="Hermann">Miki Hermann</name><affiliation><hal:affiliation type="researchteam" xml:id="struct-2360" status="OLD"><idno type="RNSR">199221357D</idno><orgName>Constraints, automatic deduction and software properties proofs</orgName><orgName type="acronym">PROTHEO</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/protheo</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation><relation active="#struct-2496" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation></affiliation></author><author><name sortKey="Kolaitis, Phokion G" sort="Kolaitis, Phokion G" uniqKey="Kolaitis P" first="Phokion G." last="Kolaitis">Phokion G. Kolaitis</name><affiliation><hal:affiliation type="laboratory" xml:id="struct-82231" status="VALID"><orgName>Department of Computer Science [Calgary]</orgName><orgName type="acronym">CPSC</orgName><desc><address><addrLine>University of Calgary 2500 University Dr. NW Calgary, Alberta Canada T2N 1N4</addrLine><country key="CA"></country></address><ref type="url">http://www.cpsc.ucalgary.ca/</ref></desc><listRelation><relation active="#struct-106219" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-106219" type="direct"><org type="institution" xml:id="struct-106219" status="VALID"><orgName>University of Calgary</orgName><desc><address><addrLine>2500 University Dr NW Calgary, Alberta, T2N 1N4</addrLine><country key="CA"></country></address></desc></org></tutelle></tutelles></hal:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:inria-00099222</idno><idno type="halId">inria-00099222</idno><idno type="halUri">https://hal.inria.fr/inria-00099222</idno><idno type="url">https://hal.inria.fr/inria-00099222</idno><date when="2000">2000</date><idno type="wicri:Area/Hal/Corpus">005044</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Unification Algorithms Cannot Be Combined in Polynomial Time</title><author><name sortKey="Hermann, Miki" sort="Hermann, Miki" uniqKey="Hermann M" first="Miki" last="Hermann">Miki Hermann</name><affiliation><hal:affiliation type="researchteam" xml:id="struct-2360" status="OLD"><idno type="RNSR">199221357D</idno><orgName>Constraints, automatic deduction and software properties proofs</orgName><orgName type="acronym">PROTHEO</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/protheo</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation><relation active="#struct-2496" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation></affiliation></author><author><name sortKey="Kolaitis, Phokion G" sort="Kolaitis, Phokion G" uniqKey="Kolaitis P" first="Phokion G." last="Kolaitis">Phokion G. Kolaitis</name><affiliation><hal:affiliation type="laboratory" xml:id="struct-82231" status="VALID"><orgName>Department of Computer Science [Calgary]</orgName><orgName type="acronym">CPSC</orgName><desc><address><addrLine>University of Calgary 2500 University Dr. NW Calgary, Alberta Canada T2N 1N4</addrLine><country key="CA"></country></address><ref type="url">http://www.cpsc.ucalgary.ca/</ref></desc><listRelation><relation active="#struct-106219" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-106219" type="direct"><org type="institution" xml:id="struct-106219" status="VALID"><orgName>University of Calgary</orgName><desc><address><addrLine>2500 University Dr NW Calgary, Alberta, T2N 1N4</addrLine><country key="CA"></country></address></desc></org></tutelle></tutelles></hal:affiliation></affiliation></author></analytic><series><title level="j">Information and Computation</title><idno type="ISSN">0890-5401</idno><imprint><date type="datePub">2000</date></imprint></series></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>#p-difficulte</term><term>#p-hardness</term><term>algorithme d'unification</term><term>combination method</term><term>fp</term><term>methode de combinaison</term><term>unification algorithm</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">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.</div></front></TEI><hal api="V3"><titleStmt><title xml:lang="en">Unification Algorithms Cannot Be Combined in Polynomial Time</title><author role="aut"><persName><forename type="first">Miki</forename><surname>Hermann</surname></persName><email>hermann@loria.fr</email><idno type="halauthor">129696</idno><orgName ref="#struct-441569"></orgName><affiliation ref="#struct-2360"></affiliation></author><author role="aut"><persName><forename type="first">Phokion G.</forename><surname>Kolaitis</surname></persName><email></email><idno type="halauthor">130182</idno><orgName ref="#struct-364599"></orgName><affiliation ref="#struct-82231"></affiliation></author><editor role="depositor"><persName><forename>Publications</forename><surname>Loria</surname></persName><email>publications@loria.fr</email></editor></titleStmt><editionStmt><edition n="v1" type="current"><date type="whenSubmitted">2006-09-26 08:51:57</date><date type="whenModified">2016-05-19 01:09:31</date><date type="whenReleased">2006-09-28 15:22:46</date><date type="whenProduced">2000</date></edition><respStmt><resp>contributor</resp><name key="108626"><persName><forename>Publications</forename><surname>Loria</surname></persName><email>publications@loria.fr</email></name></respStmt></editionStmt><publicationStmt><distributor>CCSD</distributor><idno type="halId">inria-00099222</idno><idno type="halUri">https://hal.inria.fr/inria-00099222</idno><idno type="halBibtex">hermann:inria-00099222</idno><idno type="halRefHtml">Information and Computation, Elsevier, 2000, 162 (1-2), pp.24-42</idno><idno type="halRef">Information and Computation, Elsevier, 2000, 162 (1-2), pp.24-42</idno></publicationStmt><seriesStmt><idno type="stamp" n="INRIA">INRIA - Institut National de Recherche en Informatique et en Automatique</idno><idno type="stamp" n="CNRS">CNRS - Centre national de la recherche scientifique</idno><idno type="stamp" n="INPL">Institut National Polytechnique de Lorraine</idno><idno type="stamp" n="LORIA2">Publications du LORIA</idno><idno type="stamp" n="INRIA-NANCY-GRAND-EST">INRIA Nancy - Grand Est</idno><idno type="stamp" n="LORIA-FM" p="LORIA">Méthodes formelles</idno><idno type="stamp" n="LORIA">LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications</idno><idno type="stamp" n="UNIV-LORRAINE">Université de Lorraine</idno><idno type="stamp" n="INRIA-LORRAINE">INRIA Nancy - Grand Est</idno><idno type="stamp" n="LABO-LORIA-SET" p="LORIA">LABO-LORIA-SET</idno></seriesStmt><notesStmt><note type="commentary">Article dans revue scientifique avec comité de lecture.</note><note type="audience" n="1">Not set</note><note type="popular" n="0">No</note><note type="peer" n="1">Yes</note></notesStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Unification Algorithms Cannot Be Combined in Polynomial Time</title><author role="aut"><persName><forename type="first">Miki</forename><surname>Hermann</surname></persName><email>hermann@loria.fr</email><idno type="halAuthorId">129696</idno><orgName ref="#struct-441569"></orgName><affiliation ref="#struct-2360"></affiliation></author><author role="aut"><persName><forename type="first">Phokion G.</forename><surname>Kolaitis</surname></persName><idno type="halAuthorId">130182</idno><orgName ref="#struct-364599"></orgName><affiliation ref="#struct-82231"></affiliation></author></analytic><monogr><idno type="localRef">A00-R-358 || hermann00a</idno><idno type="halJournalId" status="VALID">14180</idno><idno type="issn">0890-5401</idno><idno type="eissn">1090-2651</idno><title level="j">Information and Computation</title><imprint><publisher>Elsevier</publisher><biblScope unit="volume">162</biblScope><biblScope unit="issue">1-2</biblScope><biblScope unit="pp">24-42</biblScope><date type="datePub">2000</date></imprint></monogr></biblStruct></sourceDesc><profileDesc><langUsage><language ident="en">English</language></langUsage><textClass><keywords scheme="author"><term xml:lang="en">#p-difficulte</term><term xml:lang="en">unification algorithm</term><term xml:lang="en">#p-hardness</term><term xml:lang="en">fp</term><term xml:lang="en">combination method</term><term xml:lang="en">methode de combinaison</term><term xml:lang="en">algorithme d'unification</term></keywords><classCode scheme="halDomain" n="info.info-oh">Computer Science [cs]/Other [cs.OH]</classCode><classCode scheme="halTypology" n="ART">Journal articles</classCode></textClass><abstract xml:lang="en">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.</abstract></profileDesc></hal></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Hal/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 005044 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Hal/Corpus/biblio.hfd -nk 005044 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Hal
|étape= Corpus
|type= RBID
|clé= Hal:inria-00099222
|texte= Unification Algorithms Cannot Be Combined in Polynomial Time
}}
| This area was generated with Dilib version V0.6.33. |  |