Cylindrical Algebraic Decompositions for Boolean Combinations

TL;DR

This paper introduces Truth Table Invariant CAD (TTICAD), a new approach that focuses on truth values of formulae rather than polynomial signs, leading to more efficient problem-solving in algebraic decomposition.

Contribution

It generalizes equational constraints to develop an algorithm for constructing TTICAD, improving efficiency and results over traditional methods.

Findings

Implemented in Maple with promising experimental results

Produces stronger results than using equational constraints alone

Efficiently constructs TTICAD for a wide class of problems

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.