Towards Incremental Cylindrical Algebraic Decomposition in Maple

Authors: Alexander Cowen-Rivers and Matthew England

Paper Information

Title:Towards Incremental Cylindrical Algebraic Decomposition in Maple
Authors:Alexander Cowen-Rivers and Matthew England
Proceedings:SCSC Papers
Editors: Anna Maria Bigatti and Martin Brain
Keywords:Cylindrical Algebraic Decomposition, SMT, Incremental

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 \textsc{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 constantly 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).

Talk:Jul 11 14:30 (Session 66D: Research papers: CAD)