Showing cs.SCShow all
2 papers · 1 filter
cs.SC2025
More is Less: Adding Polynomials for Faster Explanations in NLSAT
Valentin Promies, Jasper Nalbach, Erika Ãbrahám +1
To check the satisfiability of (non-linear) real arithmetic formulas, modern satisfiability modulo theories (SMT) solving algorithms like NLSAT depend heavily on single cell constr…
cs.SC2025
FMplex: Exploring a Bridge between Fourier-Motzkin and Simplex
Valentin Promies, Jasper Nalbach, Erika Ãbrahám +1
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…