Skip to main content
SpringerLink
Log in

Why Combined Decision Problems Are Often Intractable

  • Conference paper
Frontiers of Combining Systems (FroCoS 2000)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1794))

Included in the following conference series:

Abstract

Most combination methods for decision procedures known from the area of automated deduction assign to a given “combined” input problem an exponential number of output pairs where the two components represent “pure” decision problems that can be decided with suitable component decision procedures. A mixed input decision problem evaluates to true iff there exists an output pair where both components evaluate to true. We provide a formal framework that explains why in many cases it is impossible to have a polynomial-time optimization of such a combination method, and why often combined decision problems are NP-hard, regardless of the complexity of the component problems. As a first application we consider Oppen’s combination method for algorithms that decide satisfiability of quantifier-free formulae in disjunctive normal form w.r.t. a first-order theory. A collection of first-order theories is given where combined problems are always NP-hard and Oppen’s method does not have a polynomial-time optimization. As a second example, similar results are given for the problem of combining algorithms that decide whether a unification problem has a solution w.r.t. to a given equational theory.

This paper was first presented at the “Workshop on Complexity in Automated Deduction” organized by M. Hermann in Nancy (June 1999).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • Baader, F.: On the Complexity of Boolean Unification. Information Processing Letters 67(4), 215–220 (1998)

    Article  MathSciNet  Google Scholar 

  • Baader, F., Schulz, K.U.: Combination techniques and decision problems for disunification. Theoretical Computer Science 142, 229–255 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  • Baader, F., Schulz, K.U.: Unification in the union of disjoint equational theories: Combining decision procedures. Journal of Symbolic Computation 21, 211–243 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  • Baader, F., Siekmann, J.: Unification Theory. In: Gabbay, D.M., Hogger, C., Robinson, J. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, pp. 41–125. Oxford University Press, Oxford (1994)

    Google Scholar 

  • Boudet, A.: Combining Unification Algorithms. Journal of Symbolic Computation 16, 597–626 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  • Cyrluk, D., Lincoln, P., Shankar, N.: On Shostak’s decision procedure for combinations of theories. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol. 814, pp. 463–477. Springer, Heidelberg (1994)

    Google Scholar 

  • Domenjoud, E., Klay, F., Ringeissen, R.: Combination Techniques for Non-Disjoint Equational Theories. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol. 814, pp. 267–281. Springer, Heidelberg (1994)

    Google Scholar 

  • Downey, P., Sethi, R.: Assignment commands with array references. Journal of the ACM 25 (4), 652–666 (1994)

    Article  MathSciNet  Google Scholar 

  • Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman and Co., San Francisco (1979)

    Google Scholar 

  • Guo, Q., Narendran, P., Wolfram, D.A.: Unification and Matching modulo Nilpotence. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol. 1104, pp. 261–274. Springer, Heidelberg (1996)

    Google Scholar 

  • Hermann, M., Kolaitis, P.G.: Unification Algorithms Cannot be Combined in Polynomial Time. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol. 1104, pp. 246–260. Springer, Heidelberg (1996)

    Google Scholar 

  • Herold, A.: Combination of Unification Algorithms. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230. Springer, Heidelberg (1986)

    Google Scholar 

  • Kapur, D., Narendran, P.: Complexity of Unification Problems with Associative-Commutative Operators. J. Automated Reasoning 9, 261–288 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  • Kepser, S.: Negation in Combining Constraint Systems. In: Gabbay, D.M., de Rijke, M. (eds.) Frontiers of Combining Systems 2, Papers presented at FroCoS 1998, pp. 117–192. Research Studies Press/Wiley, Amsterdam (2000)

    Google Scholar 

  • Kepser, S., Richts, J.: Optimization Techniques for Combining Constraint Solvers. In: Gabbay, D.M., de Rijke, M. (eds.) Frontiers of Combining Systems 2, Papers presented at FroCo 1998, pp. 193–210. Research Studies Press/Wiley, Amsterdam (2000)

    Google Scholar 

  • Kirchner, C.: Méthodes et outils de conception systématique d’algorithms d’unification dans les théories équationelles. Thèse d’Etat, Université de Nancy 1, France (1985)

    Google Scholar 

  • Lankford, D.S., Butler, G., Brady, B.: Abelian Group Unification Algorithms for Elementary Terms. Contemporary Mathematics 29 (1984)

    Google Scholar 

  • Nelson, C.G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Programming Languages and Systems 2(1), 245–257 (1979)

    Article  Google Scholar 

  • Nelson, C.G., Oppen, D.C.: Fast decision algorithms based on congruence closure. Journal of the ACM 27(2), 356–364 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  • Nipkow, T.: Combining Matching Algorithms: The Regular Case. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, pp. 343–358. Springer, Heidelberg (1989)

    Google Scholar 

  • Oppen, D.C.: Complexity, Convexity and Combination of Theories. Theoretical Computer Science  12, 291–302 (1980)

    Google Scholar 

  • Pigozzi, D.: The Join of Equational Theories. Colloquium Mathematicum XXX, 15–25 (1974)

    MathSciNet  Google Scholar 

  • Ringeissen, C.: Cooperation of Decision Procedures for the Satisfiability Problem. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems, Proceedings of the 1st International Workshop, FroCoS 1996, Munich, Germany. Applied Logic Series, vol. 3, pp. 121–141. Kluwer, Dordrecht (1996)

    Google Scholar 

  • Schaefer, T.J.: The complexity of satisfiability problems. In: Proceedings 10th Symposium on Theory of Computing, San Diego, CA, pp. 216–226 (1978)

    Google Scholar 

  • Schmidt-Schauβ, M.: Combination of Unification Algorithms. J. Symbolic Computation 8, 51–99 (1989)

    Google Scholar 

  • Schulz, K.U.: A Criterion for Intractability of E-unification with Free Function Symbols and its Relevance for Combination of Unification Algorithms. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 284–298. Springer, Heidelberg (1997)

    Google Scholar 

  • Schulz, K.U.: Tractable and Intractable Instances of Combination Problems for Unification and Disunification. To appear in Journal of Logic and Computation 10(1) (2000)

    Google Scholar 

  • Shostak, R.E.: Deciding Combinations of Theories. Journal of the ACM 31(1), 1–12 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  • Tidén, E.: Unification in Combinations of Collapse Free Theories with Disjoint Sets of Function Symbols. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 431–449. Springer, Heidelberg (1986)

    Google Scholar 

  • Tinelli, C., Harandi, M.: A New Correctness Proof of the Nelson-Oppen Combination Procedure. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems, Proceedings of the 1st International Workshop, FroCoS 1996, Munich, Germany. Applied Logic Series, vol. 3, pp. 103–121. Kluwer, Dordrecht (1996)

    Google Scholar 

  • Yelick, K.: Unification in Combinations of Collapse Free Regular Theories. J. Symbolic Computation 3 (1987)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CIS, University of Munich, Oettingenstr. 67, D-80538, München, Germany

    Klaus U. Schulz

Authors
  1. Klaus U. Schulz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. INRIA & LORIA,  

    Hélène Kirchner

  2. LORIA - INRIA, Campus scientifique, 615, rue du Jardin Botanique, 54602, Villers-les-Nancy, France

    Christophe Ringeissen

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schulz, K.U. (2000). Why Combined Decision Problems Are Often Intractable. In: Kirchner, H., Ringeissen, C. (eds) Frontiers of Combining Systems. FroCoS 2000. Lecture Notes in Computer Science(), vol 1794. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10720084_15

Download citation

  • DOI: https://doi.org/10.1007/10720084_15

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67281-4

  • Online ISBN: 978-3-540-46421-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation