Séminaire Calcul Formel

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

by Huu Phoc Le (PolSys Team - LIP6 -Sorbonne University)




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 enjoys a determinantal
structure 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^t D^{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 extensive 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

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