Cylindrical algebraic decompositions for boolean combinations

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

doi:10.1145/2465506.2465516

Cylindrical algebraic decompositions for boolean combinations

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

School of Computing

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

30 Citations (Scopus)

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

Original language	English
Title of host publication	ISSAC 2013 - Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation
Editors	Manuel Kauers
Place of Publication	New York
Publisher	Association for Computing Machinery
Pages	125-132
Number of pages	8
ISBN (Print)	9781450320597
DOIs	https://doi.org/10.1145/2465506.2465516
Publication status	Published - 2013
Event	38th International Symposium on Symbolic and Algebraic Computation, ISSAC 2013 - Boston, MA, United States Duration: 26 Jun 2013 → 29 Jun 2013

Other

Other	38th International Symposium on Symbolic and Algebraic Computation, ISSAC 2013
Country/Territory	United States
City	Boston, MA
Period	26/06/13 → 29/06/13

Access to Document

10.1145/2465506.2465516

Cite this

@inproceedings{d223e54d26be46e194593f9a457928d4,

title = "Cylindrical algebraic decompositions for boolean combinations",

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

author = "Russell Bradford and Davenport, {James H.} and Matthew England and Scott McCallum and David Wilson",

year = "2013",

doi = "10.1145/2465506.2465516",

language = "English",

isbn = "9781450320597",

pages = "125--132",

editor = "Manuel Kauers",

booktitle = "ISSAC 2013 - Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation",

publisher = "Association for Computing Machinery",

note = "38th International Symposium on Symbolic and Algebraic Computation, ISSAC 2013 ; Conference date: 26-06-2013 Through 29-06-2013",

}

Bradford, R, Davenport, JH, England, M, McCallum, S & Wilson, D 2013, Cylindrical algebraic decompositions for boolean combinations. in M Kauers (ed.), ISSAC 2013 - Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation. Association for Computing Machinery, New York, pp. 125-132, 38th International Symposium on Symbolic and Algebraic Computation, ISSAC 2013, Boston, MA, United States, 26/06/13. https://doi.org/10.1145/2465506.2465516

Cylindrical algebraic decompositions for boolean combinations. / Bradford, Russell; Davenport, James H.; England, Matthew; McCallum, Scott; Wilson, David.

ISSAC 2013 - Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation. ed. / Manuel Kauers. New York : Association for Computing Machinery, 2013. p. 125-132.

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

TY - GEN

T1 - Cylindrical algebraic decompositions for boolean combinations

AU - Bradford, Russell

AU - Davenport, James H.

AU - England, Matthew

AU - McCallum, Scott

AU - Wilson, David

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84882280923&partnerID=8YFLogxK

U2 - 10.1145/2465506.2465516

DO - 10.1145/2465506.2465516

M3 - Conference proceeding contribution

AN - SCOPUS:84882280923

SN - 9781450320597

SP - 125

EP - 132

BT - ISSAC 2013 - Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation

A2 - Kauers, Manuel

PB - Association for Computing Machinery

CY - New York

T2 - 38th International Symposium on Symbolic and Algebraic Computation, ISSAC 2013

Y2 - 26 June 2013 through 29 June 2013

ER -

Cylindrical algebraic decompositions for boolean combinations

Abstract

Other

Access to Document

Other files and links

Fingerprint

Cite this