Next: Stack construction Up: An overview of quantifier Previous: What is a CAD?

Projection

Any set of polynomials in defines a natural algebraic decomposition of into maximal connected regions in which the elements of the set have invariant signs. Let be the set of polynomials appearing in . The goal of the projection phase is to produce a set , , such that the natural decomposition defined by is a CAD. The set is called a projection factor set.

Because of the recursive nature of CAD's, the natural algebraic decomposition defined by is a CAD of -- the induced CAD of -space. Since (the set of polynomials appearing in ) is contained in , the induced CAD of -space (the space of the free variables of ) is truth-invariant with respect to . This means that for any two points and in the same cell, . The truth invariance of the induced CAD of -space is crucial for the application of CAD's to quantifier elimination.

The to be computed by the projection phase is not unique, and there have been several projection operators'' proposed for the construction of [Collins(1975),Hong(1990),McCallum(1998),Brown(2001)]. A projection operator, , is a function that maps a set of -level polynomials to a set of polynomials of level less than . Let be a set of -level polynomials, and let be . The key property of is that if is a region in in which the elements of have invariant sign, then the maximal sign-invariant regions of form a stack in . 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 -closure of the set of polynomials appearing in . It is sufficient to deal with these irreducible factors and much more efficient.

Next: Stack construction Up: An overview of quantifier Previous: What is a CAD?
Christopher W Brown
2001-07-10