6 papers
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…
Extensions of the Cylindrical Algebraic Covering Method for Quantifiers
Jasper Nalbach, Gereon Kremer
The cylindrical algebraic covering method was originally proposed to decide the satisfiability of a set of non-linear real arithmetic constraints. We reformulate and extend the cyl…
Projective Delineability for Single Cell Construction
Jasper Nalbach, Lucas Michel, Erika Ãbrahám +5
The cylindrical algebraic decomposition (CAD) is the only complete method used in practice for solving problems like quantifier elimination or SMT solving related to real algebra,…
A Variant of Non-uniform Cylindrical Algebraic Decomposition for Real Quantifier Elimination
Jasper Nalbach, Erika Ãbrahám
The Cylindrical Algebraic Decomposition (CAD) method is currently the only complete algorithm used in practice for solving real-algebraic problems. To ameliorate its doubly-exponen…
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…
On Projective Delineability
Lucas Michel, Jasper Nalbach, Pierre Mathonet +5
We consider cylindrical algebraic decomposition (CAD) and the key concept of delineability which underpins CAD theory. We introduce the novel concept of projective delineability wh…