Truth table invariant cylindrical algebraic decomposition
From MaRDI portal
Publication:5963392
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.
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
Cites work
- scientific article; zbMATH DE number 1262462 (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 2151206 (Why is no real title available?)
- scientific article; zbMATH DE number 2151213 (Why is no real title available?)
- scientific article; zbMATH DE number 3996993 (Why is no real title available?)
- A cluster-based cylindrical algebraic decomposition algorithm
- A repository for CAD examples
- Algorithmic methods for investigating equilibria in epidemic modeling
- An adjacency algorithm for cylindrical algebraic decompositions of three- dimensional space
- An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for quantifier elimination
- An improved projection operation for cylindrical algebraic decomposition of three-dimensional space
- Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition
- Branch cuts in Maple 17
- Choosing a variable ordering for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition
- Computation with semialgebraic sets represented by cylindrical algebraic formulas
- 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 I: The Basic Algorithm
- Cylindrical algebraic decomposition using local projections
- Cylindrical algebraic decomposition using validated numerics
- Cylindrical algebraic decompositions for Boolean combinations
- Cylindrical algebraic sub-decompositions
- Development of SyNRAC
- Efficient projection orders for CAD
- Geometry of branch cuts
- Improved projection for cylindrical algebraic decomposition
- Improving the use of equational constraints in cylindrical algebraic decomposition
- MetiTarski: past and future
- 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 the combinatorial and algebraic complexity of quantifier elimination
- On using bi-equational constraints in CAD construction
- 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 is doubly exponential
- Solving non-linear arithmetic
- Speeding up cylindrical algebraic decomposition by Gröbner bases
- Synthesis of optimal numerical algorithms using real quantifier elimination (case study: square root computation)
- The complexity of quantifier elimination and cylindrical algebraic decomposition
- Truth table invariant cylindrical algebraic decomposition by regular chains
- Understanding branch cuts of expressions
- Using the Regular Chains library to build cylindrical algebraic decompositions by projecting and lifting
Cited in
(26)- Cylindrical algebraic decomposition with equational constraints
- Levelwise construction of a single cylindrical algebraic cell
- Cylindrical algebraic decompositions for Boolean combinations
- \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
- Using machine learning to improve cylindrical algebraic decomposition
- The complexity of cylindrical algebraic decomposition with respect to polynomial degree
- Validity proof of Lazard's method for CAD construction
- Identifying the parametric occurrence of multiple steady states for some biological networks
- Kac-Rice formulas and the number of solutions of parametrized systems of polynomial equations
- Can an A.I. win a medal in the mathematical olympiad? -- Benchmarking mechanized mathematics on pre-university problems
- New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis
- Truth table invariant cylindrical algebraic decomposition by regular chains
- Deciding first-order formulas involving univariate mixed trigonometric-polynomials
- Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition
- Fully incremental cylindrical algebraic decomposition
- Variable ordering selection for cylindrical algebraic decomposition with artificial neural networks
- Need polynomial systems be doubly-exponential?
- Improved Cross-Validation for Classifiers that Make Algorithmic Choices to Minimise Runtime Without Compromising Output Correctness
- Regular cylindrical algebraic decomposition
- Recent advances in real geometric reasoning
- Choosing better variable orderings for cylindrical algebraic decomposition via exploiting chordal structure
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- Cylindrical algebraic sub-decompositions
- Lazard-style CAD and Equational Constraints
- 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
Describes a project that uses
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)
