@inproceedings{284f6c668f754f58b0aed94725a3e803,
title = "On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving",
abstract = "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.",
keywords = "cylindrical algebraic coverings, implementation, satisfiability modulo theories, smt solving",
author = "Gereon Kremer and Erika Abraham and Matthew England and Davenport, \{James H.\}",
year = "2022",
month = feb,
day = "10",
doi = "10.1109/synasc54541.2021.00018",
language = "English",
isbn = "978-1-6654-0651-2",
series = "2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)",
publisher = "IEEE",
pages = "37--39",
editor = "Carsten Schneider and Mircea Marin and Viorel Negru and Daniela Zaharie",
booktitle = "2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)",
address = "United States",
note = "23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing , SYNASC ; Conference date: 07-12-2021 Through 10-12-2021",
url = "https://synasc.ro/2021/",
}
