Projects per year
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 then 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 new contributions.
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 then 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 new contributions.
| Original language | English |
|---|---|
| Pages (from-to) | 1-35 |
| Number of pages | 35 |
| Journal | Journal of Symbolic Computation |
| Volume | 76 |
| Early online date | 4 Nov 2015 |
| DOIs | |
| Publication status | Published - 1 Sept 2016 |
Keywords
- cylindrical algebraic decomposition
- equational constraint
Fingerprint
Dive into the research topics of 'Truth table invariant cylindrical algebraic decomposition'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Real Geometry and Connectedness via Triangular Description
Davenport, J. (PI), Bradford, R. (CoI), England, M. (CoI) & Wilson, D. (CoI)
Engineering and Physical Sciences Research Council
1/10/11 → 31/12/15
Project: Research council
Profiles
-
James Davenport
- Department of Computer Science - Hebron and Medlock Professor of Information Technology
- International Centre for Higher Education Management (ICHEM)
- Institute of Coding
- UKRI CDT in Accountable, Responsible and Transparent AI
- Mathematical Foundations of Computation
Person: Research & Teaching
Datasets
-
Dataset supporting the paper: Truth table invariant cylindrical algebraic decomposition
Bradford, R. (Creator), Davenport, J. (Creator), England, M. (Creator), McCallum, S. (Creator) & Wilson, D. (Creator), University of Bath, 2015
DOI: 10.15125/BATH-00076
Dataset