Cylindrical algebraic decompositions for boolean combinations

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

Research output: Chapter in Book/Report/Conference proceedingConference proceedingpeer-review

31 Citations (Scopus)


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 inMaple and we present promising results from experimentation.

Original languageEnglish
Title of host publicationISSAC 2013 - Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation
EditorsManual Kauers
Place of PublicationNew York
Number of pages8
ISBN (Print)9781450320597
Publication statusPublished - 2013
Externally publishedYes
Event38th International Symposium on Symbolic and Algebraic Computation, ISSAC 2013 - Boston, United States
Duration: 26 Jun 201329 Jun 2013


Conference38th International Symposium on Symbolic and Algebraic Computation, ISSAC 2013
Country/TerritoryUnited States


  • Cylindrical algebraic decomposition
  • Equational constraint

ASJC Scopus subject areas

  • Mathematics(all)


Dive into the research topics of 'Cylindrical algebraic decompositions for boolean combinations'. Together they form a unique fingerprint.

Cite this