Cylindrical Algebraic Decomposition with Equational Constraints

Matthew England, Russell Bradford, James H. Davenport

Research output: Contribution to journalArticle

8 Downloads (Pure)

Abstract

Cylindrical Algebraic Decomposition (CAD) has long been one of the most important algorithms within Symbolic Computation, as a tool to perform quantifier elimination in first order logic over the reals. More recently it is finding prominence in the Satisfiability Checking community as a tool to identify satisfying solutions of problems in nonlinear real arithmetic.

The original algorithm produces decompositions according to the signs of polynomials, when what is usually required is a decomposition according to the truth of a formula containing those polynomials. One approach to achieve that coarser (but hopefully cheaper) decomposition is to reduce the polynomials identified in the CAD to reflect a logical structure which reduces the solution space dimension: the presence of Equational Constraints (ECs).

This paper may act as a tutorial for the use of CAD with ECs: we describe all necessary background and the current state of the art. In particular, we present recent work on how McCallum's theory of reduced projection may be leveraged to make further savings in the lifting phase: both to the polynomials we lift with and the cells lifted over. We give a new complexity analysis to demonstrate that the double exponent in the worst case complexity bound for CAD reduces in line with the number of ECs. We show that the reduction can apply to both the number of polynomials produced and their degree.
Original languageEnglish
Pages (from-to)(In-Press)
Number of pages34
JournalJournal of Symbolic Computation
Volume(In-Press)
Early online date2 Aug 2019
DOIs
Publication statusE-pub ahead of print - 2 Aug 2019

Fingerprint

Decomposition
Decompose
Polynomials
Polynomial
Quantifier Elimination
Complexity Analysis
Symbolic Computation
Decomposition Algorithm
First-order Logic
Exponent
Projection
Necessary
Line
Cell
Demonstrate

Keywords

  • cylindrical algebraic decomposition
  • non linear real arithmetic
  • symbolic computation
  • computer algebra
  • equational constraint

Cite this

Cylindrical Algebraic Decomposition with Equational Constraints. / England, Matthew; Bradford, Russell; Davenport, James H.

In: Journal of Symbolic Computation, Vol. (In-Press), 02.08.2019, p. (In-Press).

Research output: Contribution to journalArticle

England, Matthew ; Bradford, Russell ; Davenport, James H. / Cylindrical Algebraic Decomposition with Equational Constraints. In: Journal of Symbolic Computation. 2019 ; Vol. (In-Press). pp. (In-Press).
@article{27a21f0f343844518b209424de765bba,
title = "Cylindrical Algebraic Decomposition with Equational Constraints",
abstract = "Cylindrical Algebraic Decomposition (CAD) has long been one of the most important algorithms within Symbolic Computation, as a tool to perform quantifier elimination in first order logic over the reals. More recently it is finding prominence in the Satisfiability Checking community as a tool to identify satisfying solutions of problems in nonlinear real arithmetic.The original algorithm produces decompositions according to the signs of polynomials, when what is usually required is a decomposition according to the truth of a formula containing those polynomials. One approach to achieve that coarser (but hopefully cheaper) decomposition is to reduce the polynomials identified in the CAD to reflect a logical structure which reduces the solution space dimension: the presence of Equational Constraints (ECs).This paper may act as a tutorial for the use of CAD with ECs: we describe all necessary background and the current state of the art. In particular, we present recent work on how McCallum's theory of reduced projection may be leveraged to make further savings in the lifting phase: both to the polynomials we lift with and the cells lifted over. We give a new complexity analysis to demonstrate that the double exponent in the worst case complexity bound for CAD reduces in line with the number of ECs. We show that the reduction can apply to both the number of polynomials produced and their degree.",
keywords = "cylindrical algebraic decomposition, non linear real arithmetic, symbolic computation, computer algebra, equational constraint",
author = "Matthew England and Russell Bradford and Davenport, {James H.}",
year = "2019",
month = "8",
day = "2",
doi = "10.1016/j.jsc.2019.07.019",
language = "English",
volume = "(In-Press)",
pages = "(In--Press)",
journal = "Journal of Symbolic Computation",
issn = "0747-7171",
publisher = "Elsevier",

}

TY - JOUR

T1 - Cylindrical Algebraic Decomposition with Equational Constraints

AU - England, Matthew

AU - Bradford, Russell

AU - Davenport, James H.

PY - 2019/8/2

Y1 - 2019/8/2

N2 - Cylindrical Algebraic Decomposition (CAD) has long been one of the most important algorithms within Symbolic Computation, as a tool to perform quantifier elimination in first order logic over the reals. More recently it is finding prominence in the Satisfiability Checking community as a tool to identify satisfying solutions of problems in nonlinear real arithmetic.The original algorithm produces decompositions according to the signs of polynomials, when what is usually required is a decomposition according to the truth of a formula containing those polynomials. One approach to achieve that coarser (but hopefully cheaper) decomposition is to reduce the polynomials identified in the CAD to reflect a logical structure which reduces the solution space dimension: the presence of Equational Constraints (ECs).This paper may act as a tutorial for the use of CAD with ECs: we describe all necessary background and the current state of the art. In particular, we present recent work on how McCallum's theory of reduced projection may be leveraged to make further savings in the lifting phase: both to the polynomials we lift with and the cells lifted over. We give a new complexity analysis to demonstrate that the double exponent in the worst case complexity bound for CAD reduces in line with the number of ECs. We show that the reduction can apply to both the number of polynomials produced and their degree.

AB - Cylindrical Algebraic Decomposition (CAD) has long been one of the most important algorithms within Symbolic Computation, as a tool to perform quantifier elimination in first order logic over the reals. More recently it is finding prominence in the Satisfiability Checking community as a tool to identify satisfying solutions of problems in nonlinear real arithmetic.The original algorithm produces decompositions according to the signs of polynomials, when what is usually required is a decomposition according to the truth of a formula containing those polynomials. One approach to achieve that coarser (but hopefully cheaper) decomposition is to reduce the polynomials identified in the CAD to reflect a logical structure which reduces the solution space dimension: the presence of Equational Constraints (ECs).This paper may act as a tutorial for the use of CAD with ECs: we describe all necessary background and the current state of the art. In particular, we present recent work on how McCallum's theory of reduced projection may be leveraged to make further savings in the lifting phase: both to the polynomials we lift with and the cells lifted over. We give a new complexity analysis to demonstrate that the double exponent in the worst case complexity bound for CAD reduces in line with the number of ECs. We show that the reduction can apply to both the number of polynomials produced and their degree.

KW - cylindrical algebraic decomposition

KW - non linear real arithmetic

KW - symbolic computation

KW - computer algebra

KW - equational constraint

U2 - 10.1016/j.jsc.2019.07.019

DO - 10.1016/j.jsc.2019.07.019

M3 - Article

VL - (In-Press)

SP - (In-Press)

JO - Journal of Symbolic Computation

JF - Journal of Symbolic Computation

SN - 0747-7171

ER -