Skip to main content
SpringerLink
Log in

A Survey of Satisfiability Modulo Theory

  • Conference paper
  • First Online:
Computer Algebra in Scientific Computing (CASC 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9890))

Included in the following conference series:

Abstract

Satisfiability modulo theory (SMT) consists in testing the satisfiability of first-order formulas over linear integer or real arithmetic, or other theories. In this survey, we explain the combination of propositional satisfiability and decision procedures for conjunctions known as DPLL(T), and the alternative “natural domain” approaches. We also cover quantifiers, Craig interpolants, polynomial arithmetic, and how SMT solvers are used in automated software analysis.

The research leading to these results has received funding from the European Research Council under the European Union’s Seventh Framework Programme (FP/2007-2013)/ERC Grant Agreement nr. 306595 “STATOR”.

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 EPUB and 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

Notes

  1. 1.

    This survey focuses on linear and polynomial numeric constraints over integers and reals. SMT however encompasses theories as diverse as character strings, inductive data structures, bit-vector arithmetic, and ordinary differential equations.

  2. 2.

    Further propositional connectives, such as exclusive-or, or “let x be \(e_1\) in \(e_2\)” constructs may be also considered.

  3. 3.

    https://github.com/sosy-lab/java-smt [42].

  4. 4.

    e.g. ZArith https://forge.ocamlcore.org/projects/zarith.

  5. 5.

    The performance with linear programming solvers meant for large industrial instances was however disappointing [26], due to overhead. Closer integration is needed.

  6. 6.

    As implemented in e.g. Linbox (http://www.linalg.org/), IML (https://cs.uwaterloo.ca/~astorjoh/iml.html) [12] and SageMath (http://www.sagemath.org/).

  7. 7.

    One can in fact prove a form of completeness of that approach when the problem contains linear constraints defining a bounded polyhedron, and one nonlinear constraint: if such a problem is unsatisfiable, then this can be proved by going to a sufficiently high degree of products. This follows from Krivine–Handelman’s theorem [34, 46].

  8. 8.

    Following the terminology of abstract interpretation; see [10] for more.

  9. 9.

    Successive applications of Fourier-Motzkin may lead to very large sets of predicates, thus this argument seems of mostly theoretical interest.

  10. 10.

    \(x \ge K + \epsilon \) with K real means \(x > K\).

  11. 11.

    In the case of linear integer arithmetic, we need to enrich the language of the output formula with constraints of divisibility by constants: e.g. \(\exists x~ y = 2x\) is equivalent to quantifier-free \(2 \mid x\).

  12. 12.

    This amounts to projection of convex polyhedra, for which there exist algorithms based on conversion to generators (vertices), Fourier-Motzkin elimination and pruning, or parametric linear programming, among others [28].

  13. 13.

    In program analysis, this corresponds to stating “after the first instruction, the program variables satisfy \(I_1\), but then if one executes the second instruction from \(I_1\), the program variables then satisfy \(I_2\)...”, and \(\{ I_i \} ~ \tau _i~ \{ I_{i+1} \}\) constitute Hoare triples.

  14. 14.

    SMTInterpol 2.1-31-gafd0372-comp.

  15. 15.

    MathSAT 5.3.10.

  16. 16.

    Worst-case complexity, or completeness in complexity classes, is therefore not always a good indicator of practical performance. Average complexity is difficult to define (one needs to suppose a probability distribution on formulas) and may ill-describe practical use cases: it is well-known that random SAT instances behave unlike industrial examples [1], and same with random linear constraints [58]. For want of better indication, performance is measured on libraries of benchmarks.

  17. 17.

    The author had several computer algebra packages crash or produce wrong results. Perhaps running large libraries of benchmarks would help in finding such bugs.

References

  1. Achlioptas, D.: 8. In: [6], pp. 245–270

    Google Scholar 

  2. Albarghouthi, A., McMillan, K.L.: Beautiful interpolants. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 313–329. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  3. Armand, M., Faure, G., Grégoire, B., Keller, C., Théry, L., Werner, B.: A modular integration of SAT/SMT solvers to coq through proof witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 135–150. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  4. Barrett, C., Fontaine, P., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB). www.SMT-LIB.org (2016)

  5. Basu, S., Pollack, R., Roy, M.F.: Algorithms in Real Algebraic Geometry. Springer, Berlin (2006)

    MATH  Google Scholar 

  6. Handbook of Satisfiability, vol. 185. IOS Press, Amsterdam (2009)

    Google Scholar 

  7. Bjørner, N.: Linear quantifier elimination as an abstract decision procedure. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 316–330. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  8. Böhme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 179–194. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  9. Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, Berlin (2007)

    MATH  Google Scholar 

  10. Brain, M., D’Silva, V., Griggio, A., Haller, L., Kroening, D.: Deciding floating-point logic with abstract conflict driven clause learning. Formal Methods Syst. Des. 45(2), 213–245 (2014)

    Article  MATH  Google Scholar 

  11. Barbosa, C., de Oliveira, D., Monniaux, D.: Experiments on the feasibility of using a floating-point simplex in an SMT solver. In: Fontaine, P., Schmidt, R.A., Schulz, S. (eds.) Workshop on Practical Aspects of Automated Reasoning (PAAR). EPiC Series, vol. 21, pp. 19–28. Easychair (2012)

    Google Scholar 

  12. Chen, Z., Storjohann, A.: A BLAS based C library for exact linear algebra on integer matrices. In: Proceedings of the ISSAC 2005, pp. 92–99. ACM, New York (2005)

    Google Scholar 

  13. Christ, J.: Interpolation modulo theories. Ph.D. thesis, Albert-Ludwigs-Universität, Freiburg (2015)

    Google Scholar 

  14. Christ, J., Hoenicke, J., Nutz, A.: Proof tree preserving interpolation. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 124–138. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  15. Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)

    Google Scholar 

  16. Cooper, D.C.: Theorem proving in arithmetic without multiplication. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence 7, pp. 91–100. Edinburgh University Press, Edinburgh (1972)

    Google Scholar 

  17. Cotton, S.: Natural domain SMT: a preliminary assessment. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 77–91. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  18. Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  19. Dai, L., Xia, B., Zhan, N.: Generating non-linear interpolants by semidefinite programming. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 364–380. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  20. Dantzig, G.B., Thapa, M.N.: Linear Programming 1: Introduction. Springer, New York (1997)

    MATH  Google Scholar 

  21. de Moura, L.M.: Personal communication

    Google Scholar 

  22. de Moura, L., Jovanović, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1–12. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  23. Dillig, I., Dillig, T., Aiken, A.: Cuts from proofs: a complete and practical technique for solving linear inequalities over integers. Form. Methods Syst. Des. 39(3), 246–260 (2011)

    Article  MATH  Google Scholar 

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

  25. Dutertre, B., de Moura, L.M.: Integrating simplex with DPLL(T). Sri-csl-06-01, SRI International, computer science laboratory (2006)

    Google Scholar 

  26. Faure, G., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: SAT modulo the theory of linear arithmetic: exact, inexact and commercial solvers. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 77–90. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  27. Ferrante, J., Rackoff, C.: A decision procedure for the first order theory of real addition with order. SIAM J. Comput. 4(1), 69–76 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  28. Fouilhé, A.: Revisiting the abstract domain of polyhedra: constraints-only representation and formula proof. Ph.D. thesis, Université de Grenoble (2015)

    Google Scholar 

  29. Fourier, J.: Histoire de l’acadmie, partie mathmatique. In: Mmoires de l’Acadmie des sciences de l’Institut de France, vol. 7. Gauthier-Villars, xlvij-lv (1827) (1824)

    Google Scholar 

  30. Gawlitza, T., Monniaux, D.: Invariant generation through strategy iteration in succinctly represented control flow graphs. Logic. Methods Comput. Sci. 8(3:29), 1–35 (2012)

    Google Scholar 

  31. Godefroid, P., Levin, M.Y., Molnar, D.: SAGE: whitebox fuzzing for security testing. Queue 10(1), 20:20–20:27 (2012)

    Google Scholar 

  32. Grigor’ev, D.Y., Vorobjov Jr., N.N.: Solving systems of polynomial inequalities in subexponential time. J. Symb. Comput. 5(1–2), 37–64 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  33. Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39, 297–308 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  34. Handelman, D.: Representing polynomials by positive linear functions on compact convex polyhedra. Pacific J. Math. 132(1), 35–62 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  35. Henry, J., Asavoae, M., Monniaux, D., Maiza, C.: How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics. In: Zhang, Y., Kulkarni, P. (eds.) Languages, Compilers, Tools and Theory for Embedded Systems (LCTES), pp. 43–52. ACM, New York (2014)

    Google Scholar 

  36. Henry, J., Monniaux, D., Moy, M.: PAGAI: a path sensitive static analyzer. In: Jeannet, B. (ed.) Third Workshop on Tools for Automatic Program Analysis (TAPAS 2012). Electronic Notes in Theoretical Computer Science 289, pp. 15–25 (2012)

    Google Scholar 

  37. Henry, J., Monniaux, D., Moy, M.: Succinct representations for abstract interpretation. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 283–299. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  38. Hoder, K., Kovács, L., Voronkov, A.: Playing in the grey area of proofs. In: Field, J., Hicks, M. (eds.) ACM Symposium on Principles of Programming Languages (POPL), pp. 259–272. ACM, New York (2012)

    Google Scholar 

  39. Hong, H.: An improvement of the projection operator in cylindrical algebraic decomposition. In: Watanabe, S., Nagata, M. (eds.) Proceedings of the ISSAC 1990, pp. 261–264. ACM, New York (1990)

    Google Scholar 

  40. IEEE: IEEE standard for Binary floating-point arithmetic for microprocessor systems. ANSI/IEEE Standard 754–1985 (1985)

    Google Scholar 

  41. Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 339–354. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  42. Karpenkov, E., Beyer, D., Friedberger, K.: JavaSMT: A unified interface for SMT solvers in Java. In: VSTTE (2016, to appear)

    Google Scholar 

  43. Keller, C.: Extended resolution as certificates for propositional logic. In: Blanchette, J.C., Urban, J. (eds.) Proof Exchange for Theorem Proving (PxTP). EPiC Series, vol. 14, pp. 96–109. EasyChair (2013)

    Google Scholar 

  44. King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  45. King, T., Barrett, C.W., Tinelli, C.: Leveraging linear and mixed integer programming for SMT. In: Formal Methods in Computer-Aided Design, (FMCAD), pp. 139–146. IEEE (2014)

    Google Scholar 

  46. Krivine, J.L.: Anneaux préordonnés. J. d’analyse mathématique 12, 307–326 (1964)

    Google Scholar 

  47. Kroening, D., Strichman, O.: Decision Procedures. Springer, New York (2008)

    MATH  Google Scholar 

  48. Loos, R., Weispfenning, V.: Applying linear quantifier elimination. Comput. J. 36(5), 450–462 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  49. Marques-Silva, J.P., Lynce, I., Malik, S.: 4. In: [6], pp. 131–153

    Google Scholar 

  50. Maréchal, A., Fouilhé, A., King, T., Monniaux, D., Périn, M.: Polyhedral approximation of multivariate polynomials using Handelman’s theorem. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 166–184. Springer, Berlin (2016)

    Chapter  Google Scholar 

  51. McCallum, S.: An improved projection operation for cylindrical algebraic decomposition. In: Quantifier Elimination and Cylindrical Algebraic Decomposition, pp. 242–268. Springer, Wien (1998)

    Google Scholar 

  52. McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345(1), 101–121 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  53. McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  54. McMillan, K.L., Kuehlmann, A., Sagiv, M.: Generalizing DPLL to richer logics. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 462–476. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  55. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Design Automation Conference (DAC), pp. 530–535. ACM, New York (2001)

    Google Scholar 

  56. Mitchell, J.E.: Branch-and-cut algorithms for combinatorial optimization problems. In: Pardalos, P.M., Resende, M.G.C. (eds.) Handbook of Applied Optimization. Oxford University Press, Oxford (2002)

    Google Scholar 

  57. Monniaux, D.: A quantifier elimination algorithm for linear real arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 243–257. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  58. Monniaux, D.: On using floating-point computations to help an exact linear arithmetic decision procedure. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 570–583. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  59. Monniaux, D.: Quantifier elimination by lazy model enumeration. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 585–599. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  60. Phan, A.D., Bjørner, N., Monniaux, D.: Anatomy of alternating quantifier satisfiability (work in progress). In: Fontaine, P., Goel, A. (eds.) 10th International Workshop on Satisfiability Modulo Theories (SMT), pp. 120–130 (2012)

    Google Scholar 

  61. Pugh, W.: The Omega test: A fast and practical integer programming algorithm for dependence analysis. In: Supercomputing, pp. 4–13. ACM, New York (1991)

    Google Scholar 

  62. Safey El Din, M., Schost, É.: Polar varieties and computation of one point in each connected component of a smooth real algebraic set. In: Proceedings of the ISSAC 2003, pp. 224–231. ACM, New York (2003)

    Google Scholar 

  63. Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1998)

    MATH  Google Scholar 

  64. Sebastiani, R., Tomasi, S.: Optimization in SMT with \({\cal L}\mathit{A}\)(\(\mathbb{Q}\)) cost functions. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 484–498. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  65. Sharma, R., Nori, A.V., Aiken, A.: Interpolants as classifiers. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 71–87. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  66. Stein, W.A.: Modular Forms, a Computational Approach. Graduate Studies in Mathematics, vol. 79. AMS (2007)

    Google Scholar 

  67. Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning: 2: Classical Papers on Computational Logic 1967–1970, pp. 466–483. Springer, Berlin (1983)

    Google Scholar 

  68. Unno, H., Terauchi, T.: Inferring simple solutions to recursion-free horn clauses via sampling. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 149–163. Springer, Heidelberg (2015)

    Google Scholar 

  69. Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge (1993)

    MATH  Google Scholar 

