Modular strategic SMT solving with SMT-RAT

Gereon Kremer; Erika Ábrahám

doi:10.2478/ausi-2018-0001

Abstract

In this paper we present the latest developments in SMT-RAT, a tool for the automated check of quantifier-free real and integer arithmetic formulas for satisfiability. As a distinguishing feature, SMT-RAT provides a set of solving modules and supports their strategic combination. We describe our CArL library for arithmetic computations, the available modules implemented on top of CArL, and how modules can be combined to satisfiability-modulo-theories (SMT) solvers. Besides the traditional SMT approach, some new modules support also the recently proposed and highly promising model-constructing satisfiability calculus approach.

References

[1] J. Abbott, A. M. Bigatti, CoCoALib: A C++ library for computations in commutative algebra . . . and beyond. Proc. of ICMS’10 (2010), vol. 6327 of LNCS, Springer, pp. 73–76. ⇒7, 1210.1007/978-3-642-15582-6_15
Search in Google Scholar Back to article
[2] E. Ábrahám, J. Nalbach, G. Kremer, Embedding the virtual substitution method in the model constructing satisfiability calculus framework. Proc. of SC-square’17 (2017), vol. 1974 of CEUR Workshop Proceedings, CEUR-WS.org. ⇒16
Search in Google Scholar Back to article
[3] A. Albarghouthi, A. Gurfinkel, O. Wei, M. Chechik, Abstract analysis of symbolic executions. Proc. of CAV’10 (2010), vol. 6174 of LNCS, Springer, pp. 495–510. ⇒1210.1007/978-3-642-14295-6_43
Search in Google Scholar Back to article
[4] C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanović, T. King, A. Reynolds, C. Tinelli, CVC4. Proc. of CAV’11 (2011), vol. 6806 of LNCS, Springer, pp. 171–177. ⇒9, 1410.1007/978-3-642-22110-1_14
Search in Google Scholar Back to article
[5] C. Barrett, P. Fontaine, C. Tinelli, The Satisfiability Modulo Theories Library (SMT-LIB). http://www.SMT-LIB.org, 2016. ⇒20
Search in Google Scholar Back to article
[6] C. Bauer, A. Frink, R. Kreckel, Introduction to the GiNaC framework for symbolic computation within the C++ programming language, Journal of Symbolic Computation33, 1 (2002) 1–12. ⇒7, 1210.1006/jsco.2001.0494
Search in Google Scholar Back to article
[7] T. Bouton, D. C. B. de Oliveira, D. Déharbe, P. Fontaine, veriT: An open, trustable and efficient SMT-solver, Proc. of CADE-22 (2009), vol. 5663 of LNCS, Springer, pp. 151–156. ⇒9, 1410.1007/978-3-642-02959-2_12
Search in Google Scholar Back to article
[8] M. Bromberger, C. Weidenbach, Fast cube tests for LIA constraint solving. Proc. of IJCAR’16 (2016), Springer, pp. 116–132. ⇒1510.1007/978-3-319-40229-1_9
Search in Google Scholar Back to article
[9] C. W. Brown, M. Košta, Constructing a single cell in cylindrical algebraic decomposition, Journal of Symbolic Computation70 (2015) 14–48. ⇒1710.1016/j.jsc.2014.09.024
Search in Google Scholar Back to article
[10] B. Buchberger, Gröbner bases: Applications. in: The Concise Handbook of Algebra. Kluwer Academic Publishers, 2002, pp. 265–268. ⇒12
Search in Google Scholar Back to article
[11] P.-S. Chen, Y.-S. Hwang, R. D.-C. Ju, J.-K. Lee, Interprocedural probabilistic pointer analysis, IEEE Trans. Parallel Distrib. Syst. 15, 10 (2004) 893–907. ⇒ 1210.1109/TPDS.2004.56
Search in Google Scholar Back to article
[12] A. Cimatti, A. Griggio, B. Schaafsma, B., R. Sebastiani, The MathSAT5 SMT solver. Proc. of TACAS’13, vol. 7795 of LNCS. Springer, 2013, pp. 93–107. ⇒910.1007/978-3-642-36742-7_7
Search in Google Scholar Back to article
[13] G. E. Collins, Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Automata Theory and Formal Languages (1975), vol. 33 of LNCS, Springer, pp. 134–183. ⇒11, 1210.1007/3-540-07407-4_17
Search in Google Scholar Back to article
[14] F. Corzilius, Virtual substitution in SMT solving, Diploma thesis, RWTH Aachen University, 2011. ⇒1410.1007/978-3-642-22953-4_31
Search in Google Scholar Back to article
[15] F. Corzilius, Integrating Virtual Substitution into Strategic SMT Solving. PhD thesis, RWTH Aachen University, 2016. ⇒15
Search in Google Scholar Back to article
[16] F. Corzilius, G. Kremer, S. Junges, S. Schupp, E. Ábrahám, SMT-RAT: An open source C++ toolbox for strategic and parallel SMT solving. Proc. of SAT’15 (2015), vol. 9340 of LNCS, Springer, pp. 360–368. ⇒6, 7, 9, 15, 2010.1007/978-3-319-24318-4_26
Search in Google Scholar Back to article
[17] F. Corzilius, U. Loup, S. Junges, S., E. Ábrahám, SMT-RAT: An SMT-compliant nonlinear real arithmetic toolbox. Proc. of SAT’12 (2012), vol. 7317 of LNCS, Springer, pp. 442–448. ⇒6, 710.1007/978-3-642-31612-8_35
Search in Google Scholar Back to article
[18] G. B. Dantzig, Linear programming and extensions. Princeton University Press, 1963. ⇒1010.7249/R366
Search in Google Scholar Back to article
[19] M. Davis, H. Putnam, A computing procedure for quantification theory. Journal of the ACM7, 3 (1960) 201–215. ⇒810.1145/321033.321034
Search in Google Scholar Back to article
[20] L. de Moura, N. Bjørner, Z3: An efficient SMT solver. Proc. of TACAS’08 (2008), vol. 4963 of LNCS, Springer, pp. 337–340. ⇒9, 1410.1007/978-3-540-78800-3_24
Search in Google Scholar Back to article
[21] L. M. de Moura, D. Jovanovic, A model-constructing satisfiability calculus. Proc. of VMCAI’13 (2013), vol. 7737 of LNCS, Springer, pp. 1–12. ⇒9, 16
Search in Google Scholar Back to article
[22] B. Dutertre, Yices 2.2. Proc. of CAV’14 (2014), vol. 8559 of LNCS, Springer, pp. 737–744. ⇒9, 1410.1007/978-3-319-08867-9_49
Search in Google Scholar Back to article
[23] B. Dutertre, L. M. de Moura, A fast linear-arithmetic solver for DPLL(T). Proc. of CAV’06 (2006), vol. 4144 of LNCS, Springer, pp. 81–94. ⇒1510.1007/11817963_11
Search in Google Scholar Back to article
[24] N. Eén, N. Sörensson, An extensible SAT-solver. Proc. of SAT’03 (2004), vol. 2919 of LNCS, Springer, pp. 502–518. ⇒1510.1007/978-3-540-24605-3_37
Search in Google Scholar Back to article
[25] P. Fontaine, M. Ogawa, T. Sturm, T., X. T. Vu, Subtropical satisfiability. Proc. of FroCoS’17 (2017), Springer, pp. 189–206. ⇒11, 1610.1007/978-3-319-66167-4_11
Search in Google Scholar Back to article
[26] C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, H. Zankl, SAT solving for termination analysis with polynomial interpretations. Proc. of SAT’07 (2007), Springer, pp. 340–354. ⇒1510.1007/978-3-540-72788-0_33
Search in Google Scholar Back to article
[27] S. Gao, M. Ganai, F. Ivančić, A. Gupta, S. Sankaranarayanan, E. M. Clarke, Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. Proc. of FMCAD’10 (2010), IEEE, pp. 81–90. ⇒10
Search in Google Scholar Back to article
[28] K. O. Geddes, S. R. Czapor, G. Labahn, Algorithms for Computer Algebra. Kluwer Academic Publishers, 1992. ⇒710.1007/b102438
Search in Google Scholar Back to article
[29] J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, R. Thiemann, Proving termination of programs automatically with AProVE. Proc. of IJCAR’14 (2014), vol. 8562 of LNAI, Springer, pp. 184–191. ⇒910.1007/978-3-319-08587-6_13
Search in Google Scholar Back to article
[30] M. Grobelna, SAT-modulo-theories solving for pseudo-Boolean constraints. Bachelor’s Thesis, RWTH Aachen University, 2017. ⇒14, 15
Search in Google Scholar Back to article
[31] R. Haehn, Using equational constraints in an incremental CAD projection. Master’s thesis, RWTH Aachen University, 2017. ⇒14
Search in Google Scholar Back to article
[32] E. M. Hahn, H. Hermanns, B. Wachter, L. Zhang, PARAM: A model checker for parametric Markov models. Proc. of CAV’10 (2010), vol. 6174 of LNCS, Springer, pp. 660–664. ⇒1210.1007/978-3-642-14295-6_56
Search in Google Scholar Back to article
[33] W. Hentze, Infeasible subsets for nonlinear SMT. Bachelor’s Thesis, RWTH Aachen University, 2017. ⇒14
Search in Google Scholar Back to article
[34] S. Herbort, D. Ratz, Improving the efficiency of a nonlinear-system-solver using a componentwise Newton method. Tech. Rep. 2/1997, Inst. für Angewandte Mathematik, University of Karlsruhe, 1997. ⇒10
Search in Google Scholar Back to article
[35] D. Jovanović, Solving nonlinear integer arithmetic with MCSAT. Proc. of VM-CAI’17 (2017), Springer, pp. 330–346. ⇒2010.1007/978-3-319-52234-0_18
Search in Google Scholar Back to article
[36] D. Jovanović, L. de Moura, Solving non-linear arithmetic. Proc. of IJCAR’12 (2012), vol. 7364 of LNAI, Springer, pp. 339–354. ⇒1610.1007/978-3-642-31365-3_27
Search in Google Scholar Back to article
[37] S. Junges, On Gröbner bases in SMT-compliant decision procedures. Bachelor’s Thesis, RWTH Aachen University, 2012. ⇒14
Search in Google Scholar Back to article
[38] S. Junges, U. Loup, F. Corzilius, E. Ábrahám, E. On Gröbner bases in the context of satisfiability-modulo-theories solving over the real numbers. Proc. of CAI’13 (2013), vol. 8080 of LNCS, Springer, pp. 186–198. ⇒1510.1007/978-3-642-40663-8_18
Search in Google Scholar Back to article
[39] T. V. Khanh, X. Vu, M. Ogawa, raSAT: SMT for polynomial inequality. Proc. of SMT’14 (2014), p. 67. ⇒9
Search in Google Scholar Back to article
[40] G. Kremer, Isolating real roots using adaptable-precision interval arithmetic. Master’s thesis, RWTH Aachen University, 2013. ⇒14
Search in Google Scholar Back to article
[41] G. Kremer, F. Corzilius, E. Ábrahám, A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic. Proc. of CASC’16 (2016), vol. 9890 of LNCS, Springer, pp. 315–335. ⇒11, 15, 2010.1007/978-3-319-45641-6_21
Search in Google Scholar Back to article
[42] A. Krüger, Bitvectors in SMT-RAT and their application to integer arithmetics. Master’s thesis, RWTH Aachen University, 2015. ⇒14, 15
Search in Google Scholar Back to article
[43] J. P. Marques-Silva, K. A. Sakallah, Grasp: A search algorithm for propositional satisfiability. IEEE Transactions on Computers48 (1999) 506–521. ⇒810.1109/12.769433
Search in Google Scholar Back to article
[44] J. Nalbach, Embedding the virtual substitution in the MCSAT framework. Bachelor’s Thesis, RWTH Aachen University, 2017. ⇒14
Search in Google Scholar Back to article
[45] L. Netz, Using Horner schemes to improve the efficiency and precision of interval constraint propagation. Bachelor’s Thesis, RWTH Aachen University, 2015. ⇒ 14
Search in Google Scholar Back to article
[46] L. Neuberger, Generation of infeasible subsets in less-lazy SMT-solving for the theory of uninterpreted functions. Bachelor’s Thesis, RWTH Aachen University, 2015. ⇒14
Search in Google Scholar Back to article
[47] J. Redies, An extension of the GiNaCRA library for the cylindrical algebraic decomposition. Bachelor’s Thesis, RWTH Aachen University, 2012. ⇒14
Search in Google Scholar Back to article
[48] SMT-COMP 2017 result summary. http://smtcomp.sourceforge.net/2017/results-toc.shtml, 2017. ⇒21
Search in Google Scholar Back to article
[49] S. Schupp, Interval constraint propagation in SMT compliant decision procedures. Master’s thesis, RWTH Aachen University, 2013. ⇒14, 15
Search in Google Scholar Back to article
[50] D. Scully, Preprocessing for solving non-linear real-arithmetic formulas. Bachelor’s Thesis, RWTH Aachen University, 2012. ⇒14
Search in Google Scholar Back to article
[51] G. S. Tseitin, On the complexity of derivation in propositional calculus. in: Automation of Reasoning. Springer, 1983, pp. 466–483. ⇒810.1007/978-3-642-81955-1_28
Search in Google Scholar Back to article
[52] V. X. Tung, T. Van Khanh, M. Ogawa, raSAT: An SMT solver for polynomial constraints. Formal Methods in System Design51, 3 (2017), 462–499. ⇒14, 2010.1007/s10703-017-0284-9
Search in Google Scholar Back to article
[53] T. Viehmann, Projection operators for the CAD. Bachelor’s Thesis, RWTH Aachen University, 2016. ⇒14
Search in Google Scholar Back to article
[54] T. Viehmann, G. Kremer, E. Ábrahám, Comparing different projection operators in the cylindrical algebraic decomposition for SMT solving. Proc. of SC-square’17 (2017), vol. 1974 of CEUR Workshop Proceedings, CEUR-WS.org. ⇒15
Search in Google Scholar Back to article
[55] V. Weispfenning, Quantifier elimination for real algebra – the quadratic case and beyond. Appl. Algebra Eng. Commun. Comput. 8, 2 (1997), 85–101. ⇒1010.1007/s002000050055
Search in Google Scholar Back to article
[56] T. Winkler, Using Thom’s lemma for real algebraic numbers in the CAD. Bachelor’s Thesis, RWTH Aachen University, 2016. ⇒14
Search in Google Scholar Back to article

Modular strategic SMT solving with SMT-RAT

Abstract

Paradigm

My account