Levelwise construction of a single cylindrical algebraic cell
From MaRDI portal
(Redirected from Publication:6149151)
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.
Cites work
- scientific article; zbMATH DE number 575960 (Why is no real title available?)
- scientific article; zbMATH DE number 589124 (Why is no real title available?)
- scientific article; zbMATH DE number 1157650 (Why is no real title available?)
- scientific article; zbMATH DE number 1157658 (Why is no real title available?)
- scientific article; zbMATH DE number 3053259 (Why is no real title available?)
- A model-constructing satisfiability calculus
- Applying machine learning to heuristics for real polynomial constraint solving
- Constructing a single cell in cylindrical algebraic decomposition
- Constructing a single open cell in a cylindrical algebraic decomposition
- Curtains in CAD: Why Are They a Problem and How Do We Fix Them?
- Cylindrical algebraic decomposition with equational constraints
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- Enhancements to Lazard's method for cylindrical algebraic decomposition
- Flexible proof production in an industrial-strength SMT solver
- Improved projection for cylindrical algebraic decomposition
- Invariant checking of NRA transition systems via incremental reduction to LRA with EUF
- On using Lazard's projection in CAD construction
- Open non-uniform cylindrical algebraic decompositions
- Optimizations of the subresultant algorithm
- Partial cylindrical algebraic decomposition for quantifier elimination
- Projection and Quantifier Elimination Using Non-uniform Cylindrical Algebraic Decomposition
- Quantifier elimination and cylindrical algebraic decomposition. Proceedings of a symposium, Linz, Austria, October 6--8, 1993
- Real quantifier elimination is doubly exponential
- Solving non-linear arithmetic
- Solving nonlinear integer arithmetic with MCSAT
- Truth table invariant cylindrical algebraic decomposition
- Validity proof of Lazard's method for CAD construction
- \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
Cited in
(3)
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)
