×

zbMATH — the first resource for mathematics

A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic. (English) Zbl 1453.90186
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, 315-335 (2016).
Summary: The branch-and-bound framework has already been successfully applied in SAT-modulo-theories (SMT) solvers to check the satisfiability of linear integer arithmetic formulas. In this paper we study how it can be used in SMT solvers for non-linear integer arithmetic on top of two real-algebraic decision procedures: the virtual substitution and the cylindrical algebraic decomposition methods. We implemented this approach in our SMT solver SMT-RAT and compared it with the currently best performing SMT solvers for this logic, which are mostly based on bit-blasting. Furthermore, we implemented a combination of our approach with bit-blasting that outperforms the state-of-the-art SMT solvers for most instances.
For the entire collection see [Zbl 1346.68010].

MSC:
90C57 Polyhedral combinatorics, branch-and-bound, branch-and-cut
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Arnon, D.S., Collins, G.E., McCallum, S.: Cylindrical algebraic decomposition I: the basic algorithm. SIAM J. Comput. 13(4), 865–877 (1984) · Zbl 0562.14001 · doi:10.1137/0213054
[2] Arnon, D.S., Collins, G.E., McCallum, S.: Cylindrical algebraic decomposition II: an adjacency algorithm for the plane. SIAM J. Comput. 13(4), 878–889 (1984) · Zbl 0562.14001 · doi:10.1137/0213055
[3] Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., M. Leino, K.R.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006) · Zbl 05189652 · doi:10.1007/11804192_17
[4] Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011) · Zbl 05940712 · doi:10.1007/978-3-642-22110-1_14
[5] Barrett, C.W., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 512–526. Springer, Heidelberg (2006) · Zbl 1165.68480 · doi:10.1007/11916277_35
[6] Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, Chap. 26, pp. 825–885. IOS Press, Amsterdam (2009)
[7] Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009) · Zbl 1183.68568
[8] Borralleras, C., Lucas, S., Navarro-Marset, R., Rodríguez-Carbonell, E., Rubio, A.: Solving non-linear polynomial arithmetic via SAT modulo linear arithmetic. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 294–305. Springer, Heidelberg (2009) · Zbl 1250.68184 · doi:10.1007/978-3-642-02959-2_23
[9] Bouton, T., Caminha B. de Oliveira, D., Déharbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 151–156. Springer, Heidelberg (2009) · Zbl 05587935 · doi:10.1007/978-3-642-02959-2_12
[10] Brown, C.W.: Improved projection for cylindrical algebraic decomposition. J. Symbolic Comput. 32(5), 447–465 (2001) · Zbl 0981.68186 · doi:10.1006/jsco.2001.0463
[11] Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013) · Zbl 1381.68153 · doi:10.1007/978-3-642-36742-7_7
[12] Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) Automata Theory and Formal Languages, vol. 33, pp. 134–183. Springer, Berlin (1975)
[13] Corzilius, F., Ábrahám, E.: Virtual substitution for SMT-solving. In: Owe, O., Steffen, M., Telle, J.A. (eds.) FCT 2011. LNCS, vol. 6914, pp. 360–371. Springer, Heidelberg (2011) · Zbl 1342.68282 · doi:10.1007/978-3-642-22953-4_31
[14] Corzilius, F., Kremer, G., Junges, S., Schupp, S., Ábrahám, E.: SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving. In: Heule, M., et al. (eds.) SAT 2015. LNCS, vol. 9340, pp. 360–368. Springer, Heidelberg (2015) · Zbl 06512585 · doi:10.1007/978-3-319-24318-4_26
[15] Dantzig, G.B.: Linear Programming and Extensions. Princeton University Press, Princeton (1963) · Zbl 0108.33103 · doi:10.1515/9781400884179
[16] Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962) · Zbl 0217.54002 · doi:10.1145/368273.368557
[17] 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) · Zbl 05187406 · doi:10.1007/11817963_11
[18] Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Heidelberg (2014) · Zbl 06349545 · doi:10.1007/978-3-319-08867-9_49
[19] Fränzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetik constraint systems with complex Boolean structure. J. Satisfiability Boolean Model. Comput. 1, 209–236 (2007) · Zbl 1144.68371
[20] Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 340–354. Springer, Heidelberg (2007) · Zbl 1214.68352 · doi:10.1007/978-3-540-72788-0_33
[21] Griggio, A.: A practical approach to satisfiability modulo linear integer arithmetic. J. Satisfiability Boolean Model. Comput. 8, 1–27 (2012) · Zbl 1331.68207
[22] 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
[23] Kim, H., Somenzi, F., Jin, H.S.: Efficient term-ITE conversion for satisfiability modulo theories. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 195–208. Springer, Heidelberg (2009) · Zbl 1247.68254 · doi:10.1007/978-3-642-02777-2_20
[24] McCallum, S.: An improved projection operation for cylindrical algebraic decomposition of three-dimensional space. J. Symbolic Comput. 5(1), 141–161 (1988) · Zbl 0648.68054 · doi:10.1016/S0747-7171(88)80010-5
[25] de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008) · Zbl 05262379 · doi:10.1007/978-3-540-78800-3_24
[26] Schrijver, A.: Theory of Linear and Integer Programming. John Wiley & Sons, Inc., New York (1986) · Zbl 0665.90063
[27] Tung, V.X., Van Khanh, T., Ogawa, M.: raSAT: an SMT solver for polynomial constraints. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 228–237. Springer, Heidelberg (2016) · Zbl 06623264 · doi:10.1007/978-3-319-40229-1_16
[28] Weispfenning, V.: Quantifier elimination for real algebra - the quadratic case and beyond. Appl. Algebra Eng. Commun. Comput. 8(2), 85–101 (1997) · Zbl 0867.03003 · doi:10.1007/s002000050055
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.