Improving the use of equational constraints in cylindrical algebraic decomposition

Abstract

When building a cylindrical algebraic decomposition (CAD) savings can be made in the presence of an equational constraint (EC): an equation logically implied by a formula. The present paper is concerned with how to use multiple ECs, propagating those in the input throughout the projection set. We improve on the approach of McCallum in ISSAC 2001 by using the reduced projection theory to make savings in the lifting phase (both to the polynomials we lift with and the cells lifted over). We demonstrate the benefits with worked examples and a complexity analysis.

References in corpus (4)

• Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition
• Using the Regular Chains Library to build cylindrical algebraic decompositions by projecting and lifting
• Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition
• Using the distribution of cells by dimension in a cylindrical algebraic decomposition

Cited by in corpus (7)

• Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings
• Symbolic Versus Numerical Computation and Visualization of Parameter Regions for Multistationarity of Biological Networks
• Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition
• Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition With Groebner Bases
• New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis
• The Potential and Challenges of CAD with Equational Constraints for SC-Square
• A Geometric Approach to Cylindrical Algebraic Decomposition