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…