On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving

Gereon Kremer, Erika Abraham, Matthew England, James H. Davenport

Research output: Chapter in Book/Report/Conference proceedingConference proceedingpeer-review

3 Citations (Scopus)
78 Downloads (Pure)

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 languageEnglish
Title of host publication 2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)
EditorsCarsten Schneider, Mircea Marin, Viorel Negru, Daniela Zaharie
PublisherIEEE
Pages37-39
Number of pages3
ISBN (Electronic)978-1-6654-0650-5
ISBN (Print)978-1-6654-0651-2
DOIs
Publication statusPublished - 10 Feb 2022
Event23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing - Department of Computer Science, West University of Timisoara, Timisoara, Romania
Duration: 7 Dec 202110 Dec 2021
https://synasc.ro/2021/

Publication series

Name2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)

Conference

Conference23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing
Abbreviated title SYNASC
Country/TerritoryRomania
CityTimisoara
Period7/12/2110/12/21
Internet address

Keywords

  • cylindrical algebraic coverings
  • implementation
  • satisfiability modulo theories
  • smt solving

Fingerprint

Dive into the research topics of 'On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving'. Together they form a unique fingerprint.

Cite this