Cylindrical algebraic decompositions for Boolean combinations

DOI10.1145/2465506.2465516zbMATH Open1359.68327DBLPconf/issac/BradfordDEMW13arXiv1304.7603OpenAlexW2113881937WikidataQ59590588 ScholiaQ59590588MaRDI QIDQ2963225FDOQ2963225

Authors: Matthew England, Scott McCallum, Russell Bradford, James H. Davenport, David Wilson 

Publication date: 10 February 2017

Published in: Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1304.7603

Recommendations

• Truth table invariant cylindrical algebraic decomposition
• Truth table invariant cylindrical algebraic decomposition by regular chains
• Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition
• Partial cylindrical algebraic decomposition for quantifier elimination
• Simple CAD construction and its applications

zbMATH Keywords

cylindrical algebraic decompositionequational constraint

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Cited In (20)

• Quantifier elimination by cylindrical algebraic decomposition based on regular chains
• Using machine learning to improve cylindrical algebraic decomposition
• Lazard-style CAD and Equational Constraints
• Speeding up cylindrical algebraic decomposition by Gröbner bases
• Truth table invariant cylindrical algebraic decomposition by regular chains
• Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition
• Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition
• Need polynomial systems be doubly-exponential?
• Cylindrical algebraic decomposition with equational constraints
• Simple CAD construction and its applications
• The complexity of cylindrical algebraic decomposition with respect to polynomial degree
• Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation)
• Special algorithm for stability analysis of multistable biological regulatory systems
• Solving Polynomial Strict Inequalities Using Cylindrical Algebraic Decomposition
• Cylindrical algebraic sub-decompositions
• Truth table invariant cylindrical algebraic decomposition
• Boolean Reducts of Relation and Cylindric Algebras and the Cube Problem
• On using Lazard's projection in CAD construction
• Optimising problem formulation for cylindrical algebraic decomposition
• Recent advances in real geometric reasoning

Uses Software

• Maple

This page was built for publication: Cylindrical algebraic decompositions for Boolean combinations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2963225)