Unifying Splitting

Gabriel Ebner; Jasmin Blanchette; Sophie Tourret

doi:10.1007/s10817-023-09660-8

Unifying Splitting

Gabriel Ebner^*, Jasmin Blanchette, Sophie Tourret

^*Corresponding author for this work

Research output: Contribution to Journal › Article › Academic › peer-review

Abstract

AVATAR is an elegant and effective way to split clauses in a saturation prover using a SAT solver. But is it refutationally complete? And how does it relate to other splitting architectures? To answer these questions, we present a unifying framework that extends a saturation calculus (e.g., superposition) with splitting and that embeds the result in a prover guided by a SAT solver. The framework also allows us to study locking, a subsumption-like mechanism based on the current propositional model. Various architectures are instances of the framework, including AVATAR, labeled splitting, and SMT with quantifiers.

Original language	English
Article number	16
Pages (from-to)	1-44
Number of pages	44
Journal	Journal of Automated Reasoning
Volume	67
Issue number	2
Early online date	28 Apr 2023
DOIs	https://doi.org/10.1007/s10817-023-09660-8
Publication status	Published - Jun 2023

Bibliographical note

Funding Information:
Petar Vukmirović greatly helped us design the abstract notions connected to A-formulas. Giles Reger patiently explained AVATAR and revealed some of its secrets. Simon Cruanes did the same regarding lightweight AVATAR. Simon Robillard, Martin Suda, Andrei Voronkov, Uwe Waldmann, and Christoph Weidenbach discussed splitting with us. Haniel Barbosa, Pascal Fontaine, Andrew Reynolds, and Cesare Tinelli explained some fine points of SMT. Natarajan Shankar pointed us to his work on the Shostak procedure. Ahmed Bhayat, Nicolas Peltier, Martin Suda, Mark Summerfield, Dmitriy Traytel, Petar Vukmirović, and the anonymous reviewers suggested textual improvements. We thank them all. This research has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (Grant Agreement No. 713999, Matryoshka). The research has also received funding from the Nederlandse Organisatie voor Wetenschappelijk Onderzoek (NWO) under the Vidi program (Project No. 016.Vidi.189.037, Lean Forward).

Publisher Copyright:
© 2023, The Author(s).

Keywords

Automated theorem proving
AVATAR
Completeness
Splitting

Access to Document

10.1007/s10817-023-09660-8

Persistent URL (handle)

Copy link address

Cite this

@article{aed2a92591a24ff496cb2b31463cd544,

title = "Unifying Splitting",

abstract = "AVATAR is an elegant and effective way to split clauses in a saturation prover using a SAT solver. But is it refutationally complete? And how does it relate to other splitting architectures? To answer these questions, we present a unifying framework that extends a saturation calculus (e.g., superposition) with splitting and that embeds the result in a prover guided by a SAT solver. The framework also allows us to study locking, a subsumption-like mechanism based on the current propositional model. Various architectures are instances of the framework, including AVATAR, labeled splitting, and SMT with quantifiers.",

keywords = "Automated theorem proving, AVATAR, Completeness, Splitting",

author = "Gabriel Ebner and Jasmin Blanchette and Sophie Tourret",

note = "Funding Information: Petar Vukmirovi{\'c} greatly helped us design the abstract notions connected to A-formulas. Giles Reger patiently explained AVATAR and revealed some of its secrets. Simon Cruanes did the same regarding lightweight AVATAR. Simon Robillard, Martin Suda, Andrei Voronkov, Uwe Waldmann, and Christoph Weidenbach discussed splitting with us. Haniel Barbosa, Pascal Fontaine, Andrew Reynolds, and Cesare Tinelli explained some fine points of SMT. Natarajan Shankar pointed us to his work on the Shostak procedure. Ahmed Bhayat, Nicolas Peltier, Martin Suda, Mark Summerfield, Dmitriy Traytel, Petar Vukmirovi{\'c}, and the anonymous reviewers suggested textual improvements. We thank them all. This research has received funding from the European Research Council (ERC) under the European Union{\textquoteright}s Horizon 2020 research and innovation program (Grant Agreement No. 713999, Matryoshka). The research has also received funding from the Nederlandse Organisatie voor Wetenschappelijk Onderzoek (NWO) under the Vidi program (Project No. 016.Vidi.189.037, Lean Forward). Publisher Copyright: {\textcopyright} 2023, The Author(s).",

year = "2023",

month = jun,

doi = "10.1007/s10817-023-09660-8",

language = "English",

volume = "67",

pages = "1--44",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "2",

}

TY - JOUR

T1 - Unifying Splitting

AU - Ebner, Gabriel

AU - Blanchette, Jasmin

AU - Tourret, Sophie

N1 - Funding Information: Petar Vukmirović greatly helped us design the abstract notions connected to A-formulas. Giles Reger patiently explained AVATAR and revealed some of its secrets. Simon Cruanes did the same regarding lightweight AVATAR. Simon Robillard, Martin Suda, Andrei Voronkov, Uwe Waldmann, and Christoph Weidenbach discussed splitting with us. Haniel Barbosa, Pascal Fontaine, Andrew Reynolds, and Cesare Tinelli explained some fine points of SMT. Natarajan Shankar pointed us to his work on the Shostak procedure. Ahmed Bhayat, Nicolas Peltier, Martin Suda, Mark Summerfield, Dmitriy Traytel, Petar Vukmirović, and the anonymous reviewers suggested textual improvements. We thank them all. This research has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (Grant Agreement No. 713999, Matryoshka). The research has also received funding from the Nederlandse Organisatie voor Wetenschappelijk Onderzoek (NWO) under the Vidi program (Project No. 016.Vidi.189.037, Lean Forward). Publisher Copyright: © 2023, The Author(s).

PY - 2023/6

Y1 - 2023/6

N2 - AVATAR is an elegant and effective way to split clauses in a saturation prover using a SAT solver. But is it refutationally complete? And how does it relate to other splitting architectures? To answer these questions, we present a unifying framework that extends a saturation calculus (e.g., superposition) with splitting and that embeds the result in a prover guided by a SAT solver. The framework also allows us to study locking, a subsumption-like mechanism based on the current propositional model. Various architectures are instances of the framework, including AVATAR, labeled splitting, and SMT with quantifiers.

AB - AVATAR is an elegant and effective way to split clauses in a saturation prover using a SAT solver. But is it refutationally complete? And how does it relate to other splitting architectures? To answer these questions, we present a unifying framework that extends a saturation calculus (e.g., superposition) with splitting and that embeds the result in a prover guided by a SAT solver. The framework also allows us to study locking, a subsumption-like mechanism based on the current propositional model. Various architectures are instances of the framework, including AVATAR, labeled splitting, and SMT with quantifiers.

KW - Automated theorem proving

KW - AVATAR

KW - Completeness

KW - Splitting

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

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

U2 - 10.1007/s10817-023-09660-8

DO - 10.1007/s10817-023-09660-8

M3 - Article

AN - SCOPUS:85156272752

SN - 0168-7433

VL - 67

SP - 1

EP - 44

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 2

M1 - 16

ER -

Unifying Splitting

Abstract

Bibliographical note

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this