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

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

32 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	Manual Kauers
Place of Publication	New York
Publisher	ACM
Pages	125-132
Number of pages	8
ISBN (Print)	9781450320597
DOIs	https://doi.org/10.1145/2465506.2465516
Publication status	Published - 2013
Externally published	Yes
Event	38th International Symposium on Symbolic and Algebraic Computation, ISSAC 2013 - Boston, United States Duration: 26 Jun 2013 → 29 Jun 2013

Conference

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

Keywords

Cylindrical algebraic decomposition
Equational constraint

ASJC Scopus subject areas

Mathematics(all)

Access to Document

10.1145/2465506.2465516

Cite this

Cylindrical algebraic decompositions for boolean combinations. / Bradford, Russell; Davenport, James H.; England, Matthew et al.
ISSAC 2013 - Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation. ed. / Manual Kauers. New York: ACM, 2013. p. 125-132.

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

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. ACM, New York, pp. 125-132, 38th International Symposium on Symbolic and Algebraic Computation, ISSAC 2013, Boston, Massachusetts, United States, 26/06/13. https://doi.org/10.1145/2465506.2465516

@inproceedings{551a6fa1df474692913c7714085ba037,

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

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

editor = "Manual Kauers",

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

publisher = "ACM",

address = "United States",

note = "38th International Symposium on Symbolic and Algebraic Computation, ISSAC 2013 ; Conference date: 26-06-2013 Through 29-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 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.

KW - Cylindrical algebraic decomposition

KW - Equational constraint

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

U2 - 10.1145/2465506.2465516

DO - 10.1145/2465506.2465516

M3 - Conference proceeding

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

PB - ACM

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

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this