Solving nonlinear integer arithmetic with MCSAT. (English) Zbl 1484.68220
Bouajjani, Ahmed (ed.) et al., Verification, model checking, and abstract interpretation. 18th international conference, VMCAI 2017, Paris, France, January 15–17, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10145, 330-346 (2017).
Summary: We present a new method for solving nonlinear integer arithmetic constraints. The method relies on the MCSat approach to solving nonlinear constraints, while using branch and bound in a conflict-directed manner. We report encouraging experimental results where the new procedure outperforms state-of-the-art SMT solvers based on bit-blasting.
For the entire collection see [Zbl 1355.68009].
For the entire collection see [Zbl 1355.68009].
MSC:
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
References:
| [1] | Albrecht, R., Buchberger, B., Collins, G.E., Loos, R.: Computer Algebra: Symbolic and Algebraic Computation, vol. 4. Springer, Vienna (2012) |
| [2] | 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). doi: 10.1007/978-3-642-22110-1_14 · doi:10.1007/978-3-642-22110-1_14 |
| [3] | Barrett, C., Stump, A., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB), vol. 15, pp. 18–52 (2010). www.SMT-LIB.org |
| [4] | Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. Handb. Satisf. 185, 825–885 (2009) |
| [5] | Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Automata Theory and Formal Languages 2nd GI Conference Kaiserslautern, 20–23 May, pp. 134–183 (1975) |
| [6] | 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., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 360–368. Springer, Heidelberg (2015). doi: 10.1007/978-3-319-24318-4_26 · Zbl 1471.68241 · doi:10.1007/978-3-319-24318-4_26 |
| [7] | de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-78800-3_24 · doi:10.1007/978-3-540-78800-3_24 |
| [8] | 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). doi: 10.1007/978-3-642-35873-9_1 · Zbl 1426.68251 · doi:10.1007/978-3-642-35873-9_1 |
| [9] | Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Heidelberg (2014). doi: 10.1007/978-3-319-08867-9_49 · doi:10.1007/978-3-319-08867-9_49 |
| [10] | Dutertre, B., 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 · doi:10.1007/11817963_11 |
| [11] | Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004). doi: 10.1007/978-3-540-24605-3_37 · Zbl 1204.68191 · doi:10.1007/978-3-540-24605-3_37 |
| [12] | 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). doi: 10.1007/978-3-540-72788-0_33 · Zbl 1214.68352 · doi:10.1007/978-3-540-72788-0_33 |
| [13] | Giesl, J., et al.: Proving termination of programs automatically with AProVE. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 184–191. Springer, Heidelberg (2014). doi: 10.1007/978-3-319-08587-6_13 · Zbl 1409.68256 · doi:10.1007/978-3-319-08587-6_13 |
| [14] | Gomory, R.E.: Outline of an algorithm for integer solutions to linear programs. Bull. Am. Math. Soc. 64(5), 275–278 (1958) · Zbl 0085.35807 · doi:10.1090/S0002-9904-1958-10224-4 |
| [15] | Griggio, A.: A practical approach to satisfiability modulo linear integer arithmetic. J. Satisf. Boolean Model. Comput. 8, 1–27 (2012) · Zbl 1331.68207 |
| [16] | Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36–52. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-39799-8_2 · doi:10.1007/978-3-642-39799-8_2 |
| [17] | Jovanović, D.: SMT beyond DPLL(T): a new approach to theory solvers and theory combination. Ph.D. thesis, Courant Institute of Mathematical Sciences, New York (2012) |
| [18] | Jovanović, D., Barrett, C., De Moura, L.: The design and implementation of the model constructing satisfiability calculus. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 173–180 (2013) · doi:10.1109/FMCAD.2013.7027033 |
| [19] | Jovanović, D., De Moura, L.: Solving non-linear arithmetic. In: International Joint Conference on Automated Reasoning, pp. 339–354 (2012) · Zbl 1358.68257 · doi:10.1007/978-3-642-31365-3_27 |
| [20] | Jovanović, D., De Moura, L.: Cutting to the chase: solving linear integer arithmetic. J. Autom. Reason. 51(1), 79–108 (2013) · Zbl 1314.90053 · doi:10.1007/s10817-013-9281-x |
| [21] | King, T.: Effective algorithms for the satisfiability of quantifier-free formulas over linear real and integer arithmetic. Ph.D. thesis, Courant Institute of Mathematical Sciences, New York (2014) |
| [22] | Kremer, G., Corzilius, F., Ábrahám, E.: A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) CASC 2016. LNCS, vol. 9890, pp. 315–335. Springer, Heidelberg (2016). doi: 10.1007/978-3-319-45641-6_21 · Zbl 1453.90186 · doi:10.1007/978-3-319-45641-6_21 |
| [23] | Leike, J., Heizmann, M.: Geometric series as nontermination arguments for linear lasso programs. In: 14th International Workshop on Termination, p. 55 (2014) |
| [24] | Lopes, N.P., Aksoy, L., Manquinho, V., Monteiro, J.: Optimally solving the MCM problem using pseudo-boolean satisfiability (2011) |
| [25] | Matiyasevich, Y.V.: Hilbert’s Tenth Problem. The MIT Press, Cambridge (1993) · Zbl 0790.03009 |
| [26] | Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Annual Design Automation Conference, pp. 530–535 (2001) · doi:10.1145/378239.379017 |
| [27] | Papadimitriou, C.H.: On the complexity of integer programming. J. ACM 28(4), 765–768 (1981) · Zbl 0468.68050 · doi:10.1145/322276.322287 |
| [28] | Robinson, G., Wos, L.: Paramodulation and theorem-proving in first-order theories with equality. Mach. Intell. 4, 135–150 (1969) · Zbl 0219.68047 |
| [29] | Tarski, A.: A decision method for elementary algebra and geometry. Technical report R-109, Rand Corporation (1951) · Zbl 0044.25102 |
| [30] | 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. 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.
