zbMATH — the first resource for mathematics

Improved projection for cylindrical algebraic decomposition. (English) Zbl 0981.68186
Summary: McCallum’s projection operator for Cylindrical Algebraic Decomposition (CAD) represented a huge step forward for the practical utility of the CAD algorithm. This paper presents a simple theorem showing that the mathematics in McCallum’s paper actually point to a better projection operator than he proposes – a reduced McCallum projection. The reduced projection has the potential to not simply speed up CAD computation for problems that are currently solvable in practice, but actually increase the scope of problems that can realistically be attacked via CADs. Additionally, the same methods are used to show that McCallum’s projection can be reduced still further when CAD is applied to certain types of commonly occurring quantifier elimination problems.

68W30 Symbolic computation and algebraic computation
03C10 Quantifier elimination, model completeness, and related topics
Full Text: DOI
[1] Arnon, D.S.; Collins, G.E.; McCallum, S., Cylindrical algebraic decomposition I: the basic algorithm, SIAM J. comput., 13, 865-877, (1984) · Zbl 0562.14001
[2] P. Aubry, F. Rouillier, M. Safey El Din
[3] Brown, C.W., Simplification of truth-invariant cylindrical algebraic decompositions, Proceedings of international symposium on symbolic and algebraic computation, (1998), p. 295-301 · Zbl 0918.68058
[4] Caviness, B.F.; Johnson, J.R.eds., Quantifier elimination and cylindrical algebraic decomposition, texts and monographs in symbolic computation, (1998), Springer Vienna
[5] Collins, G.E., Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition, (1975 Reprinted in Caviness and Johnson (1998).), Springer Berlin, p. 134-183
[6] Collins, G.E., Quantifier elimination by cylindrical algebraic decomposition—20 years of progress, () · Zbl 0900.03053
[7] Collins, G.E.; Hong, H., Partial cylindrical algebraic decomposition for quantifier elimination, J. symb. comput., 12, 299-328, (1991) · Zbl 0754.68063
[8] Gelfand, I.M.; Kapranov, M.M.; Zelevinsky, A.V., Discriminants, resultants, and multidimensional determinants, (1994), Springer Berlin · Zbl 0827.14036
[9] Grigor’ev, D.Yu., The complexity of deciding Tarski algebra, J. symb. comput., 5, 65-108, (1988) · Zbl 0689.03021
[10] Hong, H., Simple solution formula construction in cylindrical algebraic decomposition based quantifier elimination, Proceedings of international symposium on symbolic and algebraic computation, (1992), p. 177-188 · Zbl 0919.03029
[11] Hong, H.; Liska, R.; Steinberg, S., Testing stability by quantifier elimination, J. symb. comput., 24, 161-187, (1997 Special Issue on Applications of Quantifier Elimination.)
[12] Lazard, D., Quantifier elimination: optimal solution for two classical examples, J. symb. comput., 5, 261-266, (1988) · Zbl 0647.03023
[13] Lazard, D., An improved projection for cylindrical algebraic decomposition, (), 467-476 · Zbl 0822.68118
[14] S. McCallum, 1984
[15] McCallum, S., An improved projection operation for cylindrical algebraic decomposition of three-dimensional space, J. symb. comput., 5, 141-161, (1988) · Zbl 0648.68054
[16] McCallum, S., An improved projection operator for cylindrical algebraic decomposition, () · Zbl 0900.68279
[17] McCallum, S., On projection in CAD-based quantifier elimination with equational constraint, (), 145-149
[18] Renegar, J., On the computational complexity and geometry of the first-order theory of the reals, parts I-III, J. symb. comput., 13, 255-352, (1992) · Zbl 0798.68073
[19] Rouillier, F., Solving zero-dimensional systems through the rational univariate representation, J. appl. algebra eng., commun. comput., 9, 433-461, (1999) · Zbl 0932.12008
[20] Strzebonski, A., Solving systems of strict polynomial inequalities, J. symb. comput., 29, 471-480, (2000) · Zbl 0962.68183
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.