Satisfiability Modulo Theories (SMT) solvers check the satisfiability of quantifier-free first-order logic formulas. We consider the theory of non-linear real arithmetic where the formulae are logical combinations of polynomial constraints. Here a commonly used tool is the Cylindrical Algebraic Decomposition (CAD) to decompose real space into cells where the constraints are truth-invariant through the use of projection polynomials. An improved approach is to repackage the CAD theory into a search-based algorithm: one that guesses sample points to satisfy the formula, and generalizes guesses that conflict constraints to cylindrical cells around samples which are avoided in the continuing search. Such an approach can lead to a satisfying assignment more quickly, or conclude unsatisfiability with fewer cells. A notable example of this approach is Jovanovi\'c and de Moura's NLSAT algorithm. Since these cells are produced locally to a sample we might need fewer projection polynomials than the traditional CAD projection. The original NLSAT algorithm reduced the set a little; while Brown's single cell construction reduced it much further still. However, the shape and size of the cell produced depends on the order in which the polynomials are considered. This paper proposes a method to construct such cells levelwise, i.e. built level-by-level according to a variable ordering. We still use a reduced number of projection polynomials, but can now consider a variety of different reductions and use heuristics to select the projection polynomials in order to optimise the shape of the cell under construction. We formulate all the necessary theory as a proof system: while not a common presentation for work in this field, it allows an elegant decoupling of heuristics from the algorithm and its proof of correctness.

翻译：可满足性模理论（SMT）求解器用于检验无量词一阶逻辑公式的可满足性。本文考虑非线性实数算术理论，其中公式由多项式约束的逻辑组合构成。此类问题中常用柱形代数分解（CAD）将实空间分解为单元，通过投影多项式确保约束在这些单元内保持真值不变性。一种改进方法是将CAD理论重构为基于搜索的算法：通过猜测采样点来满足公式，并将与冲突约束相关的猜测泛化为采样点周围的柱形单元，在后续搜索中避开这些单元。此类方法能更快生成可满足赋值，或通过更少的单元判定不可满足性。该方法的典型代表是Jovanović与de Moura提出的NLSAT算法。由于这些单元仅围绕采样点局部生成，所需投影多项式可能少于传统CAD投影。原始NLSAT算法对多项式集合进行了适度缩减，而Brown的单单元构造方法进一步大幅缩减了该集合。然而，所生成单元的形状与尺寸取决于多项式被考虑的顺序。本文提出一种层级式构造方法，即根据变量序逐层构建单元。该方法仍采用缩减后的投影多项式集合，但可考虑多种不同的缩减策略，并通过启发式方法选择投影多项式以优化构造中单元的形状。我们将所有必要理论构建为证明系统：虽非该领域常见呈现方式，但能优雅地将启发式方法从算法及其正确性证明中解耦。