Summer Research Report: Towards Incremental Lazard Cylindrical Algebraic Decomposition

TL;DR

This paper presents a proof of concept for an incremental CAD algorithm implemented in Maple, which refines solutions polynomially and offers computational advantages, especially for SMT-solvers, using Lazard's minimal complete CAD scheme.

Contribution

It introduces the first documented implementation of an incremental CAD algorithm with Lazard projection, enhancing efficiency for logical formula reformulation in SMT-solving.

Findings

Incremental CAD shows computational advantages over re-computation.

Implementation demonstrates the feasibility of Lazard projection in CAD.

Proof of concept supports potential integration with SMT-solvers.

Abstract

Cylindrical Algebraic Decomposition (CAD) is an important tool within computational real algebraic geometry, capable of solving many problems to do with polynomial systems over the reals, but known to have worst-case computational complexity doubly exponential in the number of variables. It has long been studied by the Symbolic Computation community and is implemented in a variety of computer algebra systems, however, it has also found recent interest in the Satisfiability Checking community for use with SMT-solvers. The SCSC Project seeks to build bridges between these communities. The present report describes progress made during a Research Internship in Summer 2017 funded by the EU H2020 SCSC CSA. We describe a proof of concept implementation of an Incremental CAD algorithm in Maple, where CADs are built and refined incrementally by polynomial constraint, in contrast to the usual approach of a single computation from a single input. This advance would make CAD of use to SMT-solvers who search for solutions by constantly reformulating logical formula and querying solvers like CAD for whether a logical solution is admissible. We describe experiments for the proof of concept, which clearly display the computational advantages when compared to iterated re-computation. In addition, the project implemented this work under the recently verified Lazard projection scheme (with corresponding Lazard evaluation). That is the minimal complete CAD method in theory, and this is the first documented implementation.