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

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

Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

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 publicationProceedings - 2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021
EditorsCarsten Schneider, Mircea Marin, Viorel Negru, Daniela Zaharie
PublisherIEEE
Pages37-39
Number of pages3
ISBN (Electronic)9781665406505
ISBN (Print)9781665406512
DOIs
Publication statusPublished - 2021
Event23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021 - Virtual, Online, Romania
Duration: 7 Dec 202110 Dec 2021

Publication series

NameProceedings - 2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021

Conference

Conference23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021
Country/TerritoryRomania
CityVirtual, Online
Period7/12/2110/12/21

Keywords

  • Cylindrical algebraic coverings
  • Implementation
  • Satisfiability modulo theories
  • Smt solving

ASJC Scopus subject areas

  • Artificial Intelligence
  • Computer Science Applications
  • Computational Mathematics
  • Modelling and Simulation

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