raSAT: an SMT solver for polynomial constraints. (English) Zbl 1377.68140

Summary: This paper presents \(\mathbf {raSAT}\) SMT solver, which is aimed to handle polynomial constraints over both reals and integers with simple unified methodologies. Its three main features are (1) a \(\mathbf {raSAT}\) loop for inequalities, which adds testing to interval constraint propagation to accelerate SAT detection, (2) a non-constructive reasoning for equations over reals based on the generalized intermediate value theorem, and (3) soundness of floating-point arithmetic that is guaranteed by (a) rounding up/down over-approximations of intervals, and (b) confirmation of a satisfying instance detected by testing using the iRRAM package, which guarantees error bounds.


68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI


[1] Alliot JM, Gotteland JB, Vanaret C, Durand N, Gianazza D (2012) Implementing an interval computation library for OCaml on x86/amd64 architectures. In: OUD 2012, OCaml users and developers workshop · Zbl 1381.68274
[2] Barr ET, Vo T, Le V, Su Z (2013) Automatic detection of floating-point exceptions. In: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, ACM, New York, POPL ’13, pp 549-560 · Zbl 1301.68087
[3] Benhamou, F; Granvilliers, L; Rossi, F (ed.); Pv, B (ed.); Walsh, T (ed.), Continuous and interval constraints, 571-604, (2006), New York
[4] Bofill, M; Nieuwenhuis, R; Oliveras, A; Rodríguez-Carbonell, E; Rubio, A; Gupta, A (ed.); Malik, S (ed.), The barcelogic SMT solver, 294-298, (2008), Berlin
[5] Brain, M; D’Silva, V; Griggio, A; Haller, L; Kroening, D, Deciding floating-point logic with abstract conflict driven clause learning, Form Methods Syst Des, 45, 213-245, (2014) · Zbl 1317.68110
[6] Comba JLD, Stolfi J (1993) Affine arithmetic and its applications to computer graphics. In: SIBGRAPI’93, pp 9-18 · Zbl 1317.68110
[7] Davenport, JH; Heintz, J, Real quantifier elimination is doubly exponential, J Symb Comput, 5, 29-35, (1988) · Zbl 0663.03015
[8] D’Silva, V; Haller, L; Kroening, D; Tautschnig, M; Flanagan, C (ed.); König, B (ed.), Numeric bounds analysis with conflict-driven learning, 48-63, (2012), Berlin · Zbl 1352.68060
[9] D’Silva V, Haller L, Kroening D (2013) Abstract conflict driven learning. In: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, ACM, New York, POPL ’13, pp 143-154 · Zbl 1301.68156
[10] Dutertre, B; Moura, L; Ball, T (ed.); Jones, RB (ed.), A fast linear-arithmetic solver for DPLL(T), 81-94, (2006), Berlin
[11] Eén, N; Sörensson, N; Giunchiglia, E (ed.); Tacchella, A (ed.), An extensible SAT-solver, 502-518, (2004), Berlin · Zbl 1204.68191
[12] Florian, C; Ulrich, L; Sebastian, J; Erika, Á; Alessandro, C (ed.); Roberto, S (ed.), SMT-RAT: an SMT-compliant nonlinear real arithmetic toolbox, 442-448, (2012), Berlin
[13] Fränzle, M; Herde, C; Teige, T; Ratschan, S; Schubert, T, Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure, J Satisf Boolean Model Comput, 1, 209-236, (2007) · Zbl 1144.68371
[14] Ganai M, Ivancic F (2009) Efficient decision procedure for non-linear arithmetic constraints using cordic. In: Formal methods in computer-aided design, 2009. FMCAD 2009, pp 61-68 · Zbl 1309.90101
[15] Gao, S; Kong, S; Clarke, E; Bonacina, M (ed.), Dreal: an SMT solver for nonlinear theories over the reals, 208-214, (2013), Berlin · Zbl 1381.68268
[16] Gao, S; Kong, S; Clarke, EM, Satisfiability modulo odes, Form Methods Comput Aided Des (FMCAD), 2013, 105-112, (2013)
[17] Goldsztejn A (2006) A branch and prune algorithm for the approximation of non-linear ae-solution sets. In: Proceedings of the 2006 ACM symposium on applied computing, ACM, New York, USA, pp 1650-1654
[18] Granvilliers, L; Benhamou, F, Realpaver: an interval solver using constraint satisfaction techniques, ACM Trans Math Softw, 32, 138-156, (2006) · Zbl 1346.65020
[19] Haller L, Griggio A, Brain M, Kroening D (2012) Deciding floating-point logic with systematic abstraction. In: 2012 formal methods in computer-aided design (FMCAD), pp 131-140 · Zbl 1317.68110
[20] Ishii, D; Goldsztejn, A; Jermann, C, Interval-based projection method for under-constrained numerical systems, Constraints, 17, 432-460, (2012) · Zbl 1309.90101
[21] Jovanović, D; Moura, L; Gramlich, B (ed.); Miller, D (ed.); Sattler, U (ed.), Solving non-linear arithmetic, 339-354, (2012), Berlin · Zbl 1358.68257
[22] Khanh, TV; Ogawa, M, SMT for polynomial constraints on real numbers, Electron Notes Theor Comput Sci, 289, 27-40, (2012)
[23] Loup, U; Scheibler, K; Corzilius, F; Ábrahám, E; Becker, B; Bonacina, MP (ed.), A symbiosis of interval constraint propagation and cylindrical algebraic decomposition, 193-207, (2013), Berlin · Zbl 1381.68274
[24] Messine, F, Extentions of affine arithmetic: application to unconstrained global optimization, J Univers Comput Sci, 8, 992-1015, (2002) · Zbl 1274.65184
[25] Miyajima, S; Miyata, T; Kashiwagi, M, A new dividing method in affine arithmetic, IEICE Trans Fundam Electron Commun Comput Sci, E86-A, 2192-2196, (2003)
[26] Moore R (1966) Interval analysis. Prentice-Hall, Englewood Cliffs · Zbl 0176.13301
[27] Neumaier A (1990) Interval methods for systems of equations. Cambridge University Press, Cambridge · Zbl 0715.65030
[28] Ngoc DTB, Ogawa M (2009) Overflow and roundoff error analysis via model checking. In: Proceedings of the 2009 seventh IEEE international conference on software engineering and formal methods, IEEE computer society, Washington, SEFM ’09, pp 105-114
[29] Nieuwenhuis, R; Oliveras, A; Tinelli, C, Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-logemann-loveland procedure to DPLL(T), J ACM, 53, 937-977, (2006) · Zbl 1326.68164
[30] Passmore GO (2011) Combined decision procedures for nonlinear arithmetics, real and complex. Dissertation, School of informatics, University of Edinburgh · Zbl 1352.68060
[31] Passmore, GO; Jackson, PB; Carette, J (ed.); Dixon, L (ed.); Coen, CS (ed.); Watt, SM (ed.), Combined decision techniques for the existential theory of the reals, 122-137, (2009), Berlin · Zbl 1247.03018
[32] Ratschan, S, Efficient solving of quantified inequality constraints over the real numbers, ACM Trans Comput Log, 7, 723-748, (2006) · Zbl 1367.68270
[33] Rennie, B; Dobson, A, On Stirling numbers of the second kind, J Comb Theory, 7, 116-121, (1969) · Zbl 0174.04002
[34] Stolfi J, Figueiredo LHD (1997) Self-validated numerical methods and applications. In: Monograph for 21st Brazilian mathematics colloquium · Zbl 1310.68126
[35] Sturm T (2015) Subtropical real root finding. In: Proceedings of the 2015 ACM on international symposium on symbolic and algebraic computation, ACM, New York, ISSAC ’15, pp 347-354 · Zbl 1345.68296
[36] Tseitin, G; Siekmann, JH (ed.); Wrightson, G (ed.), On the complexity of derivation in propositional calculus, (1983), Berlin
[37] Tung, VX; Khanh, T; Ogawa, M; Olivetti, N (ed.); Tiwari, A (ed.), Rasat: an SMT solver for polynomial constraints, 228-237, (2016), Cham · Zbl 1475.68359
[38] Zankl, H; Middeldorp, A; Clarke, EM (ed.); Voronkov, A (ed.), Satisfiability of non-linear (ir)rational arithmetic, 481-500, (2010), Berlin · Zbl 1310.68126
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.