Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test. (English) Zbl 1522.68716
Bouajjani, Ahmed (ed.) et al., Automated technology for verification and analysis. 20th international symposium, ATVA 2022, virtual event, October 25–28, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13505, 137-153 (2022).
Summary: We present a method for determining the satisfiability of quantifier-free first-order formulas modulo the theory of non-linear arithmetic over the reals augmented with transcendental functions. Our procedure is based on the fruitful combination of two main ingredients: unconstrained optimisation, to generate a set of candidate solutions, and a result from topology called the topological degree test to check whether a given bounded region contains at least a solution. We have implemented the procedure in a prototype tool called ugotNL, and integrated it within the MathSAT SMT solver. Our experimental evaluation over a wide range of benchmarks shows that it vastly improves the performance of the solver for satisfiable non-linear arithmetic formulas, significantly outperforming other available tools for problems with transcendental functions.
For the entire collection see [Zbl 1511.68011].
For the entire collection see [Zbl 1511.68011].
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
| 55M25 | Degree, winding number |
| 90C30 | Nonlinear programming |
References:
| [1] | Aberth, O., Computation of topological degree using interval arithmetic, and applications, Math. Comput., 62, 205, 171-178 (1994) · Zbl 0798.55002 · doi:10.1090/S0025-5718-1994-1203731-4 |
| [2] | Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org |
| [3] | Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability Modulo Theories, chapter 26 (2009) |
| [4] | Benhamou, F., Granvilliers, L.: Chapter 16 - continuous and interval constraints. In: Handbook of Constraint Programming (2006) · Zbl 1346.65020 |
| [5] | Brauße, F., Korovin, K., Korovina, M.V., Müller, N.T.: The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints. In: CADE (2021) · Zbl 1540.03019 |
| [6] | Barrett, C., et al.: CVC5 at the SMT Competition 2021 (2021) |
| [7] | Cimatti, A.; Griggio, A.; Irfan, A.; Roveri, M.; Sebastiani, R., Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions, ACM Trans. Comput. Logic, 19, 3, 1-52 (2018) · Zbl 1407.68285 · doi:10.1145/3230639 |
| [8] | Cimatti, A.; Griggio, A.; Schaafsma, BJ; Sebastiani, R.; Piterman, N.; Smolka, SA, The MathSAT5 SMT solver, Tools and Algorithms for the Construction and Analysis of Systems, 93-107 (2013), Heidelberg: Springer, Heidelberg · Zbl 1381.68153 · doi:10.1007/978-3-642-36742-7_7 |
| [9] | Collins, GE; Brakhage, H., Quantifier elimination for real closed fields by cylindrical algebraic decompostion, Automata Theory and Formal Languages, 134-183 (1975), Heidelberg: Springer, Heidelberg · Zbl 0318.02051 · doi:10.1007/3-540-07407-4_17 |
| [10] | Corzilius, F.; Kremer, G.; Junges, S.; Schupp, S.; Ábrahám, E.; Heule, M.; Weaver, S., SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving, Theory and Applications of Satisfiability Testing - SAT 2015, 360-368 (2015), Cham: Springer, Cham · Zbl 1471.68241 · doi:10.1007/978-3-319-24318-4_26 |
| [11] | de Moura, L.; Bjørner, N.; Ramakrishnan, CR; Rehof, J., Z3: an efficient SMT solver, Tools and Algorithms for the Construction and Analysis of Systems, 337-340 (2008), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-540-78800-3_24 |
| [12] | de Moura, L.; Jovanović, D.; Giacobazzi, R.; Berdine, J.; Mastroeni, I., A model-constructing satisfiability calculus, Verification, Model Checking, and Abstract Interpretation, 1-12 (2013), Heidelberg: Springer, Heidelberg · Zbl 1426.68251 · doi:10.1007/978-3-642-35873-9_1 |
| [13] | Dutertre, B.; Biere, A.; Bloem, R., Yices 2.2, Computer Aided Verification, 737-744 (2014), Cham: Springer, Cham · doi:10.1007/978-3-319-08867-9_49 |
| [14] | Franek, P.; Ratschan, S., Effective topological degree computation based on interval arithmetic, Math. Comput., 84, 293, 1265-1290 (2015) · Zbl 1318.55002 · doi:10.1090/S0025-5718-2014-02877-9 |
| [15] | Franek, P.; Ratschan, S.; Zgliczynski, P., Quasi-decidability of a fragment of the first-order theory of real numbers, J. Autom. Reasoning, 57, 2, 157-185 (2015) · Zbl 1437.03047 · doi:10.1007/s10817-015-9351-3 |
| [16] | 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 (2007) · Zbl 1144.68371 |
| [17] | Fu, Z.; Su, Z.; Chaudhuri, S.; Farzan, A., XSat: a fast floating-point satisfiability solver, Computer Aided Verification, 187-209 (2016), Cham: Springer, Cham · doi:10.1007/978-3-319-41540-6_11 |
| [18] | Gao, S.; Avigad, J.; Clarke, EM; Gramlich, B.; Miller, D.; Sattler, U., \( \delta \)-complete decision procedures for satisfiability over the reals, Automated Reasoning, 286-300 (2012), Heidelberg: Springer, Heidelberg · Zbl 1358.03028 · doi:10.1007/978-3-642-31365-3_23 |
| [19] | Gao, S.; Kong, S.; Clarke, EM; Bonacina, MP, dReal: an SMT solver for nonlinear theories over the reals, Automated Deduction - CADE-24, 208-214 (2013), Heidelberg: Springer, Heidelberg · Zbl 1381.68268 · doi:10.1007/978-3-642-38574-2_14 |
| [20] | Jovanović, D.; de Moura, L., Solving non-linear arithmetic, ACM Commun. Comput. Algebra, 46, 3-4, 104-105 (2013) · doi:10.1145/2429135.2429155 |
| [21] | Minh, DDL; Minh, DLP, Understanding the hastings algorithm, Commun. Stat. Simul. Comput., 44, 2, 332-349 (2015) · Zbl 1316.65004 · doi:10.1080/03610918.2013.777455 |
| [22] | Moore, R., Kearfott, R., Cloud, M.: Introduction to Interval Analysis (2009) · Zbl 1168.65002 |
| [23] | Neumaier, A.: Interval Methods for Systems of Equations. Cambridge University Press (1991) · Zbl 1152.65054 |
| [24] | O’Regan, D., Je, C.Y., Chen, Y.: Topological Degree Theory and Applications. Taylor and Francis (2006) · Zbl 1095.47001 |
| [25] | Ratschan, S., Safety verification of non-linear hybrid systems is quasi-decidable, Formal Meth. Syst. Des., 44, 1, 71-90 (2013) · Zbl 1291.68266 · doi:10.1007/s10703-013-0196-2 |
| [26] | Richardson, D., Some undecidable problems involving elementary functions of a real variable, J. Symb. Log., 33, 4, 514-520 (1968) · Zbl 0175.27404 · doi:10.2307/2271358 |
| [27] | Xuan, T.V., Khanh, T., Ogawa, M.: rasat: an smt solver for polynomial constraints. Formal Meth. Syst. Des. 51, 12 (2017) · Zbl 1377.68140 |
| [28] | Wales, D.J., Doye, J.P.K.: Global optimization by basin-hopping and the lowest energy structures of lennard-jones clusters containing up to 110 atoms. J. Phys. Chem. A, (28) (1997) |
| [29] | Zhang, L., Madigan, C.F., Moskewicz, M.H., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: ICCAD (2001) |
| [30] | Ábrahám, E.; Davenport, J.; England, M.; Kremer, G., Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings, J. Log. Algebraic Meth. Program., 119, 100633 (2020) · Zbl 1509.68243 · doi:10.1016/j.jlamp.2020.100633 |
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.
