Cylindrical Algebraic Decompositions for Boolean Combinations
arXiv:1304.7603 · doi:10.1145/2465506.2465516
Abstract
This article makes the key observation that when using cylindrical algebraic decomposition (CAD) to solve a problem with respect to a set of polynomials, it is not always the signs of those polynomials that are of paramount importance but rather the truth values of certain quantifier free formulae involving them. This motivates our definition of a Truth Table Invariant CAD (TTICAD). We generalise the theory of equational constraints to design an algorithm which will efficiently construct a TTICAD for a wide class of problems, producing stronger results than when using equational constraints alone. The algorithm is implemented fully in Maple and we present promising results from experimentation.
To appear in the proceedings of the 38th International Symposium on Symbolic and Algebraic Computation (ISSAC '13)
References in corpus (1)
Cited by in corpus (26)
- Truth Table Invariant Cylindrical Algebraic Decomposition
- Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition
- Improving the use of equational constraints in cylindrical algebraic decomposition
- Truth Table Invariant Cylindrical Algebraic Decomposition by Regular Chains
- Optimising Problem Formulation 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
- 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
- Choosing a variable ordering for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition
- Cylindrical Algebraic Sub-Decompositions
- Understanding Branch Cuts of Expressions
- Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition With Groebner Bases
- Using the distribution of cells by dimension in a cylindrical algebraic decomposition
- An implementation of CAD in Maple utilising problem formulation, equational constraints and truth-table invariance
- A "Piano Movers" Problem Reformulated
- An implementation of CAD in Maple utilising McCallum projection
- Need Polynomial Systems be Doubly-exponential?
- Branch Cuts in Maple 17
- Recent Advances in Real Geometric Reasoning
- Lazard-style CAD and Equational Constraints
- The Potential and Challenges of CAD with Equational Constraints for SC-Square
- An implementation of Sub-CAD in Maple
- Special Algorithm for Stability Analysis of Multistable Biological Regulatory Systems