Merging Adjacent Cells During Single Cell Construction

The cylindrical algebraic decomposition (CAD) is currently the only complete method used in practise for answering questions about real algebra, despite its doubly exponential complexity. Recently, some novel algorithms like NLSAT, CAlC and NuCAD for satisfiability checking respectively quantifier elimination have been proposed, which build on the CAD idea to generalize a sample point to a connected set (cell) of points that share certain properties with the sample. This process is called single cell construction. In this paper, we adapt this method to potentially generate bigger cells by detecting that certain adjacent cells maintain those relevant invariance properties. For formalizing the resulting algorithm in this paper, we generalize the notion of delineability to local delineability. An experimental evaluation of a first implementation in NLSAT is provided.