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!