Skip to main content
SpringerLink
Log in

The Strategy Challenge in SMT Solving

  • Chapter
Automated Reasoning and Mathematics

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

Abstract

High-performance SMT solvers contain many tightly integrated, hand-crafted heuristic combinations of algorithmic proof methods. While these heuristic combinations tend to be highly tuned for known classes of problems, they may easily perform badly on classes of problems not anticipated by solver developers. This issue is becoming increasingly pressing as SMT solvers begin to gain the attention of practitioners in diverse areas of science and engineering. We present a challenge to the SMT community: to develop methods through which users can exert strategic control over core heuristic aspects of SMT solvers. We present evidence that the adaptation of ideas of strategy prevalent both within the Argonne and LCF theorem proving paradigms can go a long way towards realizing this goal.

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 49.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

  1. Dolzmann, T.S.A.: Redlog User Manual - Edition 2.0. MIP-9905 (1999)

    Google Scholar 

  2. Ackermann, W.: Solvable cases of the decision problem. Studies in Logic and the Foundation of Mathematics (1954)

    Google Scholar 

  3. Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: The Matita Interactive Theorem Prover. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 64–69. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  4. Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library, SMT-LIB (2010), http://www.SMT-LIB.org

  5. Barrett, C.W., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  6. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004)

    Google Scholar 

  7. Bonacina, M.P.: A Taxonomy of Theorem-Proving Strategies. In: Veloso, M.M., Wooldridge, M.J. (eds.) Artificial Intelligence Today. LNCS (LNAI), vol. 1600, pp. 43–84. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  8. Bonacina, M.P., Hsiang, J.: On the modeling of search in theorem proving–towards a theory of strategy analysis. Inf. Comput. 147(2), 171–208 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  9. Bonacina, M.P., McCune, W.W.: Distributed Theorem Proving by Peers. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 841–845. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  10. Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Rossum, P., Schulz, S., Sebastiani, R.: MathSAT: Tight Integration of SAT and Mathematical Decision Procedures. J. Autom. Reason. 35(1-3), 265–293 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  11. Brown, C.W.: QEPCAD-B: A System for Computing with Semi-algebraic Sets via Cylindrical Algebraic Decomposition. SIGSAM Bull. 38, 23–24 (2004)

    Article  Google Scholar 

  12. Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Santuari, A., Sebastiani, R.: To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in \(\mathit{SMT}(\mathcal{EUF} \cup \mathcal{T})\). In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 557–571. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  13. Davis, M.: Eliminating the Irrelevant from Mechanical Proofs. In: Proc. Symp. Applied Math., vol. XV, pp. 15–30 (1963)

    Google Scholar 

  14. Davis, M.: The early history of automated deduction. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 3–15. Elsevier and MIT Press (2001)

    Google Scholar 

  15. Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5, 394–397 (1962)

    Article  MathSciNet  MATH  Google Scholar 

  16. Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7, 201–215 (1960)

    Article  MathSciNet  MATH  Google Scholar 

  17. de Moura, L., Bjørner, N.: Relevancy propagation. Technical Report MSR-TR-2007-140, Microsoft Research (2007)

    Google Scholar 

  18. de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  19. de Moura, L.M., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)

    Article  Google Scholar 

  20. Dolzmann, A., Seidl, A., Sturm, T.: Efficient Projection Orders for CAD. In: ISSAC 2004: Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation, pp. 111–118. ACM (2004)

    Google Scholar 

  21. Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  22. Gilmore, P.C.: A Proof Method for Quantification Theory: its Justification and Realization. IBM J. Res. Dev. 4, 28–35 (1960)

    Article  MathSciNet  MATH  Google Scholar 

  23. Gordon, M.: From LCF to HOL: a short history, pp. 169–185. MIT Press, Cambridge (2000)

    Google Scholar 

  24. Gordon, M.J.C., Melham, T.F.: Introduction to HOL: a theorem-proving environment for higher-order logic. Cambridge University Press (1993)

    Google Scholar 

  25. Hickey, J.J.: The MetaPRL Logical Programming Environment. PhD thesis, Cornell University, Ithaca, NY (January 2001)

    Google Scholar 

  26. Jovanović, D., de Moura, L.: Cutting to the Chase Solving Linear Integer Arithmetic. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 338–353. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  27. Kirchner, F., Muñoz, C.: The proof monad. Journal of Logic and Algebraic Programming 79(3-5), 264–277 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  28. Kowalski, R.: Search Strategies for Theorem Proving. Machine Intelligence 5, 181–201 (1969)

    MATH  Google Scholar 

  29. Lusk, E.L.: Controlling Redundancy in Large Search Spaces: Argonne-Style Theorem Proving Through the Years. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 96–106. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  30. Luttik, B., Visser, E.: Specification of rewriting strategies. In: Sellink, M.P.A. (ed.) 2nd International Workshop on the Theory and Practice of Algebraic Specifications (ASF+SDF 1997), Electronic Workshops in Computing. Springer, Berlin (1997)

    Google Scholar 

  31. McCune, W.: Solution of the Robbins Problem. J. Autom. Reason. 19(3), 263–276 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  32. McCune, W.: Prover9 and Mace4 (2005-2010), http://www.cs.unm.edu/mccune/prover9/

  33. Milner, R.: Logic for computable functions: description of a machine implementation. Technical Report STAN-CS-72-288, Stanford University (1972)

    Google Scholar 

  34. Newell, A., Shaw, J.C., Simon, H.A.: Elements of a Theory of Human Problem Solving. Psychological Review 65, 151–166 (1958)

    Article  Google Scholar 

  35. Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  36. Passmore, G.O.: Combined Decision Procedures for Nonlinear Arithmetics, Real and Complex. PhD thesis, University of Edinburgh (2011)

    Google Scholar 

  37. Passmore, G.O., Jackson, P.B.: Combined Decision Techniques for the Existential Theory of the Reals. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) Calculemus/MKM 2009. LNCS (LNAI), vol. 5625, pp. 122–137. Springer, Heidelberg (2009)

    Google Scholar 

  38. Passmore, G.O., Jackson, P.B.: Abstract Partial Cylindrical Algebraic Decomposition I: The Lifting Phase. In: Cooper, S.B., Dawar, A., Löwe, B. (eds.) CiE 2012. LNCS, vol. 7318, pp. 560–570. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  39. Paulson, L.: Logic and Computation: Interactive Proof with Cambdrige LCF, vol. 2. Cambridge University Press (1987)

    Google Scholar 

  40. Paulson, L.: Isabelle: The next 700 theorem provers. In: Logic and Computer Science, pp. 361–386. Academic Press (1990)

    Google Scholar 

  41. Plaisted, D.A.: The Search Efficiency of Theorem Proving Strategies. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 57–71. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  42. Prawitz, D.: An Improved Proof Procedure. Theoria 26(2), 102–139 (1960)

    Article  MathSciNet  MATH  Google Scholar 

  43. Robinson, A.: Short Lecture. Summer Institute for Symbolic Logic, Cornell University (1957)

    Google Scholar 

  44. Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12, 23–41 (1965)

    Article  MathSciNet  MATH  Google Scholar 

  45. Wang, H.: Toward mechanical mathematics. IBM J. Res. Dev. 4, 2–22 (1960)

    Article  MathSciNet  MATH  Google Scholar 

  46. Weispfenning, V.: Quantifier Elimination for Real Algebra - the Quadratic Case and Beyond. Appl. Algebra Eng. Commun. Comput. 8(2), 85–101 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  47. Wos, L., Carson, D., Robinson, G.: The unit preference strategy in theorem proving. In: Proceedings of the Fall Joint Computer Conference, AFIPS 1964, Part I, October 27-29, pp. 615–621. ACM, New York (1964)

    Google Scholar 

  48. Wos, L., Robinson, G.A., Carson, D.F.: Efficiency and completeness of the set of support strategy in theorem proving. J. ACM 12, 536–541 (1965)

    Article  MathSciNet  MATH  Google Scholar 

  49. Zankl, H., Middeldorp, A.: Satisfiability of Non-linear (Ir)rational Arithmetic. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16. LNCS (LNAI), vol. 6355, pp. 481–500. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Microsoft Research, Redmond, US

    Leonardo de Moura

  2. Clare Hall, University of Cambridge, UK

    Grant Olney Passmore

  3. LFCS, University of Edinburgh, UK

    Grant Olney Passmore

Authors
  1. Leonardo de Moura
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Grant Olney Passmore
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università degli Studi di Verona, 37134, Verona, Italy

    Maria Paola Bonacina

  2. Artificial Intelligence Center, SRI International, 333 Ravenswood Avenue, 94025, Menlo Park, CA, USA

    Mark E. Stickel

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

de Moura, L., Passmore, G.O. (2013). The Strategy Challenge in SMT Solving. In: Bonacina, M.P., Stickel, M.E. (eds) Automated Reasoning and Mathematics. Lecture Notes in Computer Science(), vol 7788. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36675-8_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-36675-8_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-36674-1

  • Online ISBN: 978-3-642-36675-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation