Complexity of quantifier elimination

[Bonny Banerjee]

I would like to know the computational complexity of the algorithm used by
Mathematica for eliminating quantifiers from polynomials, preferably in the
domain of Reals. It would be very helpful if someone could let me know about
it or point me towards some relevant literature from where I can figure it
out.

I assume Mathematica exploits the algorithms with the best complexity. If
not, any reference to the algorithm with the best complexity will be
appreciated.

Thanks,
Bonny.

[Andrzej Kozlowski]

I believe Mathematica uses Collins's Cylindrical Algebraic
Decomposition for quantifier elimination. The complexity of this
algorithm is huge : double exponential in the number of variables. A
much faster algorithm exists and is due to Basu, Pollack and Roy (see
their book "Algorithms in Real Algebraic Geometry"). The complexity
of this algorithm is still double exponential but not in the number
of variables but in the number of blocks of variables, where the
blocks of variables are delimited by alternations of the existential
and universal quantifiers. I am not sure if this algorithm has ever
been implemented in practice. Certainly, at the time when the book
was published (2003) no such implementation existed (the authors
state so in the preface). Having glanced at their argument, it seems
to me that such an implementation would be a highly non-trivial task.
Of course, if you really wish to know, you could try searching the
Internet for this topic.
Another possibility is that Adam Strzebonski will post a more
accurate answer than mine ;-)

Andrzej Kozlowski