zbMATH — the first resource for mathematics

Cylindrical algebraic decomposition with equational constraints. (English) Zbl 1432.68599
Summary: Cylindrical Algebraic Decomposition (CAD) has long been one of the most important algorithms within Symbolic Computation, as a tool to perform quantifier elimination in first order logic over the reals. More recently it is finding prominence in the Satisfiability Checking community, as a tool to identify satisfying solutions of problems in nonlinear real arithmetic. The original algorithm produces decompositions according to the signs of polynomials, when what is usually required is a decomposition according to the truth of a formula containing those polynomials. One approach to achieve that coarser (but hopefully cheaper) decomposition is to reduce the polynomials identified in the CAD to reflect a logical structure which reduces the solution space dimension: the presence of Equational Constraints (ECs). This paper may act as a tutorial for the use of CAD with ECs: we describe all necessary background and the current state of the art. In particular, we present recent work on how McCallum’s theory of reduced projection may be leveraged to make further savings in the lifting phase: both to the polynomials we lift with and the cells lifted over. We give a new complexity analysis to demonstrate that the double exponent in the worst case complexity bound for CAD reduces in line with the number of ECs. We show that the reduction can apply to both the number of polynomials produced and their degree.
Reviewer: Reviewer (Berlin)

MSC:
 68W30 Symbolic computation and algebraic computation 68Q25 Analysis of algorithms and problem complexity
