Abstract
In 1994 Daniel Lazard proposed an improved method for constructing a cylindrical algebraic decomposition (CAD) from a set of polynomials, which recent work has, finally, fully validated. Lazard’s method works for any set of input polynomials, but is less efficient than the method of Brown (2001) which, however, fails for input sets that are not “well-oriented”. The present work improves Lazard’s method so that it is as efficient for well-oriented input as Brown’s method, while retaining its infallibility. Justifying these improvements requires novel and non-trivial mathematics.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
The system \(a c - 1 = 0 \wedge a c + b^2 = 0\) is easily shown to be unsatisfiable by a number of means, including simply substituting for linearly occurring variables.
References
Arnon, D.S., Collins, G.E., McCallum, S.: Cylindrical algebraic decomposition I: the basic algorithm. SIAM J. Comput. 13, 865–877 (1984)
Bradford, R., Davenport, J.H., England, M., McCallum, S., Wilson, D.: Truth table invariant cylindrical algebraic decomposition. J. Symbolic Comput. 76, 1–35 (2016)
Brown, C.W.: Improved projection for cylindrical algebraic decomposition. J. Symbolic Comput. 32, 447–465 (2001)
Brown, C. W., Davenport, J.H.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: ISSAC 2007: Proceedings of the 2007 International Symposium on Symbolic and Algebraic Computation, pp. 54–60. ACM, New York (2007)
Caviness, B., Johnson, J.R. (Eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation. Springer, Wien (1998). https://doi.org/10.1007/978-3-7091-9459-1
Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975). https://doi.org/10.1007/3-540-07407-4_17
Collins, G.E.: Quantifier elimination by cylindrical algebraic decomposition - twenty years of progress. In [5]
Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symbolic Comput. 12, 299–328 (1991)
Cowen-Rivers, A.I., England, M.: Towards incremental cylindrical algebraic decomposition. In: Bigatti, A., Brain, M. (Eds.) Proceedings of 3rd Workshop on Satisfiability Checking and Symbolic Computation 2018. No. 2189 in CEUR Workshop Proceedings, pp. 3–18. http://ceur-ws.org/Vol-2189/
Hong, H.: An improvement of the projection operator in cylindrical algebraic decomposition. In: ISSAC 1990: Proceedings of the 1990 International Symposium on Symbolic and Algebraic Computation, pp. 261–264. ACM Press, New York (1990). Reprinted in [5]
Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 339–354. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31365-3_27
Kremer, G., Abraham, E.: Fully incremental cylindrical algebraic decomposition. J. Symbolic Comput. 100, 11–37 (2020)
Lazard, D.: An improved projection for cylindrical algebraic decomposition. Algebraic Geometry and its Applications. Springer, New York (1994). https://doi.org/10.1007/978-1-4612-2628-4_29
McCallum, S.: An improved projection operation for cylindrical algebraic decomposition of three-dimensional space. J. Symbolic Comput. 5, 141–161 (1988)
McCallum, S.: An improved projection operation for cylindrical algebraic decomposition. In [5]
McCallum, S.: On projection in CAD-based quantifier elimination with equational constraint. In: Dooley, S. (ed.) Proceedings of International Symposium on Symbolic and Algebraic Computation ISSAC 1999, pp. 145–149. ACM Press, New York (1999)
McCallum, S., Hong, H.: On using Lazard’s projection in CAD construction. J. Symbolic Comput. 72, 65–81 (2016)
McCallum, S., Parusiński, A., Paunescu, L.: Validity proof of Lazard’s method for CAD construction. J. Symbolic Comput. 92, 52–69 (2019)
Strzebonski, A.: Solving systems of strict polynomial inequalities. J. Symbolic Comput. 29, 471–480 (2000)
Strzebonski, A.: Divide-and-conquer computation of cylindrical algebraic decomposition. arXiv:1402.0622 (2014)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Brown, C.W., McCallum, S. (2020). Enhancements to Lazard’s Method for Cylindrical Algebraic Decomposition. In: Boulier, F., England, M., Sadykov, T.M., Vorozhtsov, E.V. (eds) Computer Algebra in Scientific Computing. CASC 2020. Lecture Notes in Computer Science(), vol 12291. Springer, Cham. https://doi.org/10.1007/978-3-030-60026-6_8
Download citation
DOI: https://doi.org/10.1007/978-3-030-60026-6_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-60025-9
Online ISBN: 978-3-030-60026-6
eBook Packages: Computer ScienceComputer Science (R0)