标题： 单细胞构造的投影可判定性 显示英文标题

标题： Projective Delineability for Single Cell Construction

摘要： 圆柱代数分解（CAD）是目前在解决与实代数相关的量词消去或SMT求解等问题时唯一实际使用的完整方法，尽管其复杂度是双重指数级的。 最近的探索引导算法，如NLSAT、NuCAD和CAlC，依赖于CAD技术，但通过启发式方法减少计算量。 单细胞构造是一种在这些算法中均被使用的范式。 CAD算法所基于的核心特性称为可划分性。 最近，我们引入了一个较弱的概念，称为投影可划分性，它可能需要更少的计算来保证，但需要谨慎应用。 本文适应了单细胞构造以利用投影可划分性，并报告了实验结果。 显示英文摘要

摘要： 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.