Stack construction

The end product of the stack construction phase is an explicit representation of the CAD of $k$-space that is implicitly defined by $P_1 \cup \cdots \cup P_k$, along with the truth value of $F$ 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 $i$-space is constructed from a CAD of $(i-1)$-space by constructing a stack over each cell in the CAD of $(i-1)$-space. Suppose $c'$ is a cell in the CAD of $(i-1)$-space, and let $\alpha = (\alpha_1,\ldots , \alpha_{i-1})$ be its sample point. The children of $c'$ will inherit its sample point, meaning that the first $i-1$ coordinates of their sample points will be $\alpha$. The children of $c'$ are exactly the maximal connected regions in $c' \times \mathbb {R}$ in which the elements of $P_i$ have invariant sign. Since we are restricting ourselves to points in $\alpha \times \mathbb {R}$, finding a sample point for each of the children of $c'$ is reduced to finding a point from each of the maximal connected regions of $\mathbb {R}^1$ in which the elements of $\{p(\alpha_1,\ldots , \alpha_{i-1},x) \vert p \in P_i\}$ have invariant sign. This can be done by real root isolation and refinement.

The stack construction phase begins with cell $c_0$, which corresponds to $\mathbb {R}^0$. Formally, its sample point is an empty vector. Sample points for $c_0$'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 $r$-space is constructed. The whole is kept in a tree structure rooted at the representation of $c_0$, with edges defined by the parent-child relation.

The truth of $F'$, the quantifier-free part of $F$, in each cell of the decomposition of $r$-space is easy to determine. Cells are regions in which the polynomials appearing in $F'$ are sign-invariant, so the truth value of $F'$ at a cell's sample point is the same as at every other point in the cell. The truth of $F'$ 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 $F'$.

Once truth values for $F'$ are determined in the cells of the CAD of $r$-space, truth values for $F$ in the cells of the induced CAD of $k$-space can be determined. Let $c$ be a cell in the CAD of $(i-1)$-space, $k < i \leq r$. $(Q_{i-k}x_i)\cdots(Q_{r-k}x_r)[F']$ is satisfied in $c$ provided that

$Q_{i-k} = \forall$

and $(Q_{i-k+1}x_{i+1})\cdots(Q_{r-k}x_r)[F']$ is satisfied in each of $c$'s children, or

$Q_{i-k} = \exists$

and $(Q_{i-k+1}x_{i+1})\cdots(Q_{r-k}x_r)[F']$ is satisfied in at least one of $c$'s children.

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