Cylindrical algebraic decomposition using validated numerics. (English) Zbl 1124.68123

Summary: We present a version of the Cylindrical Algebraic Decomposition (CAD) algorithm which uses interval sample points in the lifting phase, whenever the results can be validated. This gives substantial time savings by avoiding computations with exact algebraic numbers. We use bounds based on Rouche’s theorem combined with information collected during the projection phase and during construction of the current cell to validate the singularity structure of roots. We compare empirically our implementation of this variant of CAD with implementations of CAD using exact algebraic sample points (our and QEPCAD) and with our implementation of CAD using interval sample points with validation based solely on interval data.


68W30 Symbolic computation and algebraic computation
14P99 Real algebraic and real-analytic geometry


QEPCAD; Mathematica
Full Text: DOI


[1] Anai, H., Yokoyama, K., 2005. CAD via numerical computation with validated symbolic reconstruction. In: Dolzmann A., Seidl A., Sturm T. (Eds.), Proceedings of A3L 2005, A3L
[2] Brown, C.W., Improved projection for cylindrical algebraic decomposition, J. symbolic comput., 32, 447-465, (2001) · Zbl 0981.68186
[3] Brown, C.W., An overview of QEPCAD B: A tool for real quantifier elimination and formula simplification, J. jssac, 10, 13-22, (2003)
[4] Caviness, B.; Johnson, J., Quantifier elimination and cylindrical algebraic decomposition, (1998), Springer-Verlag Wien, New York
[5] Collins, G.E., Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition, Lect. notes comput. sci., 33, 134-183, (1975)
[6] Collins, G.E., Quantifier elimination by cylindrical algebraic decomposition — twenty years of progress, (), 8-23 · Zbl 0900.03053
[7] Collins, G.E.; Hong, H., Partial cylindrical algebraic decomposition for quantifier elimination, J. symbolic comput., 12, 299-328, (1991) · Zbl 0754.68063
[8] Collins, G.E.; Johnson, J.R.; Krandick, W., Interval arithmetic in cylindrical algebraic decomposition, J. symbolic comput., 34, 145-157, (2002) · Zbl 1007.68210
[9] Dorato, P.; Yang, W.; Abdallah, C., Robust multi-objective feedback design by quantifier elimination, J. symbolic comput., 24, 153-160, (1997) · Zbl 0938.93534
[10] Hong, H., 1990. An improvement of the projection operator in cylindrical algebraic decomposition. In: Proceedings of the International Symposium on Symbolic and Algebraic Computation. pp. 261-264
[11] Hong, H., 1993. Efficient method for analyzing topology of plane real algebraic curves. In: Proceedings of IMACS-SC 93, Lille, France
[12] Hong, H.; Liska, R.; Steinberg, S., Testing stability by quantifier elimination, J. symbolic comput., 24, 161-188, (1997) · Zbl 0886.65087
[13] Jenkins, M.A.G., 1969. Three-stage variable-shift iterations for the solution of polynomial equations with a posteriori error bounds for the zeros. Ph.D. Dissertation. Stanford University
[14] Jirstrand, M., Nonlinear control system design by quantifier elimination, J. symbolic comput., 24, 137-152, (1997) · Zbl 0882.93022
[15] Keiper, J.B., Withoff, D., 1992. Numerical Computation in Mathematica, Course Notes. In: Mathematica Conference
[16] Łojasiewicz, S., 1964. Ensembles semi-analytiques. I.H.E.S., Bures sur Yvette (preprint) · Zbl 0241.32005
[17] Loos, R.; Weispfenning, V., Applying linear quantifier elimination, The comput. J., 36, 450-461, (1993) · Zbl 0787.03021
[18] McCallum, S., An improved projection for cylindrical algebraic decomposition of three dimensional space, J. symbolic comput., 5, 141-161, (1988) · Zbl 0648.68054
[19] McCallum, S., An improved projection for cylindrical algebraic decomposition, (), 242-268 · Zbl 0900.68279
[20] McCallum, S., On projection in CAD-based quantifier elimination with equational constraint, (), 145-149
[21] McCallum, S., On propagation of equational constraints in CAD-based quantifier elimination, (), 223-230 · Zbl 1356.68287
[22] Strzeboński, A., An algorithm for systems of strong polynomial inequalities, The math. J., 4, 4, 74-77, (1994)
[23] Strzeboński, A., Algebraic numbers in Mathematica 3.0, The math. J., 6, 4, 74-80, (1996)
[24] Strzeboński, A., Computing in the field of complex algebraic numbers, J. symbolic comput., 24, 647-656, (1997) · Zbl 0910.65029
[25] Strzeboński, A., A real polynomial decision algorithm using arbitrary-precision floating point arithmetic, Reliab. comput., 5, 3, 337-346, (1999) · Zbl 1097.65526
[26] Strzeboński, A., Solving systems of strict polynomial inequalities, J. symbolic comput., 29, 471-480, (2000) · Zbl 0962.68183
[27] Strzeboński, A., Solving algebraic inequalities, The math. J., 7, 4, 525-541, (2000)
[28] Tarski, A., A decision method for elementary algebra and geometry, (1951), University of California Press Berkeley · Zbl 0044.25102
[29] Wolfram, S., The Mathematica book, 5th ed, (2003), Wolfram Media
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.