Q E P C A D - The Lifting Phase

In the Lifting (or Stack Construction) Phase, which is indicated in QEPCAD by the "Before Choice >" prompt, QEPCAD explicitly constructs a CAD of free variable space in which each cell is marked either true or false. The union of all true cells is exactly the set of points satisfying the input formula. This is done by explicitly constructing some or all of the CAD defined by the projection factor set produced by the projection phase and propagating truth-values of cells in this CAD down to cells in free-variable space according to the quantifiers appearing in the input formula.

The lifting phase is almost always the most expensive phase of quantifer elimination by CAD both in terms of time and of space. First of all there is often many, many cells to be constructed. More often, however, the real bottleneck arises from computations with algebraic numbers. Happily, there is a lot of room for improvement in how QEPCAD deals with lifting, so there is hope that things may improve in future releases.

There are some nifty things you can do here, especially when there are exactly 2 free variables, because you can use topological information here. I'll add more later!


Christopher W Brown
Last modified: Tue Jul 30 15:24:23 EDT 2002