One block quantifier elimination over the reals: algorithms, complexity and applications

Quantifier elimination over the reals is one of the central algorithmic problem in effective real algebraic geometry. Given a quantified semi-algebraic formula, it consists in computing a logically equivalent quantifier-free formula.

In this task, I will describe a new efficient algorithm for one block quantifier elimination under some mild assumptions. This computes semi-algebraic formulas which describe a dense subset of the interior of the projection of a given real algebraic set on a subset of coordinates. Interestingly, the output formula is encoded through a determinantal representation which make them easy to evaluate.

Under some genericity assumptions, we use the theory of Groebner bases to prove that our algorithm runs in time O(8^tD^{4nt}) where D
bounds the degree of the input variables, n is the number of quantified variables and t the number of parameters. Note that, by contrast with the classical Cylindrical Algebraic Decomposition algorithm (which is doubly exponential in n and t), our algorithm runs in time singly exponential.

We report on practical experiments and show that our implementation outperforms the state-of-the-art software.

Our algorithm relies on properties of Groebner bases, specialization properties of Hermite quadratic forms (a tool for real root counting) and new algorithms for solving zero-dimensional parametric systems.

Next, we show how to apply our contributions to compute the totally real hyperplane sections coming from the theory of real algebraic curves.

This talk gathers joint works with Dimitri Manevich, Daniel Plaumann and Mohab Safey El Din.