Levelwise construction of a single cylindrical algebraic cell

Jasper Nalbach, Erika Abraham, Philippe Specht, Christopher W. Brown, James H. Davenport, Matthew England

Research output: Contribution to journalArticlepeer-review

44 Downloads (Pure)

Abstract

Satisfiability modulo theories (SMT) solvers check the satisfiability of quantifier-free first-order logic formulae over different theories. 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 the real space into cells where the constraints are truth-invariant through the use of projection polynomials.
A CAD encodes more information than necessary for checking satisfiability. One approach to address this 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. This can lead to a satisfying assignment more quickly, or conclude unsatisfiability with far fewer cells. A notable example of this approach is Jovanović and de Moura's NLSAT algorithm. Since these cells are being produced locally to a sample there is scope to use 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, it refines a cell polynomial-by-polynomial, meaning the shape and size of the cell produced depends on the order in which the polynomials are considered.
The present paper proposes a method to construct such cells levelwise, i.e. built level-by-level according to a variable ordering instead of polynomial-by-polynomial for all levels. 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 optimize the shape of the cell under construction. The new method can thus improve the performance of the NLSAT algorithm. We formulate all the necessary theory that underpins the algorithm as a proof system: while not a common presentation for work in this field, it is valuable in allowing an elegant decoupling of heuristic decisions from the main algorithm and its proof of correctness. We expect the symbolic computation community may find uses for it in other areas too. In particular, the proof system could be a step towards formal proofs for non-linear real arithmetic.
This work has been implemented in the SMT-RAT solver and the benefits of the levelwise construction are validated experimentally on the SMT-LIB benchmark library. We also compare several heuristics for the construction and observe that each heuristic has strengths offering potential for further exploitation of the new approach.
Original languageEnglish
Article number102288
Number of pages44
JournalJournal of Symbolic Computation
Volume123
Early online date5 Dec 2023
DOIs
Publication statusE-pub ahead of print - 5 Dec 2023

Bibliographical note

This is an open access article distributed under the terms of the Creative Commons CC-BY license, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.

Funder

Jasper Nalbach was supported by the DFG RTG 2236 UnRAVeL. James Davenport and Matthew England were supported by the EPSRC DEWCAD Project, Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition (grant references EP/T015748/1 and EP/T015713/1).

Keywords

  • Satisfiability modulo theories
  • Cylindrical algebraic decomposition
  • Non-linear real arithmetic
  • Model-constructing satisfiability calculus
  • Formal proofs

Fingerprint

Dive into the research topics of 'Levelwise construction of a single cylindrical algebraic cell'. Together they form a unique fingerprint.

Cite this