More Web Proxy on the site http://driver.im/

research-article

Faster One Block Quantifier Elimination for Regular Polynomial Systems of Equations

Authors:

Mohab Safey El DinAuthors Info & Claims

ISSAC '21: Proceedings of the 2021 International Symposium on Symbolic and Algebraic Computation

Pages 265 - 272

https://doi.org/10.1145/3452143.3465546

Published: 18 July 2021 Publication History

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 D using O((n-s+1) 8^t D ^3t+2(t+D _t) arithmetic operations in the ground field where D = 2(n+s) D^s(D-1)^n-s+1(ⁿ_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).

References

[1]

Anai, H., and Weispfenning, V. Reach set computations using real quantifier elimination. In Hybrid Systems: Computation and Control (2001), Springer Berlin Heidelberg, pp. 63--76.

[2]

Bardet, M., Faugère, J.-C., and Salvy, B. On the complexity of the F5 Gröbner basis algorithm. J. Symb. Comput. 70 (2015), 49--70.

Digital Library

[3]

Basu, S., Pollack, R., and Roy, M.-F. On the combinatorial and algebraic complexity of quantifier elimination. J. ACM 43, 6 (Nov. 1996), 1002--1045.

Digital Library

[4]

Basu, S., Pollack, R., and Roy, M.-F. Algorithms in Real Algebraic Geometry. Springer-Verlag, Berlin, Heidelberg, 2006.

[5]

Berthomieu, J., Eder, C., and Safey El Din, M. msolve: A Library for Solving Polynomial Systems. Preprint, Feb. 2021.

[6]

Brown, C. W. Improved projection for Cylindrical Algebraic Decomposition. J. Symb. Comput. 32, 5 (2001), 447--465.

Digital Library

[7]

Brown, C. W., and Gross, C. Efficient preprocessing methods for quantifier elimination. In Computer Algebra in Scientific Computing (Berlin, Heidelberg, 2006), Springer Berlin Heidelberg, pp. 89--100.

Digital Library

[8]

Collins, G. E. Quantifier elimination for real closed fields by cylindrical algebraic decomposition: a synopsis. ACM SIGSAM Bulletin 10, 1 (1976), 10--12.

Digital Library

[9]

Collins, G. E., and Hong, H. Partial Cylindrical Algebraic Decomposition for quantifier elimination. J. Symb. Comput. 12, 3 (1991), 299--328.

Digital Library

[10]

Cox, D. A., Little, J., and O'Shea, D. Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra, (Undergraduate Texts in Mathematics). Springer-Verlag, Berlin, Heidelberg, 2007.

[11]

Davenport, J. H., and Heintz, J. Real quantifier elimination is doubly exponential. J. Symb. Comput. 5, 1 (1988), 29--35.

Digital Library

[12]

Dolzmann, A., Sturm, T., and Weispfenning, V. A new approach for automatic theorem proving in real geometry. J. Autom. Reason. 21, 3 (Dec. 1998), 357--380.

Digital Library

[13]

Dolzomann, A., and Gilch, L. A. Generic hermitian quantifier elimination. In Artificial Intelligence and Symbolic Computation (Berlin, Heidelberg, 2004), B. Buchberger and J. Campbell, Eds., Springer Berlin Heidelberg, pp. 80--93.

[14]

Eisenbud, D. Commutative Algebra: With a View Toward Algebraic Geometry. Graduate Texts in Mathematics. Springer, 1995.

[15]

Faugère, J.-C. FGb: A Library for Computing Gröbner Bases. In Mathematical Software - ICMS 2010 (2010), vol. 6327 of Lecture Notes in Computer Science, Springer Berlin / Heidelberg, pp. 84--87.

[16]

Faugère, J.-C., Safey El Din, M., and Spaenlehauer, P.-J. On the complexity of the generalized minrank problem. J. Symb. Comput. 55 (2013), 30--58.

[17]

Grigor'ev, D. Y. Complexity of deciding Tarski algebra. J. Symb. Comput. 5, 1--2 (Feb. 1988), 65--108.

Digital Library

[18]

Hermite, C. Sur le nombre des racines d'une équation algébrique comprises entre des limites données. extrait d'une lettre á m. borchardt. J. Reine Angew. Math. 52 (1856), 39--51.

[19]

Hong, H. An improvement of the projection operator in Cylindrical Algebraic Decomposition. In Proceedings of the International Symposium on Symbolic and Algebraic Computation (New York, NY, USA, 1990), ISSAC '90, Association for Computing Machinery, p. 261--264.

Digital Library

[20]

Hong, H., and Safey El Din, M. Variant real quantifier elimination: Algorithm and application. In Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation (New York, NY, USA, 2009), ISSAC '09, Association for Computing Machinery, p. 183--190.

[21]

Hong, H., and Safey El Din, M. Variant quantifier elimination. J. Symb. Comput. 47, 7 (2012), 883--901. International Symposium on Symbolic and Algebraic Computation (ISSAC 2009).

Digital Library

[22]

Le, H. P., and Safey El Din, M. Solving parametric systems of polynomial equations over the reals through Hermite matrices. Preprint, Nov. 2020.

[23]

Liska, R., and Steinberg, S. L. Applying Quantifier Elimination to Stability Analysis of Difference Schemes. The Computer Journal 36, 5 (01 1993), 497--503.

[24]

McCallum, S. An improved projection operation for Cylindrical Algebraic Decomposition of three-dimensional space. J. Symb. Comput. 5 (1988), 141--161.

Digital Library

[25]

McCallum, S. On projection in CAD-based quantifier elimination with equational constraint. In Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation (New York, NY, USA, 1999), ISSAC '99, Association for Computing Machinery, p. 145--149.

[26]

Nie, J., and Ranestad, K. Algebraic degree of polynomial optimization. SIAM J. on Optimization 20, 1 (Apr. 2009), 485--502.

Digital Library

[27]

Pedersen, P., Roy, M.-F., and Szpirglas, A. Counting real zeros in the multivariate case. In Computational Algebraic Geometry (Boston, MA, 1993), F. Eyssette and A. Galligo, Eds., Birkhäuser Boston, pp. 203--224.

[28]

Renegar, J. On the computational complexity and geometry of the first-order theory of the reals. Part III: Quantifier elimination. J. Symb. Comput. 13, 3 (Mar. 1992), 329--352.

[29]

Safey El Din, M. Real alebraic geometry library, RAGlib (version 3.4), 2017.

[30]

Safey El Din, M., and Schost, E. Polar varieties and computation of one point in each connected component of a smooth real algebraic set. In Proc. of the 2003 Int. Symp. on Symb. and Alg. Comp. (NY, USA, 2003), ISSAC '03, ACM, p. 224--231.

[31]

Safey El Din, M., and Schost, É. A nearly optimal algorithm for deciding connectivity queries in smooth and bounded real algebraic sets. J. ACM 63, 6 (Jan. 2017), 48:1--48:37.

[32]

Seidenberg, A. A new decision method for elementary algebra. Annals of Mathematics 60, 2 (1954), 365--374.

[33]

Seidl, A., and Sturm, T. A generic projection operator for partial cylindrical algebraic decomposition. In Proceedings of the 2003 International Symposium on Symbolic and Algebraic Computation (New York, NY, USA, 2003), ISSAC '03, Association for Computing Machinery, p. 240--247.

[34]

Shafarevich, I. R. Basic Algebraic Geometry 1: Varieties in Projective Space. Springer Berlin Heidelberg, Berlin, Heidelberg, 2013.

[35]

Spaenlehauer, P.-J. On the complexity of computing critical points with Gröbner bases. SIAM Journal on Optimization 24 (07 2014), 1382--1401.

Digital Library

[36]

A. W. Cylindrical Algebraic Decomposition using validated numerics. J. Symb. Comput 41, 9 (2006), 1021--1038.

[37]

Sturm, T., and Tiwari, A. Verification and synthesis using real quantifier elimination. In Proceedings of the 36th International Symposium on Symbolic and Algebraic Computation (New York, NY, USA, 2011), ISSAC '11, Association for Computing Machinery, p. 329--336.

[38]

Sturm, T., and Weispfenning, V. Computational geometry problems in REDLOG. In Selected Papers from the International Workshop on Automated Deduction in Geometry (Berlin, Heidelberg, 1996), Springer-Verlag, p. 58--86.

[39]

Tarski, A. A Decision Method for Elementary Algebra and Geometry. University of California Press, 1951.

[40]

Weispfenning, V. The complexity of linear problems in fields. J. Symb. Comput. 5, 1 (1988), 3--27.

Digital Library

[41]

Weispfenning, V. Comprehensive gröbner bases. Journal of Symbolic Computation 14, 1 (1992), 1--29.

Digital Library

[42]

Weispfenning, V. A new approach to quantifier elimination for real algebra. In Quantifier Elimination and Cylindrical Algebraic Decomposition (Vienna, 1998), Springer Vienna, pp. 376--392.

Cited By

Gaillard LSafey El Din M(2024)Solving parameter-dependent semi-algebraic systemsProceedings of the 2024 International Symposium on Symbolic and Algebraic Computation10.1145/3666000.3669718(447-456)Online publication date: 16-Jul-2024
https://dl.acm.org/doi/10.1145/3666000.3669718
Ferguson ALe HMaza MZhi L(2022)Finer Complexity Estimates for the Change of Ordering of Gröbner Bases for Generic Symmetric Determinantal IdealsProceedings of the 2022 International Symposium on Symbolic and Algebraic Computation10.1145/3476446.3536182(399-407)Online publication date: 4-Jul-2022
https://dl.acm.org/doi/10.1145/3476446.3536182

Index Terms

Faster One Block Quantifier Elimination for Regular Polynomial Systems of Equations
1. Computing methodologies
  1. Symbolic and algebraic manipulation
    1. Symbolic and algebraic algorithms
      1. Equation and inequality solving algorithms
2. Theory of computation
  1. Randomness, geometry and discrete structures
    1. Computational geometry

Recommendations

Quantifier elimination for a class of exponential polynomial formulas

Quantifier elimination is a foundational issue in the field of algebraic and logic computation. In first-order logic, every formula is well composed of atomic formulas by negation, conjunction, disjunction, and introducing quantifiers. It is often made ...
Models and quantifier elimination for quantified Horn formulas

In this paper, quantified Horn formulas (QHORN) are investigated. We prove that the behavior of the existential quantifiers depends only on the cases where at most one of the universally quantified variables is zero. Accordingly, we give a detailed ...
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
CPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs

We formalize a multivariate quantifier elimination (QE) algorithm in the theorem prover Isabelle/HOL. Our algorithm is complete, in that it is able to reduce any quantified formula in the first-order logic of real arithmetic to a logically equivalent ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ISSAC '21: Proceedings of the 2021 International Symposium on Symbolic and Algebraic Computation

July 2021

379 pages

ISBN:9781450383820

DOI:10.1145/3452143

General Chair:
Frédéric Chyzak
Inria, France
,
Program Chair:
George Labahn
University of Waterloo, Canada

Copyright © 2021 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSAM: ACM Special Interest Group on Symbolic and Algebraic Manipulation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 July 2021

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

ISSAC '21

Sponsor:

SIGSAM

ISSAC '21: International Symposium on Symbolic and Algebraic Computation

July 18 - 23, 2021

Virtual Event, Russian Federation

Acceptance Rates

Overall Acceptance Rate 395 of 838 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
75
Total Downloads

Downloads (Last 12 months)16
Downloads (Last 6 weeks)1

Reflects downloads up to 18 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Gaillard LSafey El Din M(2024)Solving parameter-dependent semi-algebraic systemsProceedings of the 2024 International Symposium on Symbolic and Algebraic Computation10.1145/3666000.3669718(447-456)Online publication date: 16-Jul-2024
https://dl.acm.org/doi/10.1145/3666000.3669718
Ferguson ALe HMaza MZhi L(2022)Finer Complexity Estimates for the Change of Ordering of Gröbner Bases for Generic Symmetric Determinantal IdealsProceedings of the 2022 International Symposium on Symbolic and Algebraic Computation10.1145/3476446.3536182(399-407)Online publication date: 4-Jul-2022
https://dl.acm.org/doi/10.1145/3476446.3536182

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents