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.
| Original language | English |
|---|---|
| Title of host publication | 2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC) |
| Editors | Carsten Schneider, Mircea Marin, Viorel Negru, Daniela Zaharie |
| Publisher | IEEE |
| Pages | 37-39 |
| Number of pages | 3 |
| ISBN (Electronic) | 978-1-6654-0650-5 |
| ISBN (Print) | 978-1-6654-0651-2 |
| DOIs | |
| Publication status | Published - 10 Feb 2022 |
| Event | 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing - Department of Computer Science, West University of Timisoara, Timisoara, Romania Duration: 7 Dec 2021 → 10 Dec 2021 https://synasc.ro/2021/ |
Publication series
| Name | 2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC) |
|---|
Conference
| Conference | 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing |
|---|---|
| Abbreviated title | SYNASC |
| Country/Territory | Romania |
| City | Timisoara |
| Period | 7/12/21 → 10/12/21 |
| Internet address |
Keywords
- cylindrical algebraic coverings
- implementation
- satisfiability modulo theories
- smt solving