Computational Complexity of Simultaneous Elementary Matching Problems

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 : The simultaneous elementary E-matching problem for an equational theory~E is to decide whether there is an E-matcher for a given system of equations in which the only non-constant function symbols occurring in the terms to be matched are the ones constrained by the equational axioms of~E. We study the computational complexity of simultaneous elementary matching problems for the equational theories A of semigroups, AC of commutative semigroups, and ACU of commutative monoids. In each case, we delineate the boundary between NP-completeness and solvability in polynomial time by considering two parameters, the number of equations in the systems and the number of constant symbols in the signature. Moreover, we analyze further the intractable cases of simultaneous elementary AC-matching and ACU-matching by taking also into account the maximum number of occurrences of each variable. Using combinatorial optimization techniques, we show that if each variable is restricted to having at most two occurrences, then several cases of simultaneous elementary AC-matching and ACU-matching can be solved in polynomial time.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 1999, 23 (2), pp.107-136
Liste complète des métadonnées

https://hal.inria.fr/inria-00098986
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:41:00
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58

Identifiants

  • HAL Id : inria-00098986, version 1

Collections

Citation

Miki Hermann, Phokion G. Kolaitis. Computational Complexity of Simultaneous Elementary Matching Problems. Journal of Automated Reasoning, Springer Verlag, 1999, 23 (2), pp.107-136. 〈inria-00098986〉

Partager

Métriques

Consultations de la notice

122