** Next:** Solution formula construction
** Up:** An overview of quantifier
** Previous:** Projection

##

Stack construction

The end product of the stack construction phase is an explicit
representation of the CAD of -space that is implicitly defined by
, along with the truth value of in each
cell of the decomposition.
Each cell in the CAD will be represented by a point from the cell, a
* sample point*. A CAD of -space is constructed from a CAD of
-space by constructing a stack over each cell in the CAD
of -space. Suppose is a cell in the CAD of -space,
and let
be its sample point.
The children of will inherit its sample point, meaning that the
first coordinates of their sample points will be . The
children of are exactly the maximal connected regions in
in which the elements of have invariant sign. Since
we are restricting ourselves to points in
, finding a
sample point for each of the children of is reduced to finding a
point from each of the maximal connected regions of in which the
elements of
have
invariant sign. This can be done by real root isolation and refinement.

The stack construction phase begins with cell , which corresponds
to . Formally, its sample point is an empty vector. Sample
points for 's children are constructed by real root isolation
to get representations for cells in the CAD of 1-space. Stacks are
raised over cells in the CAD of 1-space, then over the cells in
2-space, etc. until the full CAD of -space is constructed.
The whole is kept in a tree structure rooted at the representation of
, with edges defined by the parent-child relation.

The truth of , the quantifier-free part of , in each cell of
the decomposition of -space is easy to determine.
Cells are regions in which the polynomials
appearing in are sign-invariant, so the truth value of at
a cell's sample point is the same as at every other point in the
cell. The truth of at a cell's sample point (and thus in the
whole cell) can be determined by simply substituting the sample point
into the polynomials in .

Once truth values for are determined in the cells of the CAD of
-space,
truth values for in the cells of the induced CAD of -space can
be determined.
Let be a cell in the CAD of -space, .
is satisfied in
provided that

**
**
- and
is
satisfied in each of 's children, or
**
**
- and
is
satisfied in at least one of 's children.

This gives an easy recursive procedure for determining truth values
for in the cells of the CAD of -space.

** Next:** Solution formula construction
** Up:** An overview of quantifier
** Previous:** Projection
*Christopher W Brown*

*2001-07-10*