×

zbMATH — the first resource for mathematics

Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings. (English) Zbl 07316066
Summary: We present a new algorithm for determining the satisfiability of conjunctions of non-linear polynomial constraints over the reals, which can be used as a theory solver for satisfiability modulo theory (SMT) solving for non-linear real arithmetic. The algorithm is a variant of Cylindrical Algebraic Decomposition (CAD) adapted for satisfiability, where solution candidates (sample points) are constructed incrementally, either until a satisfying sample is found or sufficient samples have been sampled to conclude unsatisfiability. The choice of samples is guided by the input constraints and previous conflicts.
The key idea behind our new approach is to start with a partial sample; demonstrate that it cannot be extended to a full sample; and from the reasons for that rule out a larger space around the partial sample, which build up incrementally into a cylindrical algebraic covering of the space. There are similarities with the incremental variant of CAD, the NLSAT method of Jovanović and de Moura, and the NuCAD algorithm of Brown; but we present worked examples and experimental results on a preliminary implementation to demonstrate the differences to these, and the benefits of the new approach.
MSC:
68W30 Symbolic computation and algebraic computation
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Sturm, T., New domains for applied quantifier elimination, (Proceedings of the 9th International Workshop on Computer Algebra in Scientific Computing. Proceedings of the 9th International Workshop on Computer Algebra in Scientific Computing, CASC 2006. Proceedings of the 9th International Workshop on Computer Algebra in Scientific Computing. Proceedings of the 9th International Workshop on Computer Algebra in Scientific Computing, CASC 2006, LNCS, vol. 4194 (2006), Springer), 295-301 · Zbl 1141.68714
[2] Bradford, R.; Davenport, J. H.; England, M.; Errami, H.; Gerdt, V.; Grigoriev, D.; Hoyt, C.; Košta, M.; Radulescu, O.; Sturm, T.; Weber, A., A case study on the parametric occurrence of multiple steady states, (Proceedings of the 42nd International Symposium on Symbolic and Algebraic Computation. Proceedings of the 42nd International Symposium on Symbolic and Algebraic Computation, ISSAC 2017 (2017), ACM), 45-52 · Zbl 1444.92034
[3] Mulligan, C. B.; Davenport, J. H.; England, M., TheoryGuru: a Mathematica package to apply quantifier elimination technology to economics, (Proceedings of the 6th International Congress on Mathematical Software. Proceedings of the 6th International Congress on Mathematical Software, ICMS 2018. Proceedings of the 6th International Congress on Mathematical Software. Proceedings of the 6th International Congress on Mathematical Software, ICMS 2018, LNCS, vol. 10931 (2018), Springer), 369-378 · Zbl 1395.68350
[4] Arai, N. H.; Matsuzaki, T.; Iwane, H.; Anai, H., Mathematics by machine, (Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation. Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation, ISSAC 2014 (2014), ACM), 1-8 · Zbl 1325.68212
[5] Tarski, A., A Decision Method for Elementary Algebra and Geometry, (Caviness, B. F.; Johnson, J. R., Quantifier Elimination and Cylindrical Algebraic Decomposition (1998), Springer), 24-84 (1951), Univ. Cal. Press, reprinted in · Zbl 0900.03045
[6] Collins, G. E., Quantifier elimination for real closed fields by cylindrical algebraic decomposition, (Caviness, B. F., Proceedings of the 2nd GI Conference on Automata Theory & Formal Languages. Proceedings of the 2nd GI Conference on Automata Theory & Formal Languages, LNCS, vol. 33 (1975), Springer). (Johnson, J. R., Quantifier Elimination and Cylindrical Algebraic Decomposition (1998), Springer), 85-121, reprinted in · Zbl 0900.03055
[7] England, M.; Bradford, R.; Davenport, J. H., Improving the use of equational constraints in cylindrical algebraic decomposition, (Proceedings of the 40th International Symposium on Symbolic and Algebraic Computation. Proceedings of the 40th International Symposium on Symbolic and Algebraic Computation, ISSAC 2015 (2015), ACM), 165-172 · Zbl 1346.68283
[8] England, M.; Davenport, J. H., The complexity of cylindrical algebraic decomposition with respect to polynomial degree, (Proceedings of the 18th International Workshop on Computer Algebra in Scientific Computing. Proceedings of the 18th International Workshop on Computer Algebra in Scientific Computing, CASC 2016. Proceedings of the 18th International Workshop on Computer Algebra in Scientific Computing. Proceedings of the 18th International Workshop on Computer Algebra in Scientific Computing, CASC 2016, LNCS, vol. 9890 (2016), Springer), 172-192 · Zbl 1453.13079
[9] M. England, R. Bradford, J. Davenport, Cylindrical algebraic decomposition with equational constraints, in: Davenport, et al. (Eds.), [55], 2019, pp. 38-71 https://doi.org/10.1016/j.jsc.2019.07.019. · Zbl 1432.68599
[10] Brown, C. W.; Davenport, J. H., The complexity of quantifier elimination and cylindrical algebraic decomposition, (Proceedings of the 2007 International Symposium on Symbolic and Algebraic Computation. Proceedings of the 2007 International Symposium on Symbolic and Algebraic Computation, ISSAC 2007 (2007), ACM), 54-60 · Zbl 1190.68028
[11] Basu, S.; Pollack, R.; Roy, M. F., Algorithms in Real Algebraic Geometry, Algorithms and Computations in Mathematics (2006), Springer
[12] Hong, H., Comparison of several decision algorithms for the existential theory of the reals (1991), Tech. rep., RISC, Linz (Report Number 91-41)
[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] Maréchal, A.; Fouilhé, A.; King, T.; Monniaux, D.; Périn, M., Polyhedral approximation of multivariate polynomials using Handelman’s theorem, (Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation. Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2016. Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation. Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2016, LNCS, vol. 9583 (2016), Springer), 166-184 · Zbl 06559857
[15] 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
[16] Tung, V. X.; Van Khanh, T.; Ogawa, M., raSAT: an SMT solver for polynomial constraints, Form. Methods Syst. Des., 51, 3, 462-499 (2017) · Zbl 1377.68140
[17] 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
[18] Corzilius, F.; Ábrahám, E., Virtual substitution for SMT solving, (Proceedings of the 18th International Symposium on Fundamentals of Computation Theory. Proceedings of the 18th International Symposium on Fundamentals of Computation Theory, FCT 2011. Proceedings of the 18th International Symposium on Fundamentals of Computation Theory. Proceedings of the 18th International Symposium on Fundamentals of Computation Theory, FCT 2011, LNCS, vol. 6914 (2011), Springer), 360-371 · Zbl 1342.68282
[19] Fontaine, P.; Ogawa, M.; Sturm, T.; Vu, X. T., Subtropical satisfiability, (Proceedings of the 11th International Symposium on Frontiers of Combining Systems. Proceedings of the 11th International Symposium on Frontiers of Combining Systems, FroCoS 2017. Proceedings of the 11th International Symposium on Frontiers of Combining Systems. Proceedings of the 11th International Symposium on Frontiers of Combining Systems, FroCoS 2017, LNCS, vol. 10483 (2017), Springer), 189-206 · Zbl 1425.68374
[20] Abbott, J.; Bigatti, A. M., CoCoALib: a C++ library for computations in commutative algebra .. and beyond, (Proceedings of the 3rd International Congress on Mathematical Software. Proceedings of the 3rd International Congress on Mathematical Software, ICMS 2010. Proceedings of the 3rd International Congress on Mathematical Software. Proceedings of the 3rd International Congress on Mathematical Software, ICMS 2010, LNCS, vol. 6327 (2010), Springer), 73-76 · Zbl 1267.13048
[21] Wilson, D.; Bradford, R.; Davenport, J. H.; England, M., Cylindrical algebraic sub-decompositions, Math. Comput. Sci., 8, 263-288 (2014) · Zbl 1309.68232
[22] Collins, G. E.; Hong, H., Partial cylindrical algebraic decomposition for quantifier elimination, J. Symb. Comput., 12, 30, 299-328 (1991) · Zbl 0754.68063
[23] Collins, G. E., Quantifier elimination by cylindrical algebraic decomposition — twenty years of progress, (Caviness, B. F.; Johnson, J. R., Quantifier Elimination and Cylindrical Algebraic Decomposition (1998), Springer), 8-23 · Zbl 0900.03053
[24] McCallum, S., On projection in CAD-based quantifier elimination with equational constraint, (Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation. Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation, ISSAC 1999 (1999), ACM), 145-149
[25] Bradford, R. J.; Davenport, J. H.; England, M.; McCallum, S.; Wilson, D. J., Truth table invariant cylindrical algebraic decomposition, J. Symb. Comput., 76, 1-35 (2016) · Zbl 1351.68314
[26] Jovanović, D., Solving nonlinear integer arithmetic with MCSAT, (Proceedings of the 18th International Conference on Verification, Model Checking, and Abstract Interpretation. Proceedings of the 18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017. Proceedings of the 18th International Conference on Verification, Model Checking, and Abstract Interpretation. Proceedings of the 18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017, LNCS, vol. 10145 (2017), Springer), 330-346 · Zbl 06687364
[27] Brown, C. W., Open non-uniform cylindrical algebraic decompositions, (Proceedings of the 40th International Symposium on Symbolic and Algebraic Computation. Proceedings of the 40th International Symposium on Symbolic and Algebraic Computation, ISSAC 2015 (2015), ACM), 85-92 · Zbl 1346.68273
[28] Barrett, C. W.; Fontaine, P.; Tinelli, C., The satisfiability modulo theories library (SMT-LIB) (2016)
[29] Seidenberg, A., A new decision method for elementary algebra, Ann. Math., 60, 2, 365-374 (1954) · Zbl 0056.01804
[30] Barrett, C.; Sebastiani, R.; Seshia, S.; Tinelli, C., Satisfiability modulo theories, (Biere, A.; Heule, M.; van Maaren, H.; Walsh, T., Handbook of Satisfiability. Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185 (2009), IOS Press), 825-885
[31] Ábrahám, E., Building bridges between symbolic computation and satisfiability checking, (Proceedings of the 40th International Symposium on Symbolic and Algebraic Computation. Proceedings of the 40th International Symposium on Symbolic and Algebraic Computation, ISSAC 2015 (2015), ACM), 1-6 · Zbl 1345.68279
[32] Ábrahám, E.; Abbott, J.; Becker, B.; Bigatti, A. M.; Brain, M.; Buchberger, B.; Cimatti, A.; Davenport, J. H.; England, M.; Fontaine, P.; Forrest, S.; Griggio, A.; Kroening, D.; Seiler, W. M.; Sturm, T., \( \mathsf{SC}^2\): satisfiability checking meets symbolic computation, (Proceedings of the 9th International Conference on Intelligent Computer Mathematics. Proceedings of the 9th International Conference on Intelligent Computer Mathematics, CICM 2016. Proceedings of the 9th International Conference on Intelligent Computer Mathematics. Proceedings of the 9th International Conference on Intelligent Computer Mathematics, CICM 2016, LNCS, vol. 9791 (2016), Springer), 28-43 · Zbl 1344.68198
[33] Corzilius, F.; Kremer, G.; Junges, S.; Schupp, S.; Ábrahám, E., SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving, (Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing. Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing, SAT 2015. Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing. Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing, SAT 2015, LNCS, vol. 9340 (2015), Springer), 360-368 · Zbl 06512585
[34] Fontaine, P.; Ogawa, M.; Sturm, T.; Khanh To, V.; Tung Vu, X., Wrapping computer algebra is surprisingly successful for non-linear SMT, (Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation \(( \mathsf{SC}^2 2018)\), no. 2189 in CEUR Workshop Proceedings (2018)), 110-117
[35] G. Kremer, E. Ábrahám, Fully incremental CAD, in: Davenport, et al. (Eds.), [55], 2019, pp. 11-37 https://doi.org/10.1016/j.jsc.2019.07.018. · Zbl 1432.68601
[36] Jovanović, D.; de Moura, L., Solving non-linear arithmetic, (Proceedings of the 6th International Joint Conference on Automated Reasoning. Proceedings of the 6th International Joint Conference on Automated Reasoning, IJCAR 2012. Proceedings of the 6th International Joint Conference on Automated Reasoning. Proceedings of the 6th International Joint Conference on Automated Reasoning, IJCAR 2012, LNCS, vol. 7364 (2012), Springer), 339-354 · Zbl 1358.68257
[37] Jaroschek, M.; Dobaland, P. F.; Fontaine, P., Adapting real quantifier elimination methods for conflict set computation, (Proceedings of the 10th International Symposium on Frontiers of Combining Systems. Proceedings of the 10th International Symposium on Frontiers of Combining Systems, FroCoS 2015. Proceedings of the 10th International Symposium on Frontiers of Combining Systems. Proceedings of the 10th International Symposium on Frontiers of Combining Systems, FroCoS 2015, LNCS, vol. 9322 (2015), Springer), 151-166 · Zbl 06688813
[38] McCallum, S., An improved projection operation for cylindrical algebraic decomposition, (Caviness, B.; Johnson, J., Quantifier Elimination and Cylindrical Algebraic Decomposition. Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts & Monographs in Symbolic Computation (1998), Springer-Verlag), 242-268 · Zbl 0900.68279
[39] Hong, H., An improvement of the projection operator in cylindrical algebraic decomposition, (Proceedings of the International Symposium on Symbolic and Algebraic Computation. Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC 1990 (1990), ACM), 261-264
[40] McCallum, S.; Parusińiski, A.; Paunescu, L., Validity proof of Lazard’s method for CAD construction, J. Symb. Comput., 92, 52-69 (2019) · Zbl 1419.14084
[41] Lazard, D., An improved projection for cylindrical algebraic decomposition, (Bajaj, C., Algebraic Geometry and Its Applications: Collections of Papers from Abhyankar’s 60th Birthday Conference (1994), Springer: Springer Berlin), 467-476 · Zbl 0822.68118
[42] Brown, C., Projection and quantifier elimination using non-uniform cylindrical algebraic decomposition, (Proceedings of the 42nd International Symposium on Symbolic and Algebraic Computation. Proceedings of the 42nd International Symposium on Symbolic and Algebraic Computation, ISSAC 2017 (2017), ACM), 53-60 · Zbl 1457.68323
[43] Chen, C.; Moreno Maza, M., Cylindrical algebraic decomposition in the RegularChains library, (Hong, H.; Yap, C., Mathematical Software - ICMS 2014. Mathematical Software - ICMS 2014, LNCS, vol. 8592 (2014), Springer: Springer Heidelberg), 425-433 · Zbl 1437.14007
[44] Franzen, H., Conflict driven cylindrical algebraic coverings for nonlinear arithmetic in SMT solving (2020), RWTH Aachen University, Master’s thesis
[45] Nalbach, J.; Kremer, G.; Ábrahám, E., On variable orderings in MCSAT for non-linear real arithmetic, (Satisfiability Checking and Symbolic Computation. Satisfiability Checking and Symbolic Computation, CEUR Workshop Proceedings, vol. 2460 (2019)), 6:1-6:7
[46] Hentze, W., Computing minimal infeasible subsets for the cylindrical algebraic decomposition (2017), RWTH Aachen University, Bachelor’s thesis
[47] England, M.; Florescu, D., Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition, (Kaliszyk, C.; Brady, E.; Kohlhase, A.; Sacerdoti, C., Intelligent Computer Mathematics. Intelligent Computer Mathematics, LNCS, vol. 11617 (2019), Springer International Publishing), 93-108 · Zbl 1428.68399
[48] Xu, L.; Hutter, F.; Hoos, H.; Leyton-Brown, K., SATzilla: portfolio-based algorithm selection for SAT, J. Artif. Intell. Res., 32, 565-606 (2008) · Zbl 1182.68272
[49] de Moura, L.; Jovanović, D., A model-constructing satisfiability calculus, (Proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation. Proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2013. Proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation. Proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2013, LNCS, vol. 7737 (2013), Springer), 1-12 · Zbl 1426.68251
[50] Huang, Z.; England, M.; Wilson, D.; Bridge, J.; Davenport, J.; Paulson, L., Using machine learning to improve cylindrical algebraic decomposition, Math. Comput. Sci., 13, 4, 461-488 (2019) · Zbl 07137257
[51] Florescu, D.; England, M., Algorithmically generating new algebraic features of polynomial systems for machine learning, (Abbott, J.; Griggio, A., Proceedings of the 4th Workshop on Satisfiability Checking and Symbolic Computation \(( \mathsf{SC}^2 2019)\), no. 2460 in CEUR Workshop Proceedings (2019)), 4:1-4:12 (2019)
[52] Florescu, D.; England, M., Improved cross-validation for classifiers that make algorithmic choices to minimise runtime without compromising output correctness, (Slamanig, D.; Tsigaridas, E.; Zafeirakopoulos, Z., Mathematical Aspects of Computer and Information Sciences. Mathematical Aspects of Computer and Information Sciences, LNCS, vol. 11989 (2019), Springer International Publishing), 341-356
[53] Brown, C.; McCallum, S., Enhancements to Lazard’s method for cylindrical algebraic decomposition, (Boulier, F.; England, M.; Sadykov, T.; Vorozhtsov, E., Computer Algebra in Scientific Computing. Computer Algebra in Scientific Computing, Lecture Notes in Computer Science, vol. 12291 (2020), Springer International Publishing), 129-149
[54] Ábrahám, E.; Davenport, J.; England, M.; Kremer, G.; Tonks, Z., New opportunities for the formal proof of computational real geometry?, (Proceedings of the 5th Workshop on Satisfiability Checking and Symbolic Computation \(( \mathsf{SC}^2 2020)\), no. 2752 in CEUR Workshop Proceedings (2020)), 178-188
[55] Davenport, J.; England, M.; Griggio, A.; Sturm, T.; Tinelli, C., Symbolic computation and satisfiability checking: Special Issue. Symbolic computation and satisfiability checking: Special Issue, J. Symb. Comput., 100 (2020) · Zbl 1444.68006
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.