Projective Delineability for Single Cell Construction.

Jasper  Nalbach; Lucas  Michel; Erika Ábrahám; Christopher W. Brown; James H. Davenport; Matthew England; Pierre Mathonet; Naïm Zénaïdi

Projective Delineability for Single Cell Construction.

Jasper Nalbach, Lucas Michel, Erika Ábrahám, Christopher W. Brown, James H. Davenport, Matthew England, Pierre Mathonet, Naïm Zénaïdi

Research Centre for Fluid and Complex Systems

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding › peer-review

2 Downloads (Pure)

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.

Original language	English
Title of host publication	Proceedings of the 10th International Workshop on Satisfiability Checking and Symbolic Computation (SC2 '25)
Publisher	CEUR Workshop Proceedings
Number of pages	13
Publication status	Accepted/In press - 13 Jun 2025
Event	10th International Workshop on Satisfiability Checking and Symbolic Computation - Stuttgart, Germany Duration: 2 Aug 2025 → 2 Aug 2025

Conference

Conference	10th International Workshop on Satisfiability Checking and Symbolic Computation
Country/Territory	Germany
City	Stuttgart
Period	2/08/25 → 2/08/25

Access to Document

NMABDEMZ25-ArxivAccepted author manuscript, 2.23 MBLicence: CC BY

Cite this

Nalbach, J, Michel, L, Ábrahám, E, Brown, CW, Davenport, JH, England, M, Mathonet, P & Zénaïdi, N 2025, Projective Delineability for Single Cell Construction. in Proceedings of the 10th International Workshop on Satisfiability Checking and Symbolic Computation (SC2 '25). CEUR Workshop Proceedings, 10th International Workshop on Satisfiability Checking and Symbolic Computation, Stuttgart, Germany, 2/08/25.

@inproceedings{817cd363ec1a4822a5d579f79673fc6b,

title = "Projective Delineability for Single Cell Construction.",

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.",

author = "Jasper Nalbach and Lucas Michel and Erika {\'A}brah{\'a}m and Brown, \{Christopher W.\} and Davenport, \{James H.\} and Matthew England and Pierre Mathonet and Na{\"i}m Z{\'e}na{\"i}di",

year = "2025",

month = jun,

day = "13",

language = "English",

booktitle = "Proceedings of the 10th International Workshop on Satisfiability Checking and Symbolic Computation (SC2 '25)",

publisher = "CEUR Workshop Proceedings",

address = "Germany",

note = "10th International Workshop on Satisfiability Checking and Symbolic Computation ; Conference date: 02-08-2025 Through 02-08-2025",

}

TY - GEN

T1 - Projective Delineability for Single Cell Construction.

AU - Nalbach, Jasper

AU - Michel, Lucas

AU - Ábrahám, Erika

AU - Brown, Christopher W.

AU - Davenport, James H.

AU - England, Matthew

AU - Mathonet, Pierre

AU - Zénaïdi, Naïm

PY - 2025/6/13

Y1 - 2025/6/13

N2 - 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.

AB - 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.

M3 - Conference proceeding

BT - Proceedings of the 10th International Workshop on Satisfiability Checking and Symbolic Computation (SC2 '25)

PB - CEUR Workshop Proceedings

T2 - 10th International Workshop on Satisfiability Checking and Symbolic Computation

Y2 - 2 August 2025 through 2 August 2025

ER -

Projective Delineability for Single Cell Construction.

Abstract

Conference

Access to Document

Fingerprint

Cite this