Download references

Acknowledgements

Thanks to the anonymous referees for their careful proofreading.

Author information

Authors and Affiliations

  1. Univ. Grenoble Alpes, VERIMAG, 38000, Grenoble, France

    David Monniaux

  2. CNRS, VERIMAG, 38000, Grenoble, France

    David Monniaux

Authors
  1. David Monniaux
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to David Monniaux .

Editor information

Editors and Affiliations

  1. Laboratory of Information Technologies, Joint Institute of Nuclear Research, Dubna, Russia

    Vladimir P. Gerdt

  2. Institut für Mathematik, Universität Kassel, Kassel, Germany

    Wolfram Koepf

  3. Institut für Mathematik, Universität Kassel, Kassel, Germany

    Werner M. Seiler

  4. Institute of Theoretical and Applied Mechanics, Russian Academy of Sciences, Novosibirsk, Russia

    Evgenii V. Vorozhtsov

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Monniaux, D. (2016). A Survey of Satisfiability Modulo Theory. In: Gerdt, V., Koepf, W., Seiler, W., Vorozhtsov, E. (eds) Computer Algebra in Scientific Computing. CASC 2016. Lecture Notes in Computer Science(), vol 9890. Springer, Cham. https://doi.org/10.1007/978-3-319-45641-6_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-45641-6_26

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-45640-9

  • Online ISBN: 978-3-319-45641-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation