Define a cell in as an open interval or a point. A cell in then has one of two forms,
(1)
or
(2)
where , is a cell in , and are either (1) continuous functions on such that for some polynomials and , and , or (2) , and for all .
A cylindrical algebraic decomposition of is a representation of as a finite union of disjoint cells. Let be finite set of polynomials in variables. A cylindrical algebraic decomposition of is said to be -invariant if each of the polynomials from has a constant sign on each cell of the decomposition.
The cylindrical algebraic decomposition (CAD) algorithm, given a finite set
of polynomials in variables, computes an -invariant cylindrical algebraic decomposition of . Given a logical combination of polynomial equations and
inequalities in real unknowns, one can use the
CAD algorithm to find a cylindrical algebraic decomposition of its solution set.
For example, the decomposition of
(3)
is given by
(4)
The command CylindricalDecomposition[ineqs, x1,
x2, ...] performs cylindrical algebraic decompositions in the Wolfram
Language. Although the process is algorithmic, it becomes computationally infeasible
for complicated inequalities.
Brown, C. W. "Simple CAD Construction and Its Applications." J. Symbolic Comput.31, 521-547, 2001.Caviness,
B. F. and Johnson, J. R. (Eds.). Quantifier
Elimination and Cylindrical Algebraic Decomposition. New York: Springer-Verlag,
1998.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.Collins, G. E.
"Quantifier Elimination by Cylindrical Algebraic Decomposition--Twenty Years
of Progress." In Quantifier
Elimination and Cylindrical Algebraic Decomposition (Ed. B. F. Caviness
and J. R. Johnson). New York: Springer-Verlag, pp. 8-23, 1998.Collins,
G. E. and Hong, H. "Partial Cylindrical Algebraic Decomposition for Quantifier
Elimination." J. Symb. Comput.12, 299-328, 1991.Dolzmann,
A. and Sturm, T. "Simplification of Quantifier-Free Formulae Over Ordered Fields."
J. Symb. Comput.24, 209-231, 1997.Faugere, J. C.;
Gianni, P.; Lazard, D.; and Mora, T. "Efficient Computation of Zero-Dimensional
Groebner Bases by Change of Ordering." J. Symb. Comput.16, 329-344,
1993.Hong, H. "An Improvement of the Projection Operator in Cylindrical
Algebraic Decomposition." In ISSAC
'90: Proceedings of the International Symposium on Symbolic and Algebraic Computation,
August 20-24, 1990, Tokyo, Japan (Ed. S. Watanabe and M. Nagata).
New York: ACM Press, pp. 261-264, 1990.Loos, R. and Weispfenning,
V. "Applying Lattice Quantifier Elimination." Comput. J.36,
450-461, 1993.McCallum, S. "Solving Polynomial Strict Inequalities
Using Cylindrical Algebraic Decomposition." Comput. J.36, 432-438,
1993.McCallum, S. "An Improved Projection for Cylindrical Algebraic
Decomposition of Three Dimensional Space." J. Symb. Comput.5,
141-161, 1988.McCallum, S. "An Improved Projection for Cylindrical
Algebraic Decomposition." In Quantifier
Elimination and Cylindrical Algebraic Decomposition (Ed. B. F. Caviness
and J. R. Johnson). New York: Springer-Verlag, pp. 242-268, 1998.McCallum,
S. and Collins, G. E. "Local Box Adjacency Algorithms for Cylindrical Algebraic
Decompositions." J. Symb. Comput.33, 321-342, 2002.Strzebonski,
A. "An Algorithm for Systems of Strong Polynomial Inequalities." Mathematica
J.4, 74-77, 1994.Strzebonski, A. "A Real Polynomial
Decision Algorithm Using Arbitrary-Precision Floating Point Arithmetic." Reliable
Comput.5, 337-346, 1999.Strzebonski, A. "Solving Algebraic
Inequalities." Mathematica J.7, 525-541, 2000.Trott,
M. "Polynomials in Inequalities." §1.2.3 in The
Mathematica GuideBook for Symbolics. New York: Springer-Verlag, pp. 50-78,
2006. http://www.mathematicaguidebooks.org/.
as an open interval or a point. A cell in 
then has one of two forms,
, 
is a cell in 
, 
and 
are either (1) continuous functions on 
such that for some polynomials 
and 
, 
and 
, or (2) 
, and 
for all 
.
is a representation of 
as a finite union of disjoint cells. Let 
be finite set of polynomials in 
variables. A cylindrical algebraic decomposition of 
is said to be 
-invariant if each of the polynomials from 
has a constant sign on each cell of the decomposition.
of polynomials in 
variables, computes an 
-invariant cylindrical algebraic decomposition of 
. Given a logical combination of polynomial equations and
inequalities in 
real unknowns, one can use the
CAD algorithm to find a cylindrical algebraic decomposition of its solution set.
For example, the decomposition of
x1,
x2, ...
] performs cylindrical algebraic decompositions in the Wolfram
Language. Although the process is algorithmic, it becomes computationally infeasible
for complicated inequalities.
