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