Projective Delineability for Single Cell Construction

Pure (Coventry University)

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.

Authors 8

1. Jasper Nalbach Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Aachen , Germany

2. Lucas Michel

   University of Liège

   Affiliation as printed

   University of Liège , Liège , Belgium

3. Erika Ábrahám Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Aachen , Germany

4. Christopher W. Brown Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Aachen , Germany

5. James H. Davenport
6. Matthew England Aachen

   United States Naval Academy · RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Aachen , Germany

   United States Naval Academy , Annapolis , Maryland , USA

7. Pierre Mathonet Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Aachen , Germany

8. Naïm Zénaïdi Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Aachen , Germany