Projection

Any set of polynomials in $\mathbb {Z}[x_1,\ldots ,x_r]$ defines a natural algebraic decomposition of $\mathbb {R}^r$ into maximal connected regions in which the elements of the set have invariant signs. Let $A$ be the set of polynomials appearing in $F$. The goal of the projection phase is to produce a set $P$, $A \subseteq P \subset \mathbb {R}[x_1,\ldots , x_r]$, such that the natural decomposition defined by $P$ is a CAD. The set $P$ is called a projection factor set.

Because of the recursive nature of CAD's, the natural algebraic decomposition defined by $\bigcup_{j=1}^i P_j$ is a CAD of $\mathbb {R}^i$ -- the induced CAD of $i$-space. Since $A$ (the set of polynomials appearing in $F$) is contained in $P$, the induced CAD of $k$-space (the space of the free variables of $F$) is truth-invariant with respect to $F$. This means that for any two points $\alpha$ and $\beta$ in the same cell, $F\vert _\alpha \Longleftrightarrow F\vert _\beta$. The truth invariance of the induced CAD of $k$-space is crucial for the application of CAD's to quantifier elimination.

The $P$ to be computed by the projection phase is not unique, and there have been several ``projection operators'' proposed for the construction of $P$ [Collins(1975),Hong(1990),McCallum(1998),Brown(2001)]. A projection operator, $\mbox{PROJ}$, is a function that maps a set of $i$-level polynomials to a set of polynomials of level less than $i$. Let $Q$ be a set of $i$-level polynomials, and let $S$ be $\mbox{PROJ}(Q)$. The key property of $\mbox{PROJ}$ is that if $\cal A$ is a region in $\mathbb {R}^{i-1}$ in which the elements of $S$ have invariant sign, then the maximal sign-invariant regions of $Q$ form a stack in ${\cal A} \times \mathbb {R}$. A set of polynomials that is closed under the projection operator is easily seen to define a CAD -- i.e. the natural algebraic decomposition of such a set is a CAD. The set of projection factors is constructed by computing the irreducible factors of the $\mbox{PROJ}$-closure of the set of polynomials appearing in $F$. It is sufficient to deal with these irreducible factors and much more efficient.