Computational complexity of simultaneous elementary matching problems
- 912 Downloads
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 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 graph-theoretic 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.
KeywordsPolynomial Time Function Symbol Equational Theory Commutative Semigroup Ground Term
Unable to display preview. Download preview PDF.
- [Ber73]C. Berge. Graphs and hypergraphs. North-Holland, Amsterdam, 2nd edition, 1973.Google Scholar
- [BHK*88]H-J. Bürckert, A. Herold, D. Kapur, J.H. Siekmann, M.E. Stickel, M. Tepp, and H. Zhang. Opening the AC-unification race. Journal of Automated Reasoning, 4(4):465–474, 1988.Google Scholar
- [BKN87]D. Benanav, D. Kapur, and P. Narendran. Complexity of matching problems. Journal of Symbolic Computation, 3:203–216, 1987.Google Scholar
- [BS93]F. Baader and J.H. Siekmann. Unification theory. In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, Oxford University Press, Oxford (UK), 1993.Google Scholar
- [EJ69]J. Edmonds and E.L. Johnson. Matching: a well-solved class of integer linear programs. In Combinatorial Structures and Their Applications, Calgary (Canada), pages 89–92, Gordon and Breach, 1969.Google Scholar
- [Eke93]S.M. Eker. Improving the efficiency of AC matching and unification. Research report 2104, Institut de Recherche en Informatique et en Automatique, November 1993.Google Scholar
- [GJ79]M.R. Garey and D.S. Johnson. Computers and intractability: A guide to the theory of NP-completeness. W.H. Freeman and Co, 1979.Google Scholar
- [HK94]M. Hermann and P.G. Kolaitis. The complexity of counting problems in equational matching. In A. Bundy, editor, Proceedings 12th International Conference on Automated Deduction, Nancy (France), pages 560–574, Springer-Verlag, June 1994.Google Scholar
- [JK91]J.-P. Jouannaud and C. Kirchner. Solving equations in abstract algebras: a rule-based survey of unification. In J.-L. Lassez and G. Plotkin, editors, Computational Logic. Essays in honor of Alan Robinson, chapter 8, pages 257–321, MIT Press, Cambridge (MA, USA), 1991.Google Scholar
- [Pap94]C.H. Papadimitriou. Computational complexity. Addison-Wesley, 1994.Google Scholar
- [VR92]R.M. Verma and I.V. Ramakrishnan. Tight complexity bounds for term matching problems. Information and Computation, 101:33–69, 1992.Google Scholar