Levelwise construction of a single cylindrical algebraic cell
From MaRDI portal
Publication:6149151
DOI10.1016/J.JSC.2023.102288arXiv2212.09309MaRDI QIDQ6149151FDOQ6149151
Matthew England, Jasper Nalbach, Christopher W. Brown, James H. Davenport, Erika Ábrahám, Philippe Specht
Publication date: 5 February 2024
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
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'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.
Full work available at URL: https://arxiv.org/abs/2212.09309
satisfiability modulo theoriescylindrical algebraic decompositionformal proofsnonlinear real arithmeticmodel-constructing satisfiability calculus
Cites Work
- SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
- Title not available (Why is that?)
- Partial cylindrical algebraic decomposition for quantifier elimination
- Quantifier elimination and cylindrical algebraic decomposition. Proceedings of a symposium, Linz, Austria, October 6--8, 1993
- Solving Non-linear Arithmetic
- A Model-Constructing Satisfiability Calculus
- Title not available (Why is that?)
- Improved projection for cylindrical algebraic decomposition
- Real quantifier elimination is doubly exponential
- Optimizations of the subresultant algorithm
- Title not available (Why is that?)
- Constructing a single open cell in a cylindrical algebraic decomposition
- Truth table invariant cylindrical algebraic decomposition
- Validity proof of Lazard's method for CAD construction
- Title not available (Why is that?)
- On using Lazard's projection in CAD construction
- Title not available (Why is that?)
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- Constructing a single cell in cylindrical algebraic decomposition
- Solving Nonlinear Integer Arithmetic with MCSAT
- Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
- Cylindrical algebraic decomposition with equational constraints
- Enhancements to Lazard's method for cylindrical algebraic decomposition
- Open non-uniform cylindrical algebraic decompositions
- Projection and Quantifier Elimination Using Non-uniform Cylindrical Algebraic Decomposition
- Flexible proof production in an industrial-strength SMT solver
- Applying Machine Learning to Heuristics for Real Polynomial Constraint Solving
- Curtains in CAD: Why Are They a Problem and How Do We Fix Them?
Cited In (2)
This page was built for publication: Levelwise construction of a single cylindrical algebraic cell
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6149151)
