Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Levelwise construction of a single cylindrical algebraic cell

Jasper Nalbach, Erika Ábrahám, Philippe Specht, Christopher W. Brown, James H. Davenport, Matthew England

TL;DR

This work tackles the computational difficulty of satisfiability checking in non-linear real arithmetic by refining the cylindrical algebraic decomposition (CAD) approach through a levelwise, single-cell construction. It formalizes a proof system that decouples heuristic decisions from correctness, and introduces an algorithm that builds a single algebraic cell level-by-level according to a fixed variable ordering, guided by root-ordering and equational-constraint projections. The approach aims to preserve sign- and order-invariance while allowing flexible heuristics to shape the cell, thereby reducing projection work and potentially accelerating SMT-solvers like MCSAT in practice. Experimental results within SMT-RAT show that levelwise single-cell backends can be competitive and orthogonal to existing backends, with potential for certification and extension to complete projection frameworks such as Lazard projection.

Abstract

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

Levelwise construction of a single cylindrical algebraic cell

TL;DR

This work tackles the computational difficulty of satisfiability checking in non-linear real arithmetic by refining the cylindrical algebraic decomposition (CAD) approach through a levelwise, single-cell construction. It formalizes a proof system that decouples heuristic decisions from correctness, and introduces an algorithm that builds a single algebraic cell level-by-level according to a fixed variable ordering, guided by root-ordering and equational-constraint projections. The approach aims to preserve sign- and order-invariance while allowing flexible heuristics to shape the cell, thereby reducing projection work and potentially accelerating SMT-solvers like MCSAT in practice. Experimental results within SMT-RAT show that levelwise single-cell backends can be competitive and orthogonal to existing backends, with potential for certification and extension to complete projection frameworks such as Lazard projection.

Abstract

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ć 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.
Paper Structure (55 sections, 16 theorems, 46 equations, 16 figures, 4 tables, 3 algorithms)

This paper contains 55 sections, 16 theorems, 46 equations, 16 figures, 4 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Non-linear real arithmetic and CAD
  3. NLSAT, MCSAT and single cylindrical cells
  4. First contribution: Proof system presentation
  5. Second contribution: Levelwise single cells
  6. Plan of the paper
  7. Preliminaries
  8. Variables and polynomials
  9. Real algebraic numbers, constraints and cells
  10. CAD definition
  11. McCallum's projection operator
  12. Computing a CAD
  13. Single cell computation
  14. Previous work on optimizing single cell computations
  15. Our levelwise approach to single cell computation
  16. ...and 40 more sections

Key Result

Theorem 5.1

Let $P \subseteq \mathbb{Q}[x_1,\ldots,x_n]$, and $s \in \mathbb{R}^n$. The method $\texttt{single\_cell}$ (alg:single_cell) either returns a cell data structure $\texttt{R}$ such that all polynomials in $P$ are sign-invariant on $\textit{setOf}(\texttt{R})$ and $s \in \textit{setOf}(\texttt{R})$, o

Figures (16)

  • Figure 1: Refinement-based construction of a single cell for \ref{['ex:motivation']}. In the upper row the original cell (the entire plane) is refined first by polynomial $p_1$, then by $p_2$, then by $p_3$. In the lower row a different order of refinement is used: $p_3$, $p_2$, $p_1$ giving a larger cell. Note that in the figures of this paper we label the varieties of polynomials with their name, i.e. $p_1$ labels $p_1=0$.
  • Figure 2: Construction of a single cell for \ref{['ex:motivation']} following the new levelwise approach as described in \ref{['ex:motivation_cont']}.
  • Figure 3: Proof for \ref{['Ex61']} (slightly truncated, read in columns). $Q \dashv P_1, \ldots, P_k$ means that $Q$ is derived from $P_1, \ldots, P_k$.
  • Figure 4: Examples of the two cases of polynomials without roots at the projection $s_1$ of the sample $s=(s_1,s_2)$. Dashed lines denote cylinder boundaries over the projected cell.
  • Figure 5: Two examples for the property $\ref{['def:prop:irordering']}(\preceq,s)$.
  • ...and 11 more figures

Theorems & Definitions (55)

  • Definition 2.1: Delineability Collins1975
  • Definition 2.2: Nullification
  • Definition 2.3: Indexed root expression
  • Definition 2.4: Symbolic intervals, single cell and CAD data structures
  • Definition 2.5: Indexed root expressions of polynomials
  • Example 3.1
  • Example 3.2
  • Example 4.1
  • Definition 4.1: Property
  • Definition 4.2
  • ...and 45 more