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$$ 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.

In this paper we present a quantifier elimination method for conjunctions of linear real arithmetic constraints. Our algorithm is based on the Fourier-Motzkin variable elimination procedure, but by case splitting we are able to reduce the worst-case complexity from doubly to singly exponential. The adaption of the procedure for SMT solving has strong correspondence to the simplex algorithm, therefore we name it FMplex. Besides the theoretical foundations, we provide an experimental evaluation in the context of SMT solving. This is an extended version of the authors' work previously published at the fourteenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2023).

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. Such an approach 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.

Usual formulations of the fundamental theorem of linear programming only consider weak inequalities as side conditions.