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

  • 7 Citations

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

Fingerprint

Truth table
Decompose
Polynomial
Invariant
Maple
Quantifiers
Experimentation
Generalise
Truth
Class
Observation
Design

Keywords

  • cylindrical algebraic decomposition
  • equational constraint

Cite this

Bradford, R., Davenport, J. H., 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 (pp. 125-132). New York: Association for Computing Machinery. 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 '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 in Book/Report/Conference proceedingConference contribution

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
Bradford R, Davenport JH, England M, McCallum S, Wilson D. Cylindrical algebraic decompositions for Boolean combinations. In ISSAC '13: Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation. New York: Association for Computing Machinery. 2013. p. 125-132 https://doi.org/10.1145/2465506.2465516
Bradford, Russell ; Davenport, James H ; England, Matthew ; McCallum, Scott ; Wilson, David. / Cylindrical algebraic decompositions for Boolean combinations. ISSAC '13: Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation. New York : Association for Computing Machinery, 2013. pp. 125-132
@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",

}

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 - Conference contribution

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

ER -