A short history of quantifier elimination methods

In the 1930's, A. Tarski proved that a solution formula exists for any input formula by giving an algorithm for its construction [Tarski(1951)]. Unfortunately, the computational costs of the method made it impractical except for trivial problems. Seidenberg [Seidenberg(1954)] in 1954 and Cohen [Cohen(1969)] in 1969 both offered alternative methods for solving the problem, neither of which was clearly superior to Tarski's in terms of time complexity. However, in 1973 Collins discovered a totally new method [Collins(1975)] based on cylindrical algebraic decomposition (CAD) that was far more efficient than any previous approach. The method has time complexity doubly exponential in the number of variables in $F$, but polynomial in the number of polynomials in $F$, the degree of the polynomials in $F$, the bit length of coefficients in $F$, and the number of atomic formulas in $F$. The method has since been improved in many ways, has been implemented, and has shown itself to be capable of solving non-trivial problems.

Other methods for solving the quantifier elimination problem have been proposed since the introduction of the CAD based algorithm. The methods of Renegar [Renegar(1992)] and of Heintz et. al. [Heintz et al.(1990)Heintz, Roy, and Solernó] are both doubly exponential in the number of quantifier alternations rather than the number of variables. Renegar claimed that Grigor'ev's decision procedure [Grigor'ev(1988)] could be extended to a quantifier elimination algorithm, the complexity of which would be doubly exponential in the number of quantifier alternations, though inferior to that of Renegar and of Heintz et. al.. In [Weispfenning(1998)], Weispfenning introduced another approach to quantifier elimination, based on comprehensive Gröbner bases and the work of Pedersen, Roy, and Szpirglas [Pedersen et al.(1993)Pedersen, Roy, and Szpirglas]. No asymptotic analysis was given.

Other research has focused on the consideration of restrictions of the full theory of real closed fields. For example, Weispfenning [Weispfenning(1988)] considered formulas in which bound variables appear only linearly. Hong [Hong(1993)] treated the case of an input formula of the form

$$(\exists x)[ a_2 x^2 + a_1 x + a_0 = 0 \hspace{0.1 in} \wedge \hspace{0.1 in}F' ]$$

where $F'$ is a quantifier free formula. Finally, Weispfenning [Weispfenning(1994),Weispfenning(1997)] has developed a method for attacking certain formulas in which the quantified variables appear at most cubically. The method has been implemented and has successfully dealt with many problems that would be impractical for the CAD-based method. Its complexity is not dependent on the number of free variables in $F$, which is valuable in many problems. He also indicates how the method might be extended to the full theory, i.e. no degree restrictions.

The quantifier elimination problem is inherently doubly exponential in the number of variables [Fischer and Rabin(1974),Davenport and Heintz(1997)], so any algorithm for the full theory must work within these bounds. Despite this imposing worst case time complexity, there is hope that many non-trivial problems will be solvable in a reasonable amount of time. My goal is to improve the CAD algorithm to enlarge the scope of its practical applicability.