Solution formula construction

The goal of the solution formula construction phase is to use the CAD of free-variable space and the truth values of $F$ in its cells to construct ${\overline F}$, the equivalent quantifier-free formula. Solution formula construction was the focus of my dissertation [Brown(99)], which means that it's painful for me to even tink about it. However, I'll give a quick description.

A formula in this context usually means a ``Tarski Formula'', i.e. a boolean combination of sign conditions on polynomials. Given our CAD of free variable space (augmented with truth values) the only polynomials that we have at our disposal that are at all related to the set we wish to describe are the projection factors, so we would like to construct our solution formula as a boolean combination of sign conditions on the elements of the projection factor set. While this is often possible, unfortunately it is not always possible, which is a fundamental problem. So there are three fundamental approaches to solution formula construction:

1. We construct a formula from the elements of the projection factor set. If this is possible, construction of simple solution formulas essentially becomes a combinatorial problem, which is very nice. This idea comes from [Hong(1992)], and is discussed in more detail in [Brown(99)]. It is actually (more or less) easy to decide whether or not this is possible. When it is, this CAD-with-truth-values is called Projection Definable.
2. If the elements of the projection factor set do not suffice for the construction of a solution formula, we can add new polynomials into the projection factor set, thereby enlarging the projection factor set so that solution formula construction is possible. This approach is described in [Brown(1999)]. The problem with this, is that by adding polynomials to the projection factor set, we introduce new cells (probably lots of new cells!) which require new algebraic computations to construct. This is often slow!
3. Finally, we can always construct solution formulas from the elements of the projection factor set if we extend the language in in which formulas are expressed -- specifically if we allow reference to ``indexed roots'' of polynomials. This allows us to specify, for example, the positive square root of 2 as $root_2(x^2 - 2)$. In the language of Tarski formulas this is only expressible by introducing another polynomial, as in $x > 0 \wedge x^2 - 2 = 0$. This idea is explored in [Brown(99)], and in a more restricted setting in [Strzebonski(2000)]. The nice thing about this language is that CAD is just as comfortable with it as with the language of Tarski Formulas, so that a formula in this language may be used as input to a new quantifier elimination by CAD problem.