Truth table invariant cylindrical algebraic decomposition

R. Bradford, J. H. Davenport, Matthew England, S. McCallum, D. Wilson

Research output: Contribution to journalArticle

19 Citations (Scopus)
24 Downloads (Pure)

Abstract

When using cylindrical algebraic decomposition (CAD) to solve a problem with respect to a set of polynomials, it is likely not the signs of those polynomials that are of paramount importance but rather the truth values of certain quantifier free formulae involving them. This observation motivates our article and definition of a Truth Table Invariant CAD (TTICAD). In ISSAC 2013 the current authors presented an algorithm that can efficiently and directly construct a TTICAD for a list of formulae in which each has an equational constraint. This was achieved by generalising McCallum's theory of reduced projection operators. In this paper we present an extended version of our theory which can be applied to an arbitrary list of formulae, achieving savings if at least one has an equational constraint. We also explain how the theory of reduced projection operators can allow for further improvements to the lifting phase of CAD algorithms, even in the context of a single equational constraint. The algorithm is implemented fully in Maple and we present both promising results from experimentation and a complexity analysis showing the benefits of our contributions.
Original languageEnglish
Pages (from-to)1-35
JournalJournal of Symbolic Computation
Volume76
Early online date4 Nov 2016
DOIs
Publication statusPublished - 2016

Fingerprint

Truth table
Projection Operator
Decomposition
Decompose
Invariant
Polynomials
Polynomial
Complexity Analysis
Maple
Decomposition Algorithm
Quantifiers
Experimentation
Computer aided design
Likely
Arbitrary

Bibliographical note

Open Access funded by Engineering and Physical Sciences Research Council
Under a Creative Commons license

Keywords

  • Cylindrical algebraic decomposition
  • Equational constraint

Cite this

Truth table invariant cylindrical algebraic decomposition. / Bradford, R.; Davenport, J. H.; England, Matthew; McCallum, S.; Wilson, D.

In: Journal of Symbolic Computation, Vol. 76, 2016, p. 1-35.

Research output: Contribution to journalArticle

Bradford, R. ; Davenport, J. H. ; England, Matthew ; McCallum, S. ; Wilson, D. / Truth table invariant cylindrical algebraic decomposition. In: Journal of Symbolic Computation. 2016 ; Vol. 76. pp. 1-35.
@article{9239543155194834a9c972257fe0ab43,
title = "Truth table invariant cylindrical algebraic decomposition",
abstract = "When using cylindrical algebraic decomposition (CAD) to solve a problem with respect to a set of polynomials, it is likely not the signs of those polynomials that are of paramount importance but rather the truth values of certain quantifier free formulae involving them. This observation motivates our article and definition of a Truth Table Invariant CAD (TTICAD). In ISSAC 2013 the current authors presented an algorithm that can efficiently and directly construct a TTICAD for a list of formulae in which each has an equational constraint. This was achieved by generalising McCallum's theory of reduced projection operators. In this paper we present an extended version of our theory which can be applied to an arbitrary list of formulae, achieving savings if at least one has an equational constraint. We also explain how the theory of reduced projection operators can allow for further improvements to the lifting phase of CAD algorithms, even in the context of a single equational constraint. The algorithm is implemented fully in Maple and we present both promising results from experimentation and a complexity analysis showing the benefits of our contributions.",
keywords = "Cylindrical algebraic decomposition, Equational constraint",
author = "R. Bradford and Davenport, {J. H.} and Matthew England and S. McCallum and D. Wilson",
note = "Open Access funded by Engineering and Physical Sciences Research Council Under a Creative Commons license",
year = "2016",
doi = "10.1016/j.jsc.2015.11.002",
language = "English",
volume = "76",
pages = "1--35",
journal = "Journal of Symbolic Computation",
issn = "0747-7171",
publisher = "Elsevier",

}

TY - JOUR

T1 - Truth table invariant cylindrical algebraic decomposition

AU - Bradford, R.

AU - Davenport, J. H.

AU - England, Matthew

AU - McCallum, S.

AU - Wilson, D.

N1 - Open Access funded by Engineering and Physical Sciences Research Council Under a Creative Commons license

PY - 2016

Y1 - 2016

N2 - When using cylindrical algebraic decomposition (CAD) to solve a problem with respect to a set of polynomials, it is likely not the signs of those polynomials that are of paramount importance but rather the truth values of certain quantifier free formulae involving them. This observation motivates our article and definition of a Truth Table Invariant CAD (TTICAD). In ISSAC 2013 the current authors presented an algorithm that can efficiently and directly construct a TTICAD for a list of formulae in which each has an equational constraint. This was achieved by generalising McCallum's theory of reduced projection operators. In this paper we present an extended version of our theory which can be applied to an arbitrary list of formulae, achieving savings if at least one has an equational constraint. We also explain how the theory of reduced projection operators can allow for further improvements to the lifting phase of CAD algorithms, even in the context of a single equational constraint. The algorithm is implemented fully in Maple and we present both promising results from experimentation and a complexity analysis showing the benefits of our contributions.

AB - When using cylindrical algebraic decomposition (CAD) to solve a problem with respect to a set of polynomials, it is likely not the signs of those polynomials that are of paramount importance but rather the truth values of certain quantifier free formulae involving them. This observation motivates our article and definition of a Truth Table Invariant CAD (TTICAD). In ISSAC 2013 the current authors presented an algorithm that can efficiently and directly construct a TTICAD for a list of formulae in which each has an equational constraint. This was achieved by generalising McCallum's theory of reduced projection operators. In this paper we present an extended version of our theory which can be applied to an arbitrary list of formulae, achieving savings if at least one has an equational constraint. We also explain how the theory of reduced projection operators can allow for further improvements to the lifting phase of CAD algorithms, even in the context of a single equational constraint. The algorithm is implemented fully in Maple and we present both promising results from experimentation and a complexity analysis showing the benefits of our contributions.

KW - Cylindrical algebraic decomposition

KW - Equational constraint

U2 - 10.1016/j.jsc.2015.11.002

DO - 10.1016/j.jsc.2015.11.002

M3 - Article

VL - 76

SP - 1

EP - 35

JO - Journal of Symbolic Computation

JF - Journal of Symbolic Computation

SN - 0747-7171

ER -