More is Less: Adding Polynomials for Faster Explanations in NLSAT
Valentin Promies, Jasper Nalbach, Erika Ábrahám, Paul Wagner
TL;DR
This work targets speeding up NLSAT's single cell construction for quantifier-free nonlinear real arithmetic by under-approximating cells through the dynamic introduction of linear polynomials. The authors propose apx-scc, which extends the projection set with auxiliary linear polynomials to replace costly resultants, trading larger cell counts for faster computations, and they analyze termination and several variants. Experimental results show notable runtime improvements for several simple under-approximation variants, while highlighting risks of non-termination and the need for termination controls. The approach demonstrates a practical path to accelerate NRA SMT solving and informs future work on termination guarantees, discriminant handling, and potential integration with cylindrical algebraic coverings.
Abstract
To check the satisfiability of (non-linear) real arithmetic formulas, modern satisfiability modulo theories (SMT) solving algorithms like NLSAT depend heavily on single cell construction, the task of generalizing a sample point to a connected subset (cell) of $\mathbb{R}^n$, that contains the sample and over which a given set of polynomials is sign-invariant. In this paper, we propose to speed up the computation and simplify the representation of the resulting cell by dynamically extending the considered set of polynomials with further linear polynomials. While this increases the total number of (smaller) cells generated throughout the algorithm, our experiments show that it can pay off when using suitable heuristics due to the interaction with Boolean reasoning.