Projective Delineability for Single Cell Construction

TL;DR

This paper introduces a new approach called projective delineability for single cell construction in CAD algorithms, aiming to reduce computational effort while maintaining correctness, supported by experimental results.

Contribution

It adapts single cell construction to utilize projective delineability, a weaker property that can lower computational costs in CAD-based algorithms.

Findings

Projective delineability can be effectively exploited in single cell construction.

Experimental results show potential computational savings.

The approach maintains correctness while reducing complexity.

Abstract

The cylindrical algebraic decomposition (CAD) is the only complete method used in practice for solving problems like quantifier elimination or SMT solving related to real algebra, despite its doubly exponential complexity. Recent exploration-guided algorithms like NLSAT, NuCAD, and CAlC rely on CAD technology but reduce the computational effort heuristically. Single cell construction is a paradigm that is used in each of these algorithms. The central property on which the CAD algorithm is based is called delineability. Recently, we introduced a weaker notion called projective delineability which can require fewer computations to guarantee, but needs to be applied carefully. This paper adapts the single cell construction for exploiting projective delineability and reports on experimental results.