Optimization modulo non-linear arithmetic via incremental linearization. (English) Zbl 07497924
Konev, Boris (ed.) et al., Frontiers of combining systems. 13th international symposium, FroCoS 2021, Birmingham, UK, September 8–10, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12941, 213-231 (2021).
Summary: Incremental linearization is a conceptually simple, yet effective, technique that we have recently proposed for solving SMT problems on the theories of non-linear arithmetic over the reals and the integers. Optimization Modulo Theories (OMT) is an important extension of SMT which allows for finding models that optimize given objective functions. In this paper, we show how incremental linearization can be extended to OMT in a simple way, producing an incomplete though effective OMT procedure. We describe the main ideas and algorithms, we provide an implementation within the OptiMathSAT OMT solver, and perform an empirical evaluation. The results support the effectiveness of the approach.
For the entire collection see [Zbl 1482.68028].
For the entire collection see [Zbl 1482.68028].
MSC:
| 68Txx | Artificial intelligence |
References:
| [1] | https://es-static.fbk.eu/people/mjonas/papers/frocos21_oms/ |
| [2] | https://github.com/roveri-marco/OMTNPlan |
| [3] | Ábrahám, E.; Davenport, JH; 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 Methods Program., 119, 100633 (2021) · Zbl 1509.68243 · doi:10.1016/j.jlamp.2020.100633 |
| [4] | Barrett, C., Ranise, S., Stump, A., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB) (2010). http://www.smtlib.org |
| [5] | Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories, chapter 26, pp. 825-885. Volume 185 of Biere et al. [7], February 2009 |
| [6] | Benhamou, F., Granvilliers, L.: Continuous and interval constraints. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming, Volume 2 of Foundations of Artificial Intelligence, pp. 571-603. Elsevier (2006) · Zbl 1346.65020 |
| [7] | Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. IOS Press, February 2009 · Zbl 1183.68568 |
| [8] | Bjørner, N.; Phan, A-D; Fleckenstein, L.; Baier, C.; Tinelli, C., \( \nu\) Z - an optimizing SMT solver, Tools and Algorithms for the Construction and Analysis of Systems, 194-199 (2015), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-662-46681-0_14 |
| [9] | Borralleras, C., Larraz, D., Rodríguez-Carbonell, E., Oliveras, A., Rubio, A.: Incomplete SMT techniques for solving non-linear formulas over the integers. ACM Trans. Comput. Log. 20(4), 25:1-25:36 (2019) · Zbl 1433.68405 |
| [10] | Borralleras, C.; Lucas, S.; Oliveras, A.; Rodríguez-Carbonell, E.; Rubio, A., SAT modulo linear arithmetic for solving polynomial constraints, J. Autom. Reason., 48, 1, 107-131 (2012) · Zbl 1243.68210 · doi:10.1007/s10817-010-9196-8 |
| [11] | Brauße, F.; Korovin, K.; Korovina, M.; Müller, N.; Herzig, A.; Popescu, A., A CDCL-style calculus for solving non-linear constraints, Frontiers of Combining Systems, 131-148 (2019), Cham: Springer, Cham · Zbl 1435.68300 · doi:10.1007/978-3-030-29007-8_8 |
| [12] | Cimatti, A.; Griggio, A.; Irfan, A.; Roveri, M.; Sebastiani, R.; Beyersdorff, O.; Wintersteiger, CM, Experimenting on solving nonlinear integer arithmetic with incremental linearization, Theory and Applications of Satisfiability Testing - SAT 2018, 383-398 (2018), Cham: Springer, Cham · Zbl 1407.68285 · doi:10.1007/978-3-319-94144-8_23 |
| [13] | 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. Log. 19(3), 19:1-19:52 (2018) · Zbl 1407.68285 |
| [14] | 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 |
| [15] | Collins, GE, Quantifier elimination for real closed fields by cylindrical algebraic decomposition-preliminary report, ACM SIGSAM Bull., 8, 3, 80-90 (1974) · doi:10.1145/1086837.1086852 |
| [16] | Contaldo, F.; Trentin, P.; Sebastiani, R.; Hebrard, E.; Musliu, N., From MiniZinc to optimization modulo theories, and back, Integration of Constraint Programming, Artificial Intelligence, and Operations Research, 148-166 (2020), Cham: Springer, Cham · Zbl 07636017 · doi:10.1007/978-3-030-58942-4_10 |
| [17] | 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 |
| [18] | Dixon, C.; Finger, M., Frontiers of Combining Systems (2017), Cham: Springer, Cham · Zbl 1369.68021 · doi:10.1007/978-3-319-66167-4 |
| [19] | Fontaine, P., Ogawa, M., Sturm, T., Vu, X.: Subtropical satisfiability. In: Dixon and Finger [18], pp. 189-206 · Zbl 1425.68374 |
| [20] | Fuhs, C.; Giesl, J.; Middeldorp, A.; Schneider-Kamp, P.; Thiemann, R.; Zankl, H.; Marques-Silva, J.; Sakallah, KA, SAT solving for termination analysis with polynomial interpretations, Theory and Applications of Satisfiability Testing - SAT 2007, 340-354 (2007), Heidelberg: Springer, Heidelberg · Zbl 1214.68352 · doi:10.1007/978-3-540-72788-0_33 |
| [21] | 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 |
| [22] | Jovanović, D.; Bouajjani, A.; Monniaux, D., Solving nonlinear integer arithmetic with MCSAT, Verification, Model Checking, and Abstract Interpretation, 330-346 (2017), Cham: Springer, Cham · Zbl 1484.68220 · doi:10.1007/978-3-319-52234-0_18 |
| [23] | Jovanovic, D.; de Moura, L., Solving non-linear arithmetic, ACM Commun. Comput. Algebra, 46, 3-4, 104-105 (2012) · doi:10.1145/2429135.2429155 |
| [24] | Kong, S.; Solar-Lezama, A.; Gao, S.; Chockler, H.; Weissenbacher, G., Delta-decision procedures for exists-forall problems over the reals, Computer Aided Verification, 219-235 (2018), Cham: Springer, Cham · Zbl 1511.68252 · doi:10.1007/978-3-319-96142-2_15 |
| [25] | Kremer, G.; Ábrahám, E., Fully incremental cylindrical algebraic decomposition, J. Symb. Comput., 100, 11-37 (2020) · Zbl 1432.68601 · doi:10.1016/j.jsc.2019.07.018 |
| [26] | Kremer, G.; Corzilius, F.; Ábrahám, E.; Gerdt, VP; Koepf, W.; Seiler, WM; Vorozhtsov, EV, A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic, Computer Algebra in Scientific Computing, 315-335 (2016), Cham: Springer, Cham · Zbl 1453.90186 · doi:10.1007/978-3-319-45641-6_21 |
| [27] | Leofante, F., Giunchiglia, E., Ábrahám, E., Tacchella, A.: Optimal planning modulo theories. In: Bessiere, C. (ed.) Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020, pp. 4128-4134. ijcai.org (2020) |
| [28] | Maréchal, A.; Fouilhé, A.; King, T.; Monniaux, D.; Périn, M.; Jobstmann, B.; Leino, KRM, Polyhedral approximation of multivariate polynomials using Handelman’s theorem, Verification, Model Checking, and Abstract Interpretation, 166-184 (2016), Heidelberg: Springer, Heidelberg · Zbl 1475.68093 · doi:10.1007/978-3-662-49122-5_8 |
| [29] | Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers, chapter 4, pp. 131-153. Volume 185 of Biere et al. [7], February 2009 |
| [30] | Matiyasevich, YV, Hilbert’s Tenth Problem (1993), Cambridge: MIT Press, Cambridge · Zbl 0790.03009 |
| [31] | Nadel, A.; Ryvchin, V.; Chechik, M.; Raskin, J-F, Bit-vector optimization, Tools and Algorithms for the Construction and Analysis of Systems, 851-867 (2016), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-662-49674-9_53 |
| [32] | Nieuwenhuis, R.; Oliveras, A.; Biere, A.; Gomes, CP, On SAT modulo theories and optimization problems, Theory and Applications of Satisfiability Testing - SAT 2006, 156-169 (2006), Heidelberg: Springer, Heidelberg · Zbl 1187.68558 · doi:10.1007/11814948_18 |
| [33] | Reynolds, A., Tinelli, C., Jovanovic, D., Barrett, C.W.: Designing theory solvers with extensions. In: Dixon and Finger [33], pp. 22-40 · Zbl 1495.68239 |
| [34] | Sebastiani, R.; Tomasi, S.; Gramlich, B.; Miller, D.; Sattler, U., Optimization in SMT with \({\cal{L}A}({\mathbb{Q}} )\) cost functions, Automated Reasoning, 484-498 (2012), Heidelberg: Springer, Heidelberg · Zbl 1358.68264 · doi:10.1007/978-3-642-31365-3_38 |
| [35] | Sebastiani, R.; Tomasi, S., Optimization modulo theories with linear rational costs, ACM Trans. Comput. Log., 16, 2, 1-46 (2015) · Zbl 1354.68233 · doi:10.1145/2699915 |
| [36] | Sebastiani, R.; Trentin, P.; Baier, C.; Tinelli, C., Pushing the envelope of optimization modulo theories with linear-arithmetic cost functions, Tools and Algorithms for the Construction and Analysis of Systems, 335-349 (2015), Heidelberg: Springer, Heidelberg · Zbl 1420.68197 · doi:10.1007/978-3-662-46681-0_27 |
| [37] | Sebastiani, R.; Trentin, P., OptiMathSAT: a tool for optimization modulo theories, J. Autom. Reason., 64, 423-460 (2020) · Zbl 1468.68206 · doi:10.1007/s10817-018-09508-6 |
| [38] | Stump, A.; Barrett, CW; Dill, DL; Brinksma, E.; Larsen, KG, CVC: a cooperating validity checker, Computer Aided Verification, 500-504 (2002), Heidelberg: Springer, Heidelberg · Zbl 1010.68720 · doi:10.1007/3-540-45657-0_40 |
| [39] | Trentin, P.; Sebastiani, R.; Fontaine, P., Optimization modulo the theory of floating-point numbers, Automated Deduction - CADE 27, 550-567 (2019), Cham: Springer, Cham · Zbl 1535.68320 · doi:10.1007/978-3-030-29436-6_33 |
| [40] | 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 |
| [41] | Zankl, H.; Middeldorp, A.; Clarke, EM; Voronkov, A., Satisfiability of non-linear (Ir)rational arithmetic, Logic for Programming, Artificial Intelligence, and Reasoning, 481-500 (2010), Heidelberg: Springer, Heidelberg · 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. 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.
