Cylindrical algebraic decomposition with equational constraints
From MaRDI portal
Publication:2307622
Abstract: Cylindrical Algebraic Decomposition (CAD) has long been one of the most important algorithms within Symbolic Computation, as a tool to perform quantifier elimination in first order logic over the reals. More recently it is finding prominence in the Satisfiability Checking community as a tool to identify satisfying solutions of problems in nonlinear real arithmetic. The original algorithm produces decompositions according to the signs of polynomials, when what is usually required is a decomposition according to the truth of a formula containing those polynomials. One approach to achieve that coarser (but hopefully cheaper) decomposition is to reduce the polynomials identified in the CAD to reflect a logical structure which reduces the solution space dimension: the presence of Equational Constraints (ECs). This paper may act as a tutorial for the use of CAD with ECs: we describe all necessary background and the current state of the art. In particular, we present recent work on how McCallum's theory of reduced projection may be leveraged to make further savings in the lifting phase: both to the polynomials we lift with and the cells lifted over. We give a new complexity analysis to demonstrate that the double exponent in the worst case complexity bound for CAD reduces in line with the number of ECs. We show that the reduction can apply to both the number of polynomials produced and their degree.
Recommendations
- Improving the use of equational constraints in cylindrical algebraic decomposition
- The complexity of cylindrical algebraic decomposition with respect to polynomial degree
- Cylindrical algebraic decompositions for Boolean combinations
- The Potential and Challenges of CAD with Equational Constraints for SC-Square
- Partial cylindrical algebraic decomposition for quantifier elimination
Cites work
- \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
- A case study on the parametric occurrence of multiple steady states
- A symbiosis of interval constraint propagation and cylindrical algebraic decomposition
- Algorithmic methods for investigating equilibria in epidemic modeling
- Algorithms in real algebraic geometry
- An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for quantifier elimination
- Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition
- Bruno Buchberger's PhD thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. Translation from the German
- Computing cylindrical algebraic decomposition via triangular decomposition
- Constructing a single open cell in a cylindrical algebraic decomposition
- Constructing fewer open cells by GCD computation in CAD projection
- Cylindrical algebraic decomposition using local projections
- Cylindrical algebraic decomposition using validated numerics
- Cylindrical algebraic decompositions for Boolean combinations
- Cylindrical algebraic sub-decompositions
- Dimension-dependent bounds for Gröbner bases of polynomial ideals
- Efficient projection orders for CAD
- Explicit factors of some iterated resultants and discriminants
- Factors of iterated resultants and discriminants
- scientific article; zbMATH DE number 3497890 (Why is no real title available?)
- scientific article; zbMATH DE number 589124 (Why is no real title available?)
- scientific article; zbMATH DE number 1157648 (Why is no real title available?)
- scientific article; zbMATH DE number 1157658 (Why is no real title available?)
- scientific article; zbMATH DE number 2151220 (Why is no real title available?)
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- Identifying the parametric occurrence of multiple steady states for some biological networks
- Improved projection for cylindrical algebraic decomposition
- Improving the use of equational constraints in cylindrical algebraic decomposition
- Iterated discriminants
- Le formalisme du résultant. (The formalism of resultant)
- Machine learning for mathematical software
- MetiTarski: past and future
- On delineability of varieties in CAD-based quantifier elimination with two equational constraints
- On propagation of equational constraints in CAD-based quantifier elimination
- On the Piano Movers problem. II: General techniques for computing topological properties of real algebraic manifolds
- On using bi-equational constraints in CAD construction
- On using Lazard's projection in CAD construction
- Open non-uniform cylindrical algebraic decompositions
- Optimising problem formulation for cylindrical algebraic decomposition
- Partial cylindrical algebraic decomposition for quantifier elimination
- Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition
- QEPCAD B
- Real quantifier elimination by computation of comprehensive Gröbner systems
- Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation)
- Real quantifier elimination is doubly exponential
- Solving non-linear arithmetic
- Speeding up cylindrical algebraic decomposition by Gröbner bases
- Symbolic versus numerical computation and visualization of parameter regions for multistationarity of biological networks
- The complexity of cylindrical algebraic decomposition with respect to polynomial degree
- The complexity of quantifier elimination and cylindrical algebraic decomposition
- The complexity of the word problems for commutative semigroups and polynomial ideals
- TheoryGuru: a Mathematica package to apply quantifier elimination technology to economics
- Truth table invariant cylindrical algebraic decomposition
- Truth table invariant cylindrical algebraic decomposition by regular chains
- Using machine learning to improve cylindrical algebraic decomposition
- Using the Regular Chains library to build cylindrical algebraic decompositions by projecting and lifting
- Validity proof of Lazard's method for CAD construction
- What is new in CoCoA?
Cited in
(20)- Interval arithmetic in cylindrical algebraic decomposition
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis
- Constructing a single cell in cylindrical algebraic decomposition
- Improving the use of equational constraints in cylindrical algebraic decomposition
- The complexity of cylindrical algebraic decomposition with respect to polynomial degree
- Speeding up cylindrical algebraic decomposition by Gröbner bases
- On propagation of equational constraints in CAD-based quantifier elimination
- Simplification of Cylindrical Algebraic Formulas
- scientific article; zbMATH DE number 784883 (Why is no real title available?)
- Improved Cross-Validation for Classifiers that Make Algorithmic Choices to Minimise Runtime Without Compromising Output Correctness
- Curtains in CAD: Why Are They a Problem and How Do We Fix Them?
- A Machine Learning Based Software Pipeline to Pick the Variable Ordering for Algorithms with Polynomial Inputs
- Kac-Rice formulas and the number of solutions of parametrized systems of polynomial equations
- Lazard-style CAD and Equational Constraints
- Faster real root decision algorithm for symmetric polynomials
- Explainable AI insights for symbolic computation: a case study on selecting the variable ordering for cylindrical algebraic decomposition
- Levelwise construction of a single cylindrical algebraic cell
- Iterated resultants and rational functions in real quantifier elimination
- A geometric approach to cylindrical algebraic decomposition
Describes a project that uses
Uses Software
This page was built for publication: Cylindrical algebraic decomposition with equational constraints
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2307622)
