A Variant of Non-uniform Cylindrical Algebraic Decomposition for Real Quantifier Elimination

TL;DR

This paper introduces a new variant of NuCAD, an adaptation of CAD, for real quantifier elimination and SMT solving, with an implementation and experimental comparison to CAlC.

Contribution

We develop and implement a novel variant of NuCAD for quantifier elimination and SMT solving, expanding its applicability and providing empirical evaluation.

Findings

The new NuCAD variant is effective for quantifier elimination.

Experimental results compare NuCAD to CAlC.

Implementation demonstrates practical viability.

Abstract

The Cylindrical Algebraic Decomposition (CAD) method is currently the only complete algorithm used in practice for solving real-algebraic problems. To ameliorate its doubly-exponential complexity, different exploration-guided adaptations try to avoid some of the computations. The first such adaptation named NLSAT was followed by Non-uniform CAD (NuCAD) and the Cylindrical Algebraic Covering (CAlC). Both NLSAT and CAlC have been developed and implemented in SMT solvers for satisfiability checking, and CAlC was recently also adapted for quantifier elimination. However, NuCAD was designed for quantifier elimination only, and no complete implementation existed before this work. In this paper, we present a novel variant of NuCAD for both real quantifier elimination and SMT solving, provide an implementation, and evaluate the method by experimentally comparing it to CAlC.