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 contribution

13 Citations (Scopus)
125 Downloads (Pure)

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.
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
Pages125-132
ISBN (Print)9781450320597
DOIs
Publication statusPublished - 2013
EventISSAC 2013: International Symposium on Symbolic and Algebraic Computation - Boston, USA United States
Duration: 25 Jun 201328 Jun 2013

Conference

ConferenceISSAC 2013: International Symposium on Symbolic and Algebraic Computation
CountryUSA United States
CityBoston
Period25/06/1328/06/13

Keywords

  • cylindrical algebraic decomposition
  • equational constraint

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

Cite this