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).
|Title of host publication||Proceedings of the 3rd International Workshop on Satisfiability Checking and Symbolic Computation|
|Subtitle of host publication||SC-Square 2018|
|Publisher||CEUR Workshop Proceedings|
|Number of pages||16|
|Publication status||Published - 1 Sep 2018|
|Event||3rd International Workshop on Satisfiability Checking and Symbolic Computation - University of Oxford, Oxford, United Kingdom|
Duration: 11 Jul 2018 → 11 Jul 2018
Conference number: 3
|Workshop||3rd International Workshop on Satisfiability Checking and Symbolic Computation|
|Abbreviated title||SC-Square 2018|
|Period||11/07/18 → 11/07/18|
Bibliographical noteCEUR 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.
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.