Towards Incremental Cylindrical Algebraic Decomposition in Maple

Alexander Cowen-Rivers, Matthew England

Research output: Chapter in Book/Report/Conference proceedingConference proceeding

11 Downloads (Pure)

Abstract

Cylindrical Algebraic Decomposition (CAD) is an important tool within computational real algebraic geometry, capable of solving many problems for polynomial systems over the reals. It has long been studied by the Symbolic Computation community and has found recent interest in the Satisfiability Checking community. The present report describes a proof of concept implementation of an Incremental CAD algorithm in Maple, where CADs are built and then refined as additional polynomial constraints are added. The aim is to make CAD suitable for use as a theory solver for SMT tools who search for solutions by continually reformulating logical formula and querying whether a logical solution is admissible. We describe experiments for the proof of concept, which clearly display the computational advantages compared to iterated re-computation. In addition, the project implemented this work under the recently verified Lazard projection scheme (with corresponding Lazard valuation).
Original languageEnglish
Title of host publicationProceedings of the 3rd International Workshop on Satisfiability Checking and Symbolic Computation
Subtitle of host publicationSC-Square 2018
PublisherCEUR Workshop Proceedings
Pages3-18
Number of pages16
Volume2189
Publication statusPublished - 1 Sep 2018
Event3rd International Workshop on Satisfiability Checking and Symbolic Computation - University of Oxford, Oxford, United Kingdom
Duration: 11 Jul 201811 Jul 2018
Conference number: 3
http://www.sc-square.org/CSA/workshop3.html

Workshop

Workshop3rd International Workshop on Satisfiability Checking and Symbolic Computation
Abbreviated titleSC-Square 2018
CountryUnited Kingdom
CityOxford
Period11/07/1811/07/18
Internet address

Fingerprint

Decomposition
Polynomials
Surface mount technology
Computer aided design
Geometry
Experiments

Bibliographical note

CEUR Workshop Proceedings (CEUR-WS.org) is a free open-access publication service at Sun SITE Central Europe operated under the umbrella of RWTH Aachen University. CEUR-WS.org is a recognized ISSN publication series, ISSN 1613-0073.

Cite this

Cowen-Rivers, A., & England, M. (2018). Towards Incremental Cylindrical Algebraic Decomposition in Maple. In Proceedings of the 3rd International Workshop on Satisfiability Checking and Symbolic Computation: SC-Square 2018 (Vol. 2189, pp. 3-18). CEUR Workshop Proceedings.

Towards Incremental Cylindrical Algebraic Decomposition in Maple. / Cowen-Rivers, Alexander; England, Matthew.

Proceedings of the 3rd International Workshop on Satisfiability Checking and Symbolic Computation: SC-Square 2018. Vol. 2189 CEUR Workshop Proceedings, 2018. p. 3-18.

Research output: Chapter in Book/Report/Conference proceedingConference proceeding

Cowen-Rivers, A & England, M 2018, Towards Incremental Cylindrical Algebraic Decomposition in Maple. in Proceedings of the 3rd International Workshop on Satisfiability Checking and Symbolic Computation: SC-Square 2018. vol. 2189, CEUR Workshop Proceedings, pp. 3-18, 3rd International Workshop on Satisfiability Checking and Symbolic Computation, Oxford, United Kingdom, 11/07/18.
Cowen-Rivers A, England M. Towards Incremental Cylindrical Algebraic Decomposition in Maple. In Proceedings of the 3rd International Workshop on Satisfiability Checking and Symbolic Computation: SC-Square 2018. Vol. 2189. CEUR Workshop Proceedings. 2018. p. 3-18
Cowen-Rivers, Alexander ; England, Matthew. / Towards Incremental Cylindrical Algebraic Decomposition in Maple. Proceedings of the 3rd International Workshop on Satisfiability Checking and Symbolic Computation: SC-Square 2018. Vol. 2189 CEUR Workshop Proceedings, 2018. pp. 3-18
@inproceedings{fa1f1c9274594b99ae50531986418fd9,
title = "Towards Incremental Cylindrical Algebraic Decomposition in Maple",
abstract = "Cylindrical Algebraic Decomposition (CAD) is an important tool within computational real algebraic geometry, capable of solving many problems for polynomial systems over the reals. It has long been studied by the Symbolic Computation community and has found recent interest in the Satisfiability Checking community. The present report describes a proof of concept implementation of an Incremental CAD algorithm in Maple, where CADs are built and then refined as additional polynomial constraints are added. The aim is to make CAD suitable for use as a theory solver for SMT tools who search for solutions by continually reformulating logical formula and querying whether a logical solution is admissible. We describe experiments for the proof of concept, which clearly display the computational advantages compared to iterated re-computation. In addition, the project implemented this work under the recently verified Lazard projection scheme (with corresponding Lazard valuation).",
author = "Alexander Cowen-Rivers and Matthew England",
note = "CEUR Workshop Proceedings (CEUR-WS.org) is a free open-access publication service at Sun SITE Central Europe operated under the umbrella of RWTH Aachen University. CEUR-WS.org is a recognized ISSN publication series, ISSN 1613-0073.",
year = "2018",
month = "9",
day = "1",
language = "English",
volume = "2189",
pages = "3--18",
booktitle = "Proceedings of the 3rd International Workshop on Satisfiability Checking and Symbolic Computation",
publisher = "CEUR Workshop Proceedings",

}

TY - GEN

T1 - Towards Incremental Cylindrical Algebraic Decomposition in Maple

AU - Cowen-Rivers, Alexander

AU - England, Matthew

N1 - CEUR Workshop Proceedings (CEUR-WS.org) is a free open-access publication service at Sun SITE Central Europe operated under the umbrella of RWTH Aachen University. CEUR-WS.org is a recognized ISSN publication series, ISSN 1613-0073.

PY - 2018/9/1

Y1 - 2018/9/1

N2 - Cylindrical Algebraic Decomposition (CAD) is an important tool within computational real algebraic geometry, capable of solving many problems for polynomial systems over the reals. It has long been studied by the Symbolic Computation community and has found recent interest in the Satisfiability Checking community. The present report describes a proof of concept implementation of an Incremental CAD algorithm in Maple, where CADs are built and then refined as additional polynomial constraints are added. The aim is to make CAD suitable for use as a theory solver for SMT tools who search for solutions by continually reformulating logical formula and querying whether a logical solution is admissible. We describe experiments for the proof of concept, which clearly display the computational advantages compared to iterated re-computation. In addition, the project implemented this work under the recently verified Lazard projection scheme (with corresponding Lazard valuation).

AB - Cylindrical Algebraic Decomposition (CAD) is an important tool within computational real algebraic geometry, capable of solving many problems for polynomial systems over the reals. It has long been studied by the Symbolic Computation community and has found recent interest in the Satisfiability Checking community. The present report describes a proof of concept implementation of an Incremental CAD algorithm in Maple, where CADs are built and then refined as additional polynomial constraints are added. The aim is to make CAD suitable for use as a theory solver for SMT tools who search for solutions by continually reformulating logical formula and querying whether a logical solution is admissible. We describe experiments for the proof of concept, which clearly display the computational advantages compared to iterated re-computation. In addition, the project implemented this work under the recently verified Lazard projection scheme (with corresponding Lazard valuation).

M3 - Conference proceeding

VL - 2189

SP - 3

EP - 18

BT - Proceedings of the 3rd International Workshop on Satisfiability Checking and Symbolic Computation

PB - CEUR Workshop Proceedings

ER -