A survey of satisfiability modulo theory. (English) Zbl 1453.68116
Gerdt, Vladimir P. (ed.) et al., Computer algebra in scientific computing. 18th international workshop, CASC 2016, Bucharest, Romania, September 19–23, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9890, 401-425 (2016).
Summary: 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.
For the entire collection see [Zbl 1346.68010].
For the entire collection see [Zbl 1346.68010].
MSC:
| 68R07 | Computational aspects of satisfiability |
| 03B70 | Logic in computer science |
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
References:
| [1] | Achlioptas, D.: 8. In: [6], pp. 245–270 |
| [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) · doi:10.1007/978-3-642-39799-8_22 |
| [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) · Zbl 1350.68223 · doi:10.1007/978-3-642-25379-9_12 |
| [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) · Zbl 1102.14041 |
| [6] | Handbook of Satisfiability, vol. 185. IOS Press, Amsterdam (2009) |
| [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) · Zbl 1291.68325 · doi:10.1007/978-3-642-14203-1_27 |
| [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) · Zbl 1291.68328 · doi:10.1007/978-3-642-14052-5_14 |
| [9] | Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, Berlin (2007) · Zbl 1126.03001 |
| [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) · Zbl 1317.68110 · doi:10.1007/s10703-013-0203-7 |
| [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) |
| [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) · Zbl 1360.65086 · doi:10.1145/1073884.1073899 |
| [13] | Christ, J.: Interpolation modulo theories. Ph.D. thesis, Albert-Ludwigs-Universität, Freiburg (2015) |
| [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) · Zbl 1381.68152 · doi:10.1007/978-3-642-36742-7_9 |
| [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) · doi:10.1007/3-540-07407-4_17 |
| [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) · Zbl 0258.68046 |
| [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) · Zbl 1290.68112 · doi:10.1007/978-3-642-15297-9_8 |
| [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) · doi:10.1007/978-3-642-33826-7_16 |
| [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) · Zbl 1503.68181 · doi:10.1007/978-3-642-39799-8_25 |
| [20] | Dantzig, G.B., Thapa, M.N.: Linear Programming 1: Introduction. Springer, New York (1997) · Zbl 0883.90090 |
| [21] | de Moura, L.M.: Personal communication |
| [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) · Zbl 1426.68251 · doi:10.1007/978-3-642-35873-9_1 |
| [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) · Zbl 1250.90057 · doi:10.1007/s10703-011-0127-z |
| [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) · doi:10.1007/11817963_11 |
| [25] | Dutertre, B., de Moura, L.M.: Integrating simplex with DPLL(T). Sri-csl-06-01, SRI International, computer science laboratory (2006) |
| [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) · Zbl 1138.68537 · doi:10.1007/978-3-540-79719-7_8 |
| [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) · Zbl 0294.02022 · doi:10.1137/0204006 |
| [28] | Fouilhé, A.: Revisiting the abstract domain of polyhedra: constraints-only representation and formula proof. Ph.D. thesis, Université de Grenoble (2015) |
| [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) |
| [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) · Zbl 1248.68142 |
| [31] | Godefroid, P., Levin, M.Y., Molnar, D.: SAGE: whitebox fuzzing for security testing. Queue 10(1), 20:20–20:27 (2012) |
| [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) · Zbl 0662.12001 · doi:10.1016/S0747-7171(88)80005-1 |
| [33] | Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39, 297–308 (1985) · Zbl 0586.03010 · doi:10.1016/0304-3975(85)90144-6 |
| [34] | Handelman, D.: Representing polynomials by positive linear functions on compact convex polyhedra. Pacific J. Math. 132(1), 35–62 (1988) · Zbl 0659.52002 · doi:10.2140/pjm.1988.132.35 |
| [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) · doi:10.1145/2597809.2597817 |
| [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) |
| [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) · doi:10.1007/978-3-642-33125-1_20 |
| [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) · Zbl 1321.68196 · doi:10.1145/2103656.2103689 |
| [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) · doi:10.1145/96877.96943 |
| [40] | IEEE: IEEE standard for Binary floating-point arithmetic for microprocessor systems. ANSI/IEEE Standard 754–1985 (1985) |
| [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) · Zbl 1358.68257 · doi:10.1007/978-3-642-31365-3_27 |
| [42] | Karpenkov, E., Beyer, D., Friedberger, K.: JavaSMT: A unified interface for SMT solvers in Java. In: VSTTE (2016, to appear) |
| [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) |
| [44] | King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976) · Zbl 0329.68018 · doi:10.1145/360248.360252 |
| [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) · doi:10.1109/FMCAD.2014.6987606 |
| [46] | Krivine, J.L.: Anneaux préordonnés. J. d’analyse mathématique 12, 307–326 (1964) · Zbl 0134.03902 · doi:10.1007/BF02807438 |
| [47] | Kroening, D., Strichman, O.: Decision Procedures. Springer, New York (2008) · Zbl 1149.68071 |
| [48] | Loos, R., Weispfenning, V.: Applying linear quantifier elimination. Comput. J. 36(5), 450–462 (1993) · Zbl 0787.03021 · doi:10.1093/comjnl/36.5.450 |
| [49] | Marques-Silva, J.P., Lynce, I., Malik, S.: 4. In: [6], pp. 131–153 |
| [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) · Zbl 1475.68093 · doi:10.1007/978-3-662-49122-5_8 |
| [51] | McCallum, S.: An improved projection operation for cylindrical algebraic decomposition. In: Quantifier Elimination and Cylindrical Algebraic Decomposition, pp. 242–268. Springer, Wien (1998) · Zbl 0900.68279 · doi:10.1007/978-3-7091-9459-1_12 |
| [52] | McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345(1), 101–121 (2005) · Zbl 1079.68092 · doi:10.1016/j.tcs.2005.07.003 |
| [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) · Zbl 1188.68196 · doi:10.1007/11817963_14 |
| [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) · Zbl 1242.68282 · doi:10.1007/978-3-642-02658-4_35 |
| [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) · doi:10.1145/378239.379017 |
| [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) |
| [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) · Zbl 1182.68213 · doi:10.1007/978-3-540-89439-1_18 |
| [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) · Zbl 1242.68168 · doi:10.1007/978-3-642-02658-4_42 |
| [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) · doi:10.1007/978-3-642-14295-6_51 |
| [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) |
| [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) · doi:10.1145/125826.125848 |
| [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) · Zbl 1072.68693 · doi:10.1145/860854.860901 |
| [63] | Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1998) · Zbl 0970.90052 |
| [64] | Sebastiani, R., Tomasi, S.: Optimization in SMT with \[ {\mathcal 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) · Zbl 1358.68264 · doi:10.1007/978-3-642-31365-3_38 |
| [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) · doi:10.1007/978-3-642-31424-7_11 |
| [66] | Stein, W.A.: Modular Forms, a Computational Approach. Graduate Studies in Mathematics, vol. 79. AMS (2007) · Zbl 1110.11015 |
| [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) · doi:10.1007/978-3-642-81955-1_28 |
| [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) · doi:10.1007/978-3-662-46681-0_10 |
| [69] | Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge (1993) · Zbl 0919.68082 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
