On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving
Gereon Kremer, Erika Ábrahám, Matthew England, James H. Davenport · 2021
We recently presented cylindrical algebraic coverings: a method based on the theory of cylindrical algebraic decomposition and suited for nonlinear real arithmetic theory reasoning in Satisfiability Modulo Theories solvers. We now present a more careful implementation within cvc5, discuss some implementation details, and highlight practical benefits compared to previous approaches, i.e., NLSAT and incremental CAD. We show how this new implementation simplifies proof generation for nonlinear real arithmetic problems in cvc5 and announce some very encouraging experimental results that position cvc5 at the very front of currently available SMT solvers for QF_NRA.