×

zbMATH — the first resource for mathematics

Fully incremental cylindrical algebraic decomposition. (English) Zbl 1432.68601
Summary: Collins introduced the cylindrical algebraic decomposition method for eliminating quantifiers in real arithmetic formulas. In our work we use this method for satisfiability checking in satisfiability modulo theories solver technologies, and tune it by trying to avoid some computation steps that are needed for quantifier elimination but not for satisfiability checking. We further propose novel data structures and adapt the method to work incrementally and to support backtracking. We verify the effectiveness experimentally by comparing different versions of the cylindrical algebraic decomposition used within a state-of-the-art satisfiability modulo theories solver.

MSC:
68W30 Symbolic computation and algebraic computation
68R07 Computational aspects of satisfiability
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Barrett, C.; Fontaine, P.; Tinelli, C., The Satisfiability Modulo Theories Library (SMT-LIB) (2016)
[2] Barrett, C. W.; Sebastiani, R.; Seshia, S. A.; Tinelli, C., Satisfiability modulo theories, (Handbook of Satisfiability (2009)), 825-885
[3] Bradford, R.; Davenport, J. H.; England, M.; McCallum, S.; Wilson, D., Truth table invariant cylindrical algebraic decomposition, J. Symb. Comput., 76, 1-35 (2016) · Zbl 1351.68314
[4] Brown, C. W., Improved projection for cylindrical algebraic decomposition, J. Symb. Comput., 32, 5, 447-465 (2001) · Zbl 0981.68186
[5] Brown, C. W., QEPCAD B: a program for computing with semi-algebraic sets using CADs, ACM SIGSAM Bull., 37, 4, 97-108 (2003) · Zbl 1083.68148
[6] Caviness, B. F.; Johnson, J. R., Quantifier Elimination and Cylindrical Algebraic Decomposition (1998), Springer Science & Business Media · Zbl 0906.03033
[7] Chen, C.; Moreno Maza, M.; Xia, B.; Yang, L., Computing cylindrical algebraic decomposition via triangular decomposition, (Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation. ISSAC ’09 (2009), ACM: ACM New York, NY, USA), 95-102 · Zbl 1237.14068
[8] Collins, G. E., Quantifier elimination for real closed fields by cylindrical algebraic decomposition, (Automata Theory and Formal Languages 2nd GI Conference Kaiserslautern (1975), Springer), 134-183, reprint in Caviness and Johnson (1998)
[9] Collins, G. E., Quantifier elimination by cylindrical algebraic decomposition – twenty years of progress, (Quantifier Elimination and Cylindrical Algebraic Decomposition (1998), Springer), 8-23 · Zbl 0900.03053
[10] Collins, G. E.; Hong, H., Partial cylindrical algebraic decomposition for quantifier elimination, J. Symb. Comput., 12, 3, 299-328 (1991) · Zbl 0754.68063
[11] Collins, G. E.; Loos, R., Real Zeros of Polynomials, 83-94 (1983), Springer Vienna: Springer Vienna Vienna
[12] Corzilius, F.; Kremer, G.; Junges, S.; Schupp, S.; Ábrahám, E., SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving, (International Conference on Theory and Applications of Satisfiability Testing (2015), Springer), 360-368 · Zbl 06512585
[13] Coste, M.; Roy, M., Thom’s lemma, the coding of real algebraic numbers and the computation of the topology of semi-algebraic sets, J. Symb. Comput., 5, 1, 121-129 (1988) · Zbl 0689.14006
[14] Dolzmann, A.; Seidl, A.; Sturm, T., Efficient projection orders for CAD, (International Symposium on Symbolic and algebraic computation (2004), ACM), 111-118 · Zbl 1134.68575
[15] England, M.; Bradford, R.; Davenport, J. H., Improving the use of equational constraints in cylindrical algebraic decomposition, (Proceedings of the 2015 ACM on International Symposium on Symbolic and Algebraic Computation. ISSAC ’15 (2015), ACM: ACM New York, NY, USA), 165-172 · Zbl 1346.68283
[16] England, M.; Bradford, R.; Davenport, J. H.; Wilson, D., Choosing a variable ordering for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition, (Hong, H.; Yap, C., International Congress on Mathematical Software (2014), Springer), 450-457 · Zbl 1350.68294
[17] Hentze, W., Computing Minimal Infeasible Subsets for the Cylindrical Algebraic Decomposition (2017), RWTH Aachen University, available at
[18] Huang, Z.; England, M.; Wilson, D.; Davenport, J. H.; Paulson, L. C.; Bridge, J., Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition, (Intelligent Computer Mathematics (2014), Springer), 92-107 · Zbl 1304.68224
[19] Jaroschek, M.; Dobal, P. F.; Fontaine, P., Adapting real quantifier elimination methods for conflict set computation, (International Symposium on Frontiers of Combining Systems (2015), Springer), 151-166 · Zbl 06688813
[20] Jovanović, D.; De Moura, L., Solving non-linear arithmetic, (International Joint Conference on Automated Reasoning (2012), Springer), 339-354 · Zbl 1358.68257
[21] Kremer, G.; Corzilius, F.; Ábrahám, E., A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic, (Gerdt, V. P.; Koepf, W.; Seiler, W. M.; Vorozhtsov, E. V., Computer Algebra in Scientific Computing (2016), Springer), 315-335 · Zbl 1453.90186
[22] Lazard, D., An improved projection for cylindrical algebraic decomposition, (Algebraic Geometry and Its Applications (1994), Springer), 467-476 · Zbl 0822.68118
[23] Lemaire, F.; Moreno Maza, M.; Xie, Y., The regularchains library in maple, ACM SIGSAM Bull., 39, 3, 96-97 (2005) · Zbl 1114.68628
[24] Loup, U.; Scheibler, K.; Corzilius, F.; Ábrahám, E.; Becker, B., A symbiosis of interval constraint propagation and cylindrical algebraic decomposition, (International Conference on Automated Deduction (2013), Springer), 193-207 · Zbl 1381.68274
[25] Maplesoft, Maple 2017 (2017), Waterloo Maple Inc.: Waterloo Maple Inc. Waterloo, Ontario
[26] McCallum, S., An improved projection operation for cylindrical algebraic decomposition, (Quantifier Elimination and Cylindrical Algebraic Decomposition (1998), Springer), 242-268 · Zbl 0900.68279
[27] McCallum, S., On projection in cad-based quantifier elimination with equational constraint, (Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation (1999), ACM), 145-149
[28] Neuhäuser, T., Quantifier Elimination by Cylindrical Algebraic Decomposition (2018), RWTH Aachen University, Bachelor’s thesis
[29] Viehmann, T.; Kremer, G.; Abraham, E., Comparing different projection operators in the cylindrical algebraic decomposition for SMT solving, (International Workshop on Satisfiability Checking and Symbolic Computation. CEUR-WS 1974 (2017))
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.