×

Modular strategic SMT solving with SMT-RAT. (English) Zbl 1412.68270

Summary: 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.

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68-04 Software, source code, etc. for problems pertaining to computer science
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI

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, 12; · Zbl 1267.13048
[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;
[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. ⇒12;
[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, 14;
[5] C. Barrett, P. Fontaine, C. Tinelli, The Satisfiability Modulo Theories Library (SMT-LIB). , 2016. ⇒20;
[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, 12; · Zbl 1017.68163
[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, 14;
[8] M. Bromberger, C. Weidenbach, Fast cube tests for LIA constraint solving. Proc. of IJCAR’16 (2016), Springer, pp. 116-132. ⇒15; · Zbl 1475.68337
[9] C. W. Brown, M. Košta, Constructing a single cell in cylindrical algebraic decomposition, Journal of Symbolic Computation70 (2015) 14-48. ⇒17; · Zbl 1314.68414
[10] B. Buchberger, Gröbner bases: Applications. in: The Concise Handbook of Algebra. Kluwer Academic Publishers, 2002, pp. 265-268. ⇒12;
[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. ⇒ 12;
[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. ⇒9; · Zbl 1381.68153
[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, 12;
[14] F. Corzilius, Virtual substitution in SMT solving, Diploma thesis, RWTH Aachen University, 2011. ⇒14; · Zbl 1342.68282
[15] F. Corzilius, Integrating Virtual Substitution into Strategic SMT Solving. PhD thesis, RWTH Aachen University, 2016. ⇒15;
[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, 20; · Zbl 1471.68241
[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, 7;
[18] G. B. Dantzig, Linear programming and extensions. Princeton University Press, 1963. ⇒10; · Zbl 0108.33103
[19] M. Davis, H. Putnam, A computing procedure for quantification theory. Journal of the ACM7, 3 (1960) 201-215. ⇒8; · Zbl 0212.34203
[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, 14;
[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; · Zbl 1426.68251
[22] B. Dutertre, Yices 2.2. Proc. of CAV’14 (2014), vol. 8559 of LNCS, Springer, pp. 737-744. ⇒9, 14;
[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. ⇒15;
[24] N. Eén, N. Sörensson, An extensible SAT-solver. Proc. of SAT’03 (2004), vol. 2919 of LNCS, Springer, pp. 502-518. ⇒15; · Zbl 1204.68191
[25] P. Fontaine, M. Ogawa, T. Sturm, T., X. T. Vu, Subtropical satisfiability. Proc. of FroCoS’17 (2017), Springer, pp. 189-206. ⇒11, 16; · Zbl 1425.68374
[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. ⇒15; · Zbl 1214.68352
[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;
[28] K. O. Geddes, S. R. Czapor, G. Labahn, Algorithms for Computer Algebra. Kluwer Academic Publishers, 1992. ⇒7; · Zbl 0805.68072
[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. ⇒9; · Zbl 1409.68256
[30] M. Grobelna, SAT-modulo-theories solving for pseudo-Boolean constraints. Bachelor’s Thesis, RWTH Aachen University, 2017. ⇒14, 15;
[31] R. Haehn, Using equational constraints in an incremental CAD projection. Master’s thesis, RWTH Aachen University, 2017. ⇒14;
[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. ⇒12;
[33] W. Hentze, Infeasible subsets for nonlinear SMT. Bachelor’s Thesis, RWTH Aachen University, 2017. ⇒14;
[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;
[35] D. Jovanović, Solving nonlinear integer arithmetic with MCSAT. Proc. of VM-CAI’17 (2017), Springer, pp. 330-346. ⇒20; · Zbl 1484.68220
[36] D. Jovanović, L. de Moura, Solving non-linear arithmetic. Proc. of IJCAR’12 (2012), vol. 7364 of LNAI, Springer, pp. 339-354. ⇒16; · Zbl 1358.68257
[37] S. Junges, On Gröbner bases in SMT-compliant decision procedures. Bachelor’s Thesis, RWTH Aachen University, 2012. ⇒14;
[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. ⇒15; · Zbl 1398.68696
[39] T. V. Khanh, X. Vu, M. Ogawa, raSAT: SMT for polynomial inequality. Proc. of SMT’14 (2014), p. 67. ⇒9;
[40] G. Kremer, Isolating real roots using adaptable-precision interval arithmetic. Master’s thesis, RWTH Aachen University, 2013. ⇒14;
[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, 20; · Zbl 1453.90186
[42] A. Krüger, Bitvectors in SMT-RAT and their application to integer arithmetics. Master’s thesis, RWTH Aachen University, 2015. ⇒14, 15;
[43] J. P. Marques-Silva, K. A. Sakallah, Grasp: A search algorithm for propositional satisfiability. IEEE Transactions on Computers48 (1999) 506-521. ⇒8; · Zbl 1392.68388
[44] J. Nalbach, Embedding the virtual substitution in the MCSAT framework. Bachelor’s Thesis, RWTH Aachen University, 2017. ⇒14;
[45] L. Netz, Using Horner schemes to improve the efficiency and precision of interval constraint propagation. Bachelor’s Thesis, RWTH Aachen University, 2015. ⇒ 14;
[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;
[47] J. Redies, An extension of the GiNaCRA library for the cylindrical algebraic decomposition. Bachelor’s Thesis, RWTH Aachen University, 2012. ⇒14;
[48] SMT-COMP 2017 result summary. , 2017. ⇒21;
[49] S. Schupp, Interval constraint propagation in SMT compliant decision procedures. Master’s thesis, RWTH Aachen University, 2013. ⇒14, 15;
[50] D. Scully, Preprocessing for solving non-linear real-arithmetic formulas. Bachelor’s Thesis, RWTH Aachen University, 2012. ⇒14;
[51] G. S. Tseitin, On the complexity of derivation in propositional calculus. in: Automation of Reasoning. Springer, 1983, pp. 466-483. ⇒8;
[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, 20; · Zbl 1377.68140
[53] T. Viehmann, Projection operators for the CAD. Bachelor’s Thesis, RWTH Aachen University, 2016. ⇒14;
[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;
[55] V. Weispfenning, Quantifier elimination for real algebra - the quadratic case and beyond. Appl. Algebra Eng. Commun. Comput. 8, 2 (1997), 85-101. ⇒10; · Zbl 0867.03003
[56] T. Winkler, Using Thom’s lemma for real algebraic numbers in the CAD. Bachelor’s Thesis, RWTH Aachen University, 2016. ⇒14;
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.