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

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

doi:10.1109/SYNASC54541.2021.00018

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 proceeding › Chapter in a published conference proceeding

3 Citations (SciVal)

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	Proceedings - 2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021
Editors	Carsten Schneider, Mircea Marin, Viorel Negru, Daniela Zaharie
Publisher	IEEE
Pages	37-39
Number of pages	3
ISBN (Electronic)	9781665406505
ISBN (Print)	9781665406512
DOIs	https://doi.org/10.1109/SYNASC54541.2021.00018
Publication status	Published - 2021
Event	23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021 - Virtual, Online, Romania Duration: 7 Dec 2021 → 10 Dec 2021

Publication series

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

Conference

Conference	23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021
Country/Territory	Romania
City	Virtual, Online
Period	7/12/21 → 10/12/21

Bibliographical note

Publisher Copyright:
© 2021 IEEE.

Keywords

Cylindrical algebraic coverings
Implementation
Satisfiability modulo theories
Smt solving

ASJC Scopus subject areas

Artificial Intelligence
Computer Science Applications
Computational Mathematics
Modelling and Simulation

Access to Document

10.1109/SYNASC54541.2021.00018

Cite this

Kremer, G., Abraham, E., England, M., & Davenport, J. H. (2021). On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving. In C. Schneider, M. Marin, V. Negru, & D. Zaharie (Eds.), Proceedings - 2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021 (pp. 37-39). (Proceedings - 2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021). IEEE. https://doi.org/10.1109/SYNASC54541.2021.00018

On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving. / Kremer, Gereon; Abraham, Erika; England, Matthew et al.
Proceedings - 2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021. ed. / Carsten Schneider; Mircea Marin; Viorel Negru; Daniela Zaharie. IEEE, 2021. p. 37-39 (Proceedings - 2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021).

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

Kremer, G, Abraham, E, England, M & Davenport, JH 2021, On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving. in C Schneider, M Marin, V Negru & D Zaharie (eds), Proceedings - 2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021. Proceedings - 2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021, IEEE, pp. 37-39, 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021, Virtual, Online, Romania, 7/12/21. https://doi.org/10.1109/SYNASC54541.2021.00018

Kremer G, Abraham E, England M, Davenport JH. On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving. In Schneider C, Marin M, Negru V, Zaharie D, editors, Proceedings - 2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021. IEEE. 2021. p. 37-39. (Proceedings - 2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021). doi: 10.1109/SYNASC54541.2021.00018

Kremer, Gereon ; Abraham, Erika ; England, Matthew et al. / On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving. Proceedings - 2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021. editor / Carsten Schneider ; Mircea Marin ; Viorel Negru ; Daniela Zaharie. IEEE, 2021. pp. 37-39 (Proceedings - 2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021).

@inproceedings{e130cac756f846968682964bef6efd93,

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.}",

note = "Publisher Copyright: {\textcopyright} 2021 IEEE.; 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021 ; Conference date: 07-12-2021 Through 10-12-2021",

year = "2021",

doi = "10.1109/SYNASC54541.2021.00018",

language = "English",

isbn = "9781665406512",

series = "Proceedings - 2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021",

publisher = "IEEE",

pages = "37--39",

editor = "Carsten Schneider and Mircea Marin and Viorel Negru and Daniela Zaharie",

booktitle = "Proceedings - 2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021",

address = "USA United States",

}

TY - GEN

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

AU - Kremer, Gereon

AU - Abraham, Erika

AU - England, Matthew

AU - Davenport, James H.

PY - 2021

Y1 - 2021

N2 - 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.

AB - 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.

KW - Cylindrical algebraic coverings

KW - Implementation

KW - Satisfiability modulo theories

KW - Smt solving

UR - http://www.scopus.com/inward/record.url?scp=85127018815&partnerID=8YFLogxK

U2 - 10.1109/SYNASC54541.2021.00018

DO - 10.1109/SYNASC54541.2021.00018

M3 - Chapter in a published conference proceeding

AN - SCOPUS:85127018815

SN - 9781665406512

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

SP - 37

EP - 39

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

A2 - Schneider, Carsten

A2 - Marin, Mircea

A2 - Negru, Viorel

A2 - Zaharie, Daniela

PB - IEEE

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

Y2 - 7 December 2021 through 10 December 2021

ER -

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

Abstract

Publication series

Conference

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition

Cite this

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

Abstract

Publication series

Conference

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Projects

Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition

Cite this