Skip to Main content Skip to Navigation
Conference papers

Faster One Block Quantifier Elimination for Regular Polynomial Systems of Equations

Abstract : 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).
Complete list of metadata
Contributor : Huu Phuoc Le <>
Submitted on : Wednesday, May 26, 2021 - 11:14:11 AM
Last modification on : Friday, June 4, 2021 - 3:36:41 AM


Files produced by the author(s)



Huu Phuoc Le, Mohab Safey El Din. Faster One Block Quantifier Elimination for Regular Polynomial Systems of Equations. International Symposium on Symbolic and Algebraic Computation 2021 (ISSAC '21), Jul 2021, Saint Petersburg, Russia. ⟨10.1145/3452143.3465546⟩. ⟨hal-03180730v4⟩



Record views


Files downloads