To explain the cylindrical algebraic decomposition method, we first
perform a semi-algebraic decomposition of
, which is the final
step in the projection sequence. Once this is explained, then the
multi-dimensional case follows more easily.
Let be a set of univariate polynomials,
which are used to define some semi-algebraic set in
polynomials in could come directly from a quantifier-free
formula (which could even appear inside of a Tarski
sentence, as in (6.9)).
Define a single polynomial as
. Suppose that
has distinct, real roots, which are sorted in increasing
The one-dimensional semi-algebraic decomposition is given by the
following sequence of alternating -cells and 0-cells:
Any semi-algebraic set that can be expressed using the polynomials in
can also be expressed as the union of some of the 0-cells
and -cells given in (6.20). This can also be
considered as a singular complex (it can even be considered as a
simplicial complex, but this does not extend to higher dimensions).
Sample points can be generated for each of the cells as follows. For
the unbounded cells
valid samples are
For each finite -cell,
, the midpoint
produces a sample point. For each
, the only choice is to use
as the sample point.
Two parabolas are used to define the
semi-algebraic set .
A semi-algebraic decomposition for
the polynomials in Figure 6.31.
shows a semi-algebraic subset of
is defined by two polynomials,
. Consider the quantifier-free
The semi-algebraic decomposition into five
-cells and four
-cells is shown in Figure 6.32
. Each cell is
sign invariant. The sample points for the
, respectively. The sample points for the
-cells are 0
A decision problem can be nicely solved using the decomposition.
Suppose a Tarski sentence that uses the polynomials in has been
given. Here is one possibility:
The sample points alone are sufficient to determine whether
is attempted, it is discovered that
. The quantifier-elimination problem cannot yet be
considered because more dimensions are needed.
Steven M LaValle