Truth table invariant cylindrical algebraic decomposition
From MaRDI portal
Publication:5963392
DOI10.1016/J.JSC.2015.11.002zbMATH Open1351.68314arXiv1401.0645OpenAlexW1916563250WikidataQ59590566 ScholiaQ59590566MaRDI QIDQ5963392FDOQ5963392
Scott McCallum, Matthew England, James H. Davenport, Russell Bradford, David Wilson
Publication date: 19 February 2016
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1401.0645
Recommendations
- Cylindrical algebraic decompositions for Boolean combinations
- Truth table invariant cylindrical algebraic decomposition by regular chains
- Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition
- scientific article; zbMATH DE number 1262462
- Choosing a variable ordering for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition
Symbolic computation and algebraic computation (68W30) Computational aspects in algebraic geometry (14Q99) Real algebraic and real-analytic geometry (14P99)
Cites Work
- QEPCAD B
- Partial cylindrical algebraic decomposition for quantifier elimination
- Computing cylindrical algebraic decomposition via triangular decomposition
- Solving Non-linear Arithmetic
- An improved projection operation for cylindrical algebraic decomposition of three-dimensional space
- Constructing fewer open cells by GCD computation in CAD projection
- Title not available (Why is that?)
- Improved projection for cylindrical algebraic decomposition
- On the combinatorial and algebraic complexity of quantifier elimination
- Real quantifier elimination is doubly exponential
- Computation with semialgebraic sets represented by cylindrical algebraic formulas
- Title not available (Why is that?)
- Cylindrical algebraic decomposition using validated numerics
- On propagation of equational constraints in CAD-based quantifier elimination
- An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for quantifier elimination
- Title not available (Why is that?)
- Cylindrical Algebraic Decomposition I: The Basic Algorithm
- On the Piano Movers problem. II: General techniques for computing topological properties of real algebraic manifolds
- Algorithmic methods for investigating equilibria in epidemic modeling
- Optimising Problem Formulation for Cylindrical Algebraic Decomposition
- Understanding Branch Cuts of Expressions
- MetiTarski: Past and Future
- Cylindrical algebraic decompositions for boolean combinations
- Constructing a single open cell in a cylindrical algebraic decomposition
- Efficient projection orders for CAD
- Title not available (Why is that?)
- Cylindrical algebraic sub-decompositions
- Geometry of branch cuts
- On using bi-equational constraints in CAD construction
- The complexity of quantifier elimination and cylindrical algebraic decomposition
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- An adjacency algorithm for cylindrical algebraic decompositions of three- dimensional space
- Choosing a Variable Ordering for Truth-Table Invariant Cylindrical Algebraic Decomposition by Incremental Triangular Decomposition
- Cylindrical algebraic decomposition using local projections
- A cluster-based cylindrical algebraic decomposition algorithm
- Using the Regular Chains Library to Build Cylindrical Algebraic Decompositions by Projecting and Lifting
- Improving the use of equational constraints in cylindrical algebraic decomposition
- Truth Table Invariant Cylindrical Algebraic Decomposition by Regular Chains
- Speeding Up Cylindrical Algebraic Decomposition by Gröbner Bases
- A repository for CAD examples
- Problem Formulation for Truth-Table Invariant Cylindrical Algebraic Decomposition by Incremental Triangular Decomposition
- Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition
- Synthesis of optimal numerical algorithms using real quantifier elimination (case study: square root computation)
- Development of SyNRAC
- Branch cuts in maple 17
Cited In (24)
- Validity proof of Lazard's method for CAD construction
- Choosing better variable orderings for cylindrical algebraic decomposition via exploiting chordal structure
- New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis
- Using machine learning to improve cylindrical algebraic decomposition
- $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation
- Lazard-style CAD and Equational Constraints
- Levelwise construction of a single cylindrical algebraic cell
- Cylindrical algebraic decomposition with equational constraints
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- Recent Advances in Real Geometric Reasoning
- Identifying the parametric occurrence of multiple steady states for some biological networks
- Deciding first-order formulas involving univariate mixed trigonometric-polynomials
- Fully incremental cylindrical algebraic decomposition
- Need Polynomial Systems Be Doubly-Exponential?
- Kac-Rice formulas and the number of solutions of parametrized systems of polynomial equations
- Variable Ordering Selection for Cylindrical Algebraic Decomposition with Artificial Neural Networks
- The Complexity of Cylindrical Algebraic Decomposition with Respect to Polynomial Degree
- Cylindrical algebraic sub-decompositions
- Can an A.I. win a medal in the mathematical olympiad? – Benchmarking mechanized mathematics on pre-university problems1
- Improved Cross-Validation for Classifiers that Make Algorithmic Choices to Minimise Runtime Without Compromising Output Correctness
- Regular cylindrical algebraic decomposition
- Recent developments in real quantifier elimination and cylindrical algebraic decomposition (extended abstract of invited talk)
- Choosing the variable ordering for cylindrical algebraic decomposition via exploiting chordal structure
- Problem Formulation for Truth-Table Invariant Cylindrical Algebraic Decomposition by Incremental Triangular Decomposition
Uses Software
This page was built for publication: Truth table invariant cylindrical algebraic decomposition
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5963392)