Full Text:
References:
 [1] Abbott, J.; Bigatti, A., What is new in CoCoA?, (Hong, H.; Yap, C., Mathematical Software - ICMS 2014. Mathematical Software - ICMS 2014, Lecture Notes in Computer Science, vol. 8592 (2014), Springer: Springer Heidelberg), 352-358 · Zbl 1437.13002 [2] Abbott, J.; Bigatti, A., New in CoCoA-5.2.0 and CoCoALib-0.99550 for SC-Square, (England, M.; Ganesh, V., Proceedings of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation $$( \mathsf{SC}^2 2017)$$. No. 1974 in CEUR Workshop Proceedings (2017)) [3] Abbott, J.; Bigatti, A.; Palezzato, E., New in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-Square, (Bigatti, A.; Brain, M., Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation $$( \mathsf{SC}^2 2018)$$. No. 2189 in CEUR Workshop Proceedings (2018)), 88-94 [4] Ábrahám, E.; Abbott, J.; Becker, B.; Bigatti, A.; Brain, M.; Buchberger, B.; Cimatti, A.; Davenport, J.; England, M.; Fontaine, P.; Forrest, S.; Griggio, A.; Kroening, D.; Seiler, W.; Sturm, T., $$\mathsf{SC}^2$$: satisfiability checking meets symbolic computation, (Kohlhase, M.; Johansson, M.; Miller, B.; de Moura, L.; Tompa, F., Intelligent Computer Mathematics: Proceedings CICM 2016. Intelligent Computer Mathematics: Proceedings CICM 2016, Lecture Notes in Computer Science, vol. 9791 (2016), Springer International Publishing), 28-43 · Zbl 1344.68198 [5] Barrett, C.; Fontaine, P.; Tinelli, C., The Satisfiability Modulo Theories Library (SMT-LIB) (2016), Online Resource [6] 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, Chapter 26 [7] Basu, S.; Pollack, R.; Roy, M., Algorithms in Real Algebraic Geometry, Algorithms and Computations in Mathematics, vol. 10 (2006), Springer-Verlag · Zbl 1102.14041 [8] Biere, A.; Heule, M.; van Maaren, H.; Walsh, T., Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185 (2009), IOS Press · Zbl 1183.68568 [9] Bradford, R.; Chen, C.; Davenport, J.; England, M.; Moreno Maza, M.; Wilson, D., Truth table invariant cylindrical algebraic decomposition by regular chains, (Gerdt, V.; Koepf, W.; Seiler, W.; Vorozhtsov, E., Computer Algebra in Scientific Computing. Computer Algebra in Scientific Computing, Lecture Notes in Computer Science, vol. 8660 (2014), Springer International Publishing), 44-58 · Zbl 1350.68293 [10] Bradford, R.; Davenport, J.; 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 2017 ACM International Symposium on Symbolic and Algebraic Computation. Proceedings of the 2017 ACM International Symposium on Symbolic and Algebraic Computation, ISSAC ’17 (2017), ACM), 45-52 [11] Bradford, R.; Davenport, J.; England, M.; Errami, H.; Gerdt, V.; Grigoriev, D.; Hoyt, C.; Košta, M.; Radulescu, O.; Sturm, T.; Weber, A., Identifying the parametric occurrence of multiple steady states for some biological networks, J. Symb. Comput., 98, 84-119 (2020) · Zbl 1442.92056 [12] Bradford, R.; Davenport, J.; England, M.; McCallum, S.; Wilson, D., Cylindrical algebraic decompositions for boolean combinations, (Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation. Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation, ISSAC ’13 (2013), ACM), 125-132 · Zbl 1359.68327 [13] Bradford, R.; Davenport, J.; England, M.; McCallum, S.; Wilson, D., Truth table invariant cylindrical algebraic decomposition, J. Symb. Comput., 76, 1-35 (2016) · Zbl 1351.68314 [14] Bradford, R.; Davenport, J.; England, M.; Wilson, D., Optimising problem formulations for cylindrical algebraic decomposition, (Carette, J.; Aspinall, D.; Lange, C.; Sojka, P.; Windsteiger, W., Intelligent Computer Mathematics. Intelligent Computer Mathematics, Lecture Notes in Computer Science, vol. 7961 (2013), Springer: Springer Berlin Heidelberg), 19-34 · Zbl 1390.68775 [15] Brown, C., Improved projection for cylindrical algebraic decomposition, J. Symb. Comput., 32, 5, 447-465 (2001) · Zbl 0981.68186 [16] Brown, C., QEPCAD B: a program for computing with semi-algebraic sets using CADs, SIGSAM Bull., 37, 4, 97-108 (2003) · Zbl 1083.68148 [17] Brown, C., The McCallum Projection, Lifting, and Order-Invariance (2005), U.S. Naval Academy, Computer Science Department, Tech. rep [18] Brown, C., Constructing a single open cell in a cylindrical algebraic decomposition, (Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation. Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation, ISSAC ’13 (2013), ACM), 133-140 · Zbl 1360.68924 [19] Brown, C., Open non-uniform cylindrical algebraic decompositions, (Proceedings of the 2015 International Symposium on Symbolic and Algebraic Computation. Proceedings of the 2015 International Symposium on Symbolic and Algebraic Computation, ISSAC ’15 (2015), ACM), 85-92 · Zbl 1346.68273 [20] Brown, C.; Davenport, J., 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 ’07 (2007), ACM), 54-60 · Zbl 1190.68028 [21] Brown, C.; Kahoui, M. E.; Novotni, D.; Weber, A., Algorithmic methods for investigating equilibria in epidemic modeling, J. Symb. Comput., 41, 1157-1173 (2006) · Zbl 1120.92034 [22] Brown, C.; McCallum, S., On using bi-equational constraints in CAD construction, (Proceedings of the 2005 International Symposium on Symbolic and Algebraic Computation. Proceedings of the 2005 International Symposium on Symbolic and Algebraic Computation, ISSAC ’05 (2005), ACM), 76-83 · Zbl 1360.68925 [23] Buchberger, B., Bruno Buchberger’s PhD thesis (1965): an algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal, J. Symb. Comput., 41, 3-4, 475-511 (2006) · Zbl 1158.01307 [24] Buchberger, B.; Hong, H., Speeding Up Quantifier Elimination by Gröbner Bases (1991), RISC, Johannes Kepler University, Tech. rep., 91-06 [25] Busé, L.; Mourrain, B., Explicit factors of some iterated resultants and discriminants, Math. Comput., 78, 345-386 (2009) · Zbl 1200.13042 [26] Caviness, B.; Johnson, J., Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts & Monographs in Symbolic Computation (1998), Springer-Verlag [27] Charalampakis, A.; Chatzigiannelis, I., Analytical solutions for the minimum weight design of trusses by cylindrical algebraic decomposition, Arch. Appl. Mech., 88, 1, 39-49 (2018) [28] 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. Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation, ISSAC ’09 (2009), ACM), 95-102 · Zbl 1237.14068 [29] Collins, G., Quantifier elimination for real closed fields by cylindrical algebraic decomposition, (Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages (1975), Springer-Verlag), 134-183, (reprinted in the collection Caviness and Johnson (1998)) [30] Collins, G., Quantifier elimination by cylindrical algebraic decomposition - 20 years of progress, (Caviness, B.; Johnson, J., Quantifier Elimination and Cylindrical Algebraic Decomposition. Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts & Monographs in Symbolic Computation (1998), Springer-Verlag), 8-23 · Zbl 0900.03053 [31] Collins, G.; Hong, H., Partial cylindrical algebraic decomposition for quantifier elimination, J. Symb. Comput., 12, 299-328 (1991) · Zbl 0754.68063 [32] Cowen-Rivers, A.; England, M., Towards incremental cylindrical algebraic decomposition in Maple, (Bigatti, A.; Brain, M., Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation $$( \mathsf{SC}^2 2018)$$. No. 2189 in CEUR Workshop Proceedings (2018)), 3-18 [33] Davenport, J.; Bradford, R.; England, M.; Wilson, D., Program verification in the presence of complex numbers, functions with branch cuts etc, (14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC ’12 (2012), IEEE), 83-88 [34] Davenport, J.; Heintz, J., Real quantifier elimination is doubly exponential, J. Symb. Comput., 5, 1-2, 29-35 (1988) · Zbl 0663.03015 [35] Dolzmann, A.; Seidl, A.; Sturm, T., Efficient projection orders for CAD, (Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation. Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation, ISSAC ’04 (2004), ACM), 111-118 · Zbl 1134.68575 [36] England, M., Machine learning for mathematical software, (Davenport, J.; Kauers, M.; Labahn, G.; Urban, J., Mathematical Software - Proc. ICMS 2018. Mathematical Software - Proc. ICMS 2018, Lecture Notes in Computer Science, vol. 10931 (2018), Springer International Publishing), 165-174 · Zbl 1395.68231 [37] England, M.; Bradford, R.; Chen, C.; Davenport, J.; Moreno Maza, M.; Wilson, D., Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition, (Watt, S.; Davenport, J.; Sexton, A.; Sojka, P.; Urban, J., Intelligent Computer Mathematics. Intelligent Computer Mathematics, Lecture Notes in Artificial Intelligence, vol. 8543 (2014), Springer International), 45-60 · Zbl 1304.68223 [38] England, M.; Bradford, R.; Davenport, J., Improving the use of equational constraints in cylindrical algebraic decomposition, (Proceedings of the 2015 International Symposium on Symbolic and Algebraic Computation. Proceedings of the 2015 International Symposium on Symbolic and Algebraic Computation, ISSAC ’15 (2015), ACM), 165-172 · Zbl 1346.68283 [39] England, M.; Davenport, J., The complexity of cylindrical algebraic decomposition with respect to polynomial degree, (Gerdt, V.; Koepf, W.; Werner, W.; Vorozhtsov, E., Computer Algebra in Scientific Computing: 18th International Workshop, CASC 2016. Computer Algebra in Scientific Computing: 18th International Workshop, CASC 2016, Lecture Notes in Computer Science, vol. 9890 (2016), Springer International Publishing), 172-192 · Zbl 1453.13079 [40] England, M.; Errami, H.; Grigoriev, D.; Radulescu, O.; Sturm, T.; Weber, A., Symbolic versus numerical computation and visualization of parameter regions for multistationarity of biological networks, (Gerdt, V.; Koepf, W.; Seiler, W.; Vorozhtsov, E., Computer Algebra in Scientific Computing (CASC). Computer Algebra in Scientific Computing (CASC), Lecture Notes in Computer Science, vol. 10490 (2017), Springer International Publishing), 93-108 · Zbl 1455.92058 [41] England, M.; Wilson, D.; Bradford, R.; Davenport, J., Using the Regular Chains Library to build cylindrical algebraic decompositions by projecting and lifting, (Hong, H.; Yap, C., Mathematical Software - ICMS 2014. Mathematical Software - ICMS 2014, Lecture Notes in Computer Science, vol. 8592 (2014), Springer: Springer Heidelberg), 458-465 · Zbl 1437.14008 [42] Erascu, M.; Hong, H., Real quantifier elimination for the synthesis of optimal numerical algorithms (Case study: Square root computation), J. Symb. Comput., 75, 110-126 (2016) · Zbl 1335.68300 [43] Faugère, J., A new efficient algorithm for computing Gröbner bases without reduction to zero (F5), (Proceedings of the 2002 International Symposium on Symbolic and Algebraic Computation. Proceedings of the 2002 International Symposium on Symbolic and Algebraic Computation, ISSAC ’02 (2002), ACM), 75-83 · Zbl 1072.68664 [44] Fotiou, I.; Parrilo, P.; Morari, M., Nonlinear parametric optimization using cylindrical algebraic decomposition, (Decision and Control, 2005 European Control Conference. Decision and Control, 2005 European Control Conference, CDC-ECC ’05 (2005)), 3735-3740 [45] Fukasaku, R.; Iwane, H.; Sato, Y., Real quantifier elimination by computation of comprehensive Gröbner systems, (Proceedings of the 2015 International Symposium on Symbolic and Algebraic Computation. Proceedings of the 2015 International Symposium on Symbolic and Algebraic Computation, ISSAC ’15 (2015), ACM), 173-180 · Zbl 1345.68282 [46] Haehn, R.; Kremer, G.; Ábrahám, E., Evaluation of equational constraints for CAD in SMT solving, (Bigatti, A.; Brain, M., Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation $$( \mathsf{SC}^2 2018)$$. No. 2189 in CEUR Workshop Proceedings (2018)), 19-32 [47] Han, J.; Dai, L.; Xia, B., Constructing fewer open cells by gcd computation in CAD projection, (Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation. Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation, ISSAC ’14 (2014), ACM), 240-247 · Zbl 1325.68286 [48] 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 ’90 (1990), ACM), 261-264 [49] Huang, Z.; England, M.; Davenport, J.; Paulson, L., Using machine learning to decide when to precondition cylindrical algebraic decomposition with Groebner bases, (18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC ’16) (2016), IEEE), 45-52 [50] Huang, Z.; England, M.; Wilson, D.; Davenport, J.; Paulson, L.; Bridge, J., Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition, (Watt, S.; Davenport, J.; Sexton, A.; Sojka, P.; Urban, J., Intelligent Computer Mathematics. Intelligent Computer Mathematics, Lecture Notes in Artificial Intelligence, vol. 8543 (2014), Springer International), 92-107 · Zbl 1304.68224 [51] Huang, Z.; England, M.; Wilson, D.; Bridge, J.; Davenport, J.; Paulson, L., Using machine learning to improve cylindrical algebraic decomposition, Math. Comput. Sci. (2019), Volume to be assigned, 28 pages · Zbl 07137257 [52] Iwane, H.; Yanami, H.; Anai, H.; Yokoyama, K., An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for quantifier elimination, (Proceedings of the 2009 Conference on Symbolic Numeric Computation. Proceedings of the 2009 Conference on Symbolic Numeric Computation, SNC ’09 (2009)), 55-64 · Zbl 1356.68282 [53] Jouanolou, J., Le formalisme du résultant, Adv. Math., 90, 2, 117-263 (1991) · Zbl 0747.13007 [54] Jovanovic, D.; de Moura, L., Solving non-linear arithmetic, (Gramlich, B.; Miller, D.; Sattler, U., Automated Reasoning: 6th International Joint Conference (IJCAR). Automated Reasoning: 6th International Joint Conference (IJCAR), Lecture Notes in Computer Science, vol. 7364 (2012), Springer), 339-354 · Zbl 1358.68257 [55] Kremer, G.; Ábrahám, E., Fully Incremental CAD, J. Symb. Comput. (2019), In press [56] Kroening, D.; Strichman, O., Decision Procedures: An Algorithmic Point of View (2013), Springer: Springer New York [57] 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 [58] Lazard, D.; McCallum, S., Iterated discriminants, J. Symb. Comput., 44, 9, 1176-1193 (2009) · Zbl 1206.13030 [59] Loup, U.; Scheibler, K.; Corzilius, F.; Ábrahám, E.; Becker, B., A symbiosis of interval constraint propagation and cylindrical algebraic decomposition, (Bonacina, M., Automated Deduction (CADE-24). Automated Deduction (CADE-24), Lecture Notes in Computer Science, vol. 7898 (2013), Springer: Springer Berlin Heidelberg), 193-207 · Zbl 1381.68274 [60] Mayr, E.; Meyer, A., The complexity of the word problems for commutative semigroups and polynomial ideals, Adv. Math., 46, 3, 305-329 (1982) · Zbl 0506.03007 [61] Mayr, E.; Ritscher, S., Dimension-dependent bounds for Gröbner bases of polynomial ideals, J. Symb. Comput., 49, 78-94 (2013) · Zbl 1258.13032 [62] McCallum, S., An Improved Projection Operation for Cylindrical Algebraic Decomposition (1985), University of Wisconsin-Madison, PhD Thesis (Computer Sciences Technical Report 578) [63] 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 [64] McCallum, S., Factors of iterated resultants and discriminants, J. Symb. Comput., 27, 4, 367-385 (1999) · Zbl 0927.12005 [65] 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 ’99 (1999), ACM), 145-149 [66] McCallum, S., On propagation of equational constraints in CAD-based quantifier elimination, (Proceedings of the 2001 International Symposium on Symbolic and Algebraic Computation. Proceedings of the 2001 International Symposium on Symbolic and Algebraic Computation, ISSAC ’01 (2001), ACM), 223-231 · Zbl 1356.68287 [67] McCallum, S.; Brown, C., On delineability of varieties in CAD-based quantifier elimination with two equational constraints, (Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation. Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation, ISSAC ’09 (2009), ACM), 71-78 · Zbl 1237.14067 [68] McCallum, S.; Hong, H., On using Lazard’s projection in CAD construction, J. Symb. Comput., 72, 65-81 (2016) · Zbl 1325.13026 [69] 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 [70] Mulligan, C.; Bradford, R.; Davenport, J.; England, M.; Tonks, Z., Non-linear real arithmetic benchmarks derived from automated reasoning in economics, (Bigatti, A.; Brain, M., Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation $$( \mathsf{SC}^2 2018)$$. No. 2189 in CEUR Workshop Proceedings (2018)), 48-60 [71] Mulligan, C.; Davenport, J.; England, M., TheoryGuru: a Mathematica package to apply quantifier elimination technology to economics, (Davenport, J.; Kauers, M.; Labahn, G.; Urban, J., Mathematical Software - Proc. ICMS 2018. Mathematical Software - Proc. ICMS 2018, Lecture Notes in Computer Science, vol. 10931 (2018), Springer International Publishing), 369-378 · Zbl 1395.68350 [72] Paulson, L., Metitarski: past and future, (Beringer, L.; Felty, A., Interactive Theorem Proving. Interactive Theorem Proving, Lecture Notes in Computer Science., vol. 7406 (2012), Springer), 1-10 · Zbl 1360.68765 [73] Schwartz, J.; Sharir, M., On the “Piano-Movers” problem: II. General techniques for computing topological properties of real algebraic manifolds, Adv. Appl. Math., 4, 298-351 (1983) · Zbl 0554.51008 [74] Seidl, A., Cylindrical Decomposition Under Application-Oriented Paradigms (2006), Universität Passau, Fakultät für Informatik und Mathematik, Ph.D. thesis [75] Strzeboński, A., Cylindrical algebraic decomposition using validated numerics, J. Symb. Comput., 41, 9, 1021-1038 (2006) · Zbl 1124.68123 [76] Strzeboński, A., Cylindrical algebraic decomposition using local projections, J. Symb. Comput., 76, 36-64 (2016) · Zbl 1350.14042 [77] Viehmann, T.; Kremer, G.; Ábráham, E., Comparing different projection operators in the cylindrical algebraic decomposition for smt solving, (England, M.; Ganesh, V., Proceedings of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation $$( \mathsf{SC}^2 2017)$$. No. 1974 in CEUR Workshop Proceedings (2017)) [78] Wada, Y.; Matsuzaki, T.; Terui, A.; Arai, N., An automated deduction and its implementation for solving problem of sequence at university entrance examination, (Greuel, G.-M.; Koch, T.; Paule, P.; Sommese, A., Mathematical Software - Proceedings of ICMS 2016. Mathematical Software - Proceedings of ICMS 2016, Lecture Notes in Computer Science, vol. 9725 (2016), Springer International Publishing), 82-89 · Zbl 06630646 [79] Wilson, D.; Bradford, R.; Davenport, J., Speeding up cylindrical algebraic decomposition by Gröbner bases, (Jeuring, J.; Campbell, J.; Carette, J.; Reis, G.; Sojka, P.; Wenzel, M.; Sorge, V., Intelligent Computer Mathematics. Intelligent Computer Mathematics, Lecture Notes in Computer Science, vol. 7362 (2012), Springer), 280-294 · Zbl 1360.68959 [80] Wilson, D.; Bradford, R.; Davenport, J.; England, M., Cylindrical algebraic sub-decompositions, Math. Comput. Sci., 8, 2, 263-288 (2012) · Zbl 1309.68232 [81] Wilson, D.; England, M.; Davenport, J.; Bradford, R., Using the distribution of cells by dimension in a cylindrical algebraic decomposition, (16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC ’14 (2014), IEEE), 53-60
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.