zbMATH — the first resource for mathematics

raSAT: an SMT solver for polynomial constraints. (English) Zbl 06623264
Olivetti, Nicola (ed.) et al., Automated reasoning. 8th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-40228-4/pbk; 978-3-319-40229-1/ebook). Lecture Notes in Computer Science 9706. Lecture Notes in Artificial Intelligence, 228-237 (2016).
Summary: This paper presents the raSAT SMT solver for polynomial constraints, which aims to handle them over both reals and integers with simple unified methodologies: (1) raSAT loop for inequalities, which extends the interval constraint propagation with testing to accelerate SAT detection, and (2) a non-constructive reasoning for equations over reals, based on the generalized intermediate value theorem.
For the entire collection see [Zbl 1337.68016].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI
[1] Alliot, J.M., Gotteland, J.B., Vanaret, C., Durand, N., Gianazza, D.: Implementing an interval computation library for OCaml on x86/amd64 architectures. In: ICFP. ACM (2012)
[2] Benhamou, F., Granvilliers, L.: Continuous and interval constraints. In: van Beek, P., Rossi, F., Walsh, T. (eds.) Handbook of Constraint Programming, pp. 571–604. Elsevier, Amsterdam (2006) · doi:10.1016/S1574-6526(06)80020-9
[3] Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: The barcelogic SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 294–298. Springer, Heidelberg (2008) · Zbl 05301117 · doi:10.1007/978-3-540-70545-1_27
[4] Comba, J.L.D., Stolfi, J.: Affine arithmetic and its applications to computer graphics. In: SIBGRAPI 1993, pp. 9–18 (1993)
[5] Corzilius, F., Loup, U., Junges, S., Ábrahám, E.: SMT-RAT: an SMT-compliant nonlinear real arithmetic toolbox. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 442–448. Springer, Heidelberg (2012) · Zbl 06197774 · doi:10.1007/978-3-642-31612-8_35
[6] 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) · Zbl 1204.68191 · doi:10.1007/978-3-540-24605-3_37
[7] Fränzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. JSAT 1, 209–236 (2007) · Zbl 1144.68371
[8] Ganai, M., Ivancic, F.: Efficient decision procedure for non-linear arithmetic constraints using cordic. In: FMCAD 2009, pp. 61–68, November 2009 · doi:10.1109/FMCAD.2009.5351140
[9] Gao, S., Kong, S., Clarke, E.M.: Satisfiability modulo odes. In: FMCAD 2013, pp. 105–112, October 2013
[10] Gao, S., Kong, S., Clarke, E.M.: \[ {\mathsf dReal} \] : an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 208–214. Springer, Heidelberg (2013) · Zbl 1381.68268 · doi:10.1007/978-3-642-38574-2_14
[11] Granvilliers, L., Benhamou, F.: Realpaver: an interval solver using constraint satisfaction techniques. ACM Trans. Math. Softw. 32, 138–156 (2006) · Zbl 1346.65020 · doi:10.1145/1132973.1132980
[12] Hickey, T., Ju, Q., Van Emden, M.H.: Interval arithmetic: from principles to implementation. J. ACM 48(5), 1038–1068 (2001) · Zbl 1323.65047 · doi:10.1145/502102.502106
[13] Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 339–354. Springer, Heidelberg (2012) · Zbl 1358.68257 · doi:10.1007/978-3-642-31365-3_27
[14] Khanh, T.V., Ogawa, M.: SMT for polynomial constraints on real numbers. In: TAPAS 2012. ENTCS, vol. 289, pp. 27–40 (2012) · doi:10.1016/j.entcs.2012.11.004
[15] Messine, F.: Extentions of affine arithmetic: application to unconstrained global optimization. J. UCS 8(11), 992–1015 (2002) · Zbl 1274.65184
[16] Moore, R.: Interval Analysis. Prentice-Hall Series in Automatic Computation. Prentice-Hall, Upper Saddle River (1966) · Zbl 0176.13301
[17] Neumaier, A.: Interval Methods for Systems of Equations. Cambridge Middle East Library. Cambridge University Press, Cambridge (1990)
[18] Passmore, G.O.: Combined decision procedures for nonlinear arithmetics, real and complex. Dissertation, School of Informatics, University of Edinburgh (2011)
[19] Passmore, G.O., Jackson, P.B.: Combined decision techniques for the existential theory of the reals. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) MKM 2009, Held as Part of CICM 2009. LNCS, vol. 5625, pp. 122–137. Springer, Heidelberg (2009) · Zbl 1247.03018 · doi:10.1007/978-3-642-02614-0_14
[20] Ratschan, S.: Efficient solving of quantified inequality constraints over the real numbers. ACM Trans. Comput. Logic 7(4), 723–748 (2006) · Zbl 1367.68270 · doi:10.1145/1183278.1183282
[21] Tseitin, G.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning. Symbolic Computation, pp. 466–483. Springer, Heidelberg (1983) · doi:10.1007/978-3-642-81955-1_28
[22] Tung, V.X., Khanh, T.V., Ogawa, M.: raSAT: SMT for polynomial inequality. In: SMT Workshop 2014, p. 67 (2014) · Zbl 1377.68140
[23] Zankl, H., Middeldorp, A.: Satisfiability of non-linear irrational arithmetic. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 481–500. Springer, Heidelberg (2010) · Zbl 1310.68126 · doi:10.1007/978-3-642-17511-4_27
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.