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

Macquarie University

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

20 Citations (SciVal)

176 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 language	English
Title of host publication	ISSAC '13: Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation
Place of Publication	New York
Publisher	Association for Computing Machinery
Pages	125-132
ISBN (Print)	9781450320597
DOIs	https://doi.org/10.1145/2465506.2465516
Publication status	Published - 2013
Event	ISSAC 2013: International Symposium on Symbolic and Algebraic Computation - Boston, USA United States Duration: 25 Jun 2013 → 28 Jun 2013

Conference

Conference	ISSAC 2013: International Symposium on Symbolic and Algebraic Computation
Country/Territory	USA United States
City	Boston
Period	25/06/13 → 28/06/13

Keywords

cylindrical algebraic decomposition
equational constraint

Access to Document

10.1145/2465506.2465516

Author's accepted version
© ACM 2013. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was publishined in 'ISSAC '13 Proceedings of the 38th international symposium on International symposium on symbolic and algebraic computation' 2013, http://doi.acm.org/10.1145/2465506.2465516
Accepted author manuscript, 4.59 MB

Cite this

Cylindrical algebraic decompositions for Boolean combinations. / Bradford, Russell; Davenport, James H; England, Matthew et al.
ISSAC '13: Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation. New York: Association for Computing Machinery, 2013. p. 125-132.

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

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

@inproceedings{cb7978e77ca447769711117472d539f7,

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

keywords = "cylindrical algebraic decomposition, equational constraint",

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",

booktitle = "ISSAC '13: Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation",

publisher = "Association for Computing Machinery",

address = "USA United States",

note = "ISSAC 2013: International Symposium on Symbolic and Algebraic Computation ; Conference date: 25-06-2013 Through 28-06-2013",

}

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

KW - cylindrical algebraic decomposition

KW - equational constraint

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

UR - http://www.issac-conference.org/2013/

UR - http://dx.doi.org/10.1145/2465506.2465516

U2 - 10.1145/2465506.2465516

DO - 10.1145/2465506.2465516

M3 - Chapter in a published conference proceeding

AN - SCOPUS:84871659975

SN - 9781450320597

SP - 125

EP - 132

BT - ISSAC '13: Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation

PB - Association for Computing Machinery

CY - New York

T2 - ISSAC 2013: International Symposium on Symbolic and Algebraic Computation

Y2 - 25 June 2013 through 28 June 2013

ER -

Cylindrical algebraic decompositions for Boolean combinations

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Real Geometry and Connectedness via Triangular Description

Cite this

Cylindrical algebraic decompositions for Boolean combinations

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Projects

Real Geometry and Connectedness via Triangular Description

Cite this