Cylindrical algebraic decompositions for Boolean combinations

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

Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

20 Citations (SciVal)
145 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationISSAC '13: Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation
Place of PublicationNew York
PublisherAssociation for Computing Machinery
ISBN (Print)9781450320597
Publication statusPublished - 2013
EventISSAC 2013: International Symposium on Symbolic and Algebraic Computation - Boston, USA United States
Duration: 25 Jun 201328 Jun 2013


ConferenceISSAC 2013: International Symposium on Symbolic and Algebraic Computation
Country/TerritoryUSA United States


  • cylindrical algebraic decomposition
  • equational constraint


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

Cite this