SAT-Inspired Eliminations for Superposition

Petar Vukmirović; Jasmin Blanchette; Marijn J.H. Heule

doi:10.1145/3565366

SAT-Inspired Eliminations for Superposition

Petar Vukmirović, Jasmin Blanchette, Marijn J.H. Heule

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

Abstract

Optimized SAT solvers not only preprocess the clause set, they also transform it during solving as inprocessing. Some preprocessing techniques have been generalized to first-order logic with equality. In this article, we port inprocessing techniques to work with superposition, a leading first-order proof calculus, and we strengthen known preprocessing techniques. Specifically, we look into elimination of hidden literals, variables (predicates), and blocked clauses. Our evaluation using the Zipperposition prover confirms that the new techniques usefully supplement the existing superposition machinery.

Original language	English
Article number	3565366
Pages (from-to)	1-25
Number of pages	25
Journal	ACM Transactions on Computational Logic
Volume	24
Issue number	1
Early online date	18 Jan 2023
DOIs	https://doi.org/10.1145/3565366
Publication status	Published - Jan 2023

Bibliographical note

Funding Information:
Vukmirović and Blanchette’s 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). Blanchette’s research has also received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward). Heule is supported by the National Science Foundation (NSF) under grant CCF-2015445.

Publisher Copyright:
© 2023 Copyright held by the owner/author(s). Publication rights licensed to ACM.

Funding

Vukmirović and Blanchette’s 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). Blanchette’s research has also received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward). Heule is supported by the National Science Foundation (NSF) under grant CCF-2015445.

Keywords

first-order logic
SAT solving
superposition calculus
Theorem proving

Access to Document

10.1145/3565366

Persistent URL (handle)

Persistent link

Cite this

@article{2d1c84386ae44102acdcb0671fc22cda,

title = "SAT-Inspired Eliminations for Superposition",

abstract = "Optimized SAT solvers not only preprocess the clause set, they also transform it during solving as inprocessing. Some preprocessing techniques have been generalized to first-order logic with equality. In this article, we port inprocessing techniques to work with superposition, a leading first-order proof calculus, and we strengthen known preprocessing techniques. Specifically, we look into elimination of hidden literals, variables (predicates), and blocked clauses. Our evaluation using the Zipperposition prover confirms that the new techniques usefully supplement the existing superposition machinery.",

keywords = "first-order logic, SAT solving, superposition calculus, Theorem proving",

author = "Petar Vukmirovi{\'c} and Jasmin Blanchette and Heule, {Marijn J.H.}",

note = "Funding Information: Vukmirovi{\'c} and Blanchette{\textquoteright}s 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). Blanchette{\textquoteright}s research has also received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward). Heule is supported by the National Science Foundation (NSF) under grant CCF-2015445. Publisher Copyright: {\textcopyright} 2023 Copyright held by the owner/author(s). Publication rights licensed to ACM.",

year = "2023",

month = jan,

doi = "10.1145/3565366",

language = "English",

volume = "24",

pages = "1--25",

journal = "ACM Transactions on Computational Logic",

issn = "1529-3785",

publisher = "Association for Computing Machinery (ACM)",

number = "1",

}

TY - JOUR

T1 - SAT-Inspired Eliminations for Superposition

AU - Vukmirović, Petar

AU - Blanchette, Jasmin

AU - Heule, Marijn J.H.

N1 - Funding Information: Vukmirović and Blanchette’s 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). Blanchette’s research has also received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward). Heule is supported by the National Science Foundation (NSF) under grant CCF-2015445. Publisher Copyright: © 2023 Copyright held by the owner/author(s). Publication rights licensed to ACM.

PY - 2023/1

Y1 - 2023/1

N2 - Optimized SAT solvers not only preprocess the clause set, they also transform it during solving as inprocessing. Some preprocessing techniques have been generalized to first-order logic with equality. In this article, we port inprocessing techniques to work with superposition, a leading first-order proof calculus, and we strengthen known preprocessing techniques. Specifically, we look into elimination of hidden literals, variables (predicates), and blocked clauses. Our evaluation using the Zipperposition prover confirms that the new techniques usefully supplement the existing superposition machinery.

AB - Optimized SAT solvers not only preprocess the clause set, they also transform it during solving as inprocessing. Some preprocessing techniques have been generalized to first-order logic with equality. In this article, we port inprocessing techniques to work with superposition, a leading first-order proof calculus, and we strengthen known preprocessing techniques. Specifically, we look into elimination of hidden literals, variables (predicates), and blocked clauses. Our evaluation using the Zipperposition prover confirms that the new techniques usefully supplement the existing superposition machinery.

KW - first-order logic

KW - SAT solving

KW - superposition calculus

KW - Theorem proving

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

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

U2 - 10.1145/3565366

DO - 10.1145/3565366

M3 - Article

AN - SCOPUS:85147333822

SN - 1529-3785

VL - 24

SP - 1

EP - 25

JO - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

IS - 1

M1 - 3565366

ER -

SAT-Inspired Eliminations for Superposition

Abstract

Bibliographical note

Funding

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this