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.
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 language | English |
|---|---|
| Pages (from-to) | 38-71 |
| Number of pages | 34 |
| Journal | Journal of Symbolic Computation |
| Volume | 100 |
| Early online date | 26 Jul 2019 |
| DOIs | |
| Publication status | Published - 1 Sept 2020 |
Bibliographical note
NOTICE: this is the author’s version of a work that was accepted for publication in Journal of Symbolic Computation. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in Journal of Symbolic Computation, 100, (2020)DOI: 10.1016/j.jsc.2019.07.019
© 2020, Elsevier. Licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International http://creativecommons.org/licenses/by-nc-nd/4.0/
Funder
This work was originally supported by EPSRC grant EP/J003247/1 and later by EU H2020-FETOPEN-2016-2017-CSA project SC 2 ( 712689).Funding
| Funders | Funder number |
|---|---|
| European Horizon 2020 | 712689 |
| Engineering and Physical Sciences Research Council | EP/J003247/1 |
| China Aerospace Science and Technology Corporation |
Keywords
- cylindrical algebraic decomposition
- non linear real arithmetic
- symbolic computation
- computer algebra
- equational constraint
