Bi-Weekly Talk: Jasper Nalbach: Levelwise construction of a single cylindrical algebraic cell

Wednesday, April 13, 2022, 10:30am

Location: Online session

Speaker: Jasper Nalbach

 

Abstract: 

Satisfiability modulo theories (SMT) solving is a technique for checking the satisfiability of quantifier-free first-order logic formulas over different theories. We consider the theory of non-linear real arithmetic where the formulae are logical combinations of polynomial constraints. The most commonly used decision procedure is the cylindrical algebraic decomposition (CAD) which has doubly exponential complexity (in the number of real variables). It works through a projection and lifting framework, where the projection tracks the resultants, discriminants and coefficients of all polynomials involved.

A CAD encodes more information than necessary for checking satisfiability. Hence there has been the recent development of sample-based algorithms which reduce the computational effort in CAD by guessing samples and generalizing conflicts by constructing truth-invariant cells around conflicting samples. The most notable example of this is the NLSAT algorithm, an instantiation of the model-constructing satisfiability calculus (MCSAT).
Conflict generalization improves on CAD by reducing the number of polynomials to project, and reducing the projection itself based on the sample for the conflict. The original NLSAT only reduces the number of coefficients tracked in projection, but it was followed by the single cell construction which reduces further the number of resultants and discriminants used. This construction involved refining a cell iteratively, polynomial by polynomial, meaning the shape and size of the resulting cell depends on the order in which the polynomials are considered.

We further develop these ideas by employing a levelwise approach to cell construction, so called as the cell is built level by level according to a variable ordering, rather than incrementally refined according to a polynomial ordering. We still use a reduced number of projection polynomials based on the sample being generalised, but we consider at once all the possibilities for these at a given level allowing for the use of heuristics to select the polynomials used to try and optimise on the shape of the cell.