Quantifier elimination over the reals is a central problem in computational real algebraic geometry, polynomial system solving and symbolic computation. Given a semi-algebraic formula (whose atoms are polynomial constraints) with quantifiers on some variables, it consists in computing a logically equivalent formula involving only unquantified variables. When there is no alternation of quantifiers, one has a one block quantifier elimination problem. This paper studies a variant of the one block quantifier elimination in which we compute an almost equivalent formula of the input. We design a new probabilistic efficient algorithm for solving this variant when the input is a system of polynomial equations satisfying some regularity assumptions. When the input is generic, involves $s$ polynomials of degree bounded by $D$ with $n$ quantified variables and $t$ unquantified ones, we prove that this algorithm outputs semi-algebraic formulas of degree bounded by $mathcal{D}$ using $O {widetilde{~}}left ((n-s+1) 8^{t} mathcal{D}^{3t+2} binom{t+mathcal{D}}{t} right )$ arithmetic operations in the ground field where $mathcal{D} = 2(n+s) D^s(D-1)^{n-s+1} binom{n}{s}$. In practice, it allows us to solve quantifier elimination problems which are out of reach of the state-of-the-art (up to $8$ variables).
Download