Truth Table Invariant Cylindrical Algebraic Decomposition
arXiv:1401.0645 · doi:10.1016/j.jsc.2015.11.002
Abstract
When using cylindrical algebraic decomposition (CAD) to solve a problem with respect to a set of polynomials, it is likely not the signs of those polynomials that are of paramount importance but rather the truth values of certain quantifier free formulae involving them. This observation motivates our article and definition of a Truth Table Invariant CAD (TTICAD). In ISSAC 2013 the current authors presented an algorithm that can efficiently and directly construct a TTICAD for a list of formulae in which each has an equational constraint. This was achieved by generalising McCallum's theory of reduced projection operators. In this paper we present an extended version of our theory which can be applied to an arbitrary list of formulae, achieving savings if at least one has an equational constraint. We also explain how the theory of reduced projection operators can allow for further improvements to the lifting phase of CAD algorithms, even in the context of a single equational constraint. The algorithm is implemented fully in Maple and we present both promising results from experimentation and a complexity analysis showing the benefits of our contributions.
40 pages
References in corpus (10)
- Improving the use of equational constraints in cylindrical algebraic decomposition
- Truth Table Invariant Cylindrical Algebraic Decomposition by Regular Chains
- 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
- Understanding the Learners' Actions when using Mathematics Learning Tools
- Choosing a variable ordering for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition
- Speeding up Cylindrical Algebraic Decomposition by Gröbner Bases
- Cylindrical Algebraic Sub-Decompositions
- An implementation of CAD in Maple utilising McCallum projection
- An Incremental Algorithm for Computing Cylindrical Algebraic Decompositions
Cited by in corpus (35)
- Satisfiability Checking meets Symbolic Computation (Project Paper)
- Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings
- Improving the use of equational constraints in cylindrical algebraic decomposition
- Truth Table Invariant Cylindrical Algebraic Decomposition by Regular Chains
- Identifying the Parametric Occurrence of Multiple Steady States for some Biological Networks
- Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition
- Cylindrical Algebraic Decomposition with Equational Constraints
- Using Machine Learning to Improve Cylindrical Algebraic Decomposition
- The complexity of cylindrical algebraic decomposition with respect to polynomial degree
- Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition
- Symbolic Versus Numerical Computation and Visualization of Parameter Regions for Multistationarity of Biological Networks
- Choosing a variable ordering for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition
- Machine Learning for Mathematical Software
- Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition With Groebner Bases
- Levelwise construction of a single cylindrical algebraic cell
- New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis
- Algorithmically generating new algebraic features of polynomial systems for machine learning
- Polynomial Superlevel Set Representation of the Multistationarity Region of Chemical Reaction Networks
- Improved cross-validation for classifiers that make algorithmic choices to minimise runtime without compromising output correctness
- Need Polynomial Systems be Doubly-exponential?
- How to flatten a soccer ball
- New Opportunities for the Formal Proof of Computational Real Geometry?
- Regular cylindrical algebraic decomposition
- Recent Advances in Real Geometric Reasoning
- Lazard-style CAD and Equational Constraints
- Quantifier Elimination for Reasoning in Economics
- The DEWCAD Project: Pushing Back the Doubly Exponential Wall of Cylindrical Algebraic Decomposition
- The Potential and Challenges of CAD with Equational Constraints for SC-Square
- Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics
- Towards Incremental Cylindrical Algebraic Decomposition in Maple
- Recent Developments in Real Quantifier Elimination and Cylindrical Algebraic Decomposition
- Validity proof of Lazard's method for CAD construction
- Choosing the Variable Ordering for Cylindrical Algebraic Decomposition via Exploiting Chordal Structure
- An implementation of Sub-CAD in Maple
- Understanding Multistationarity of Fully Open Reaction Networks