Cylindrical algebraic decompositions for Boolean combinations

DOI10.1145/2465506.2465516MaRDI QIDQ2963225zbMATH OpenOpenAlexDBLPWikidataFDO

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)

Full work available at URL https://arxiv.org/abs/1304.7603, http://opus.bath.ac.uk/33926/5/England_ISSAC2013.pdf

zbMATH Keywords

cylindrical algebraic decompositionequational constraint

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

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.

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

Cited in

(20)

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

Describes a project that uses

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)