Skip to Main content Skip to Navigation
Conference papers

A Unifying Splitting Framework

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 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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03364063
Contributor : Jasmin Blanchette Connect in order to contact the contributor
Submitted on : Monday, October 4, 2021 - 1:43:33 PM
Last modification on : Monday, February 14, 2022 - 8:13:16 PM
Long-term archiving on: : Wednesday, January 5, 2022 - 6:33:49 PM

File

conf.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Gabriel Ebner, Jasmin Blanchette, Sophie Tourret. A Unifying Splitting Framework. CADE 2021 - 28th International Conference on Automated Deduction, Jul 2021, Pittsburgh, PA / online, United States. pp.344-360, ⟨10.1007/978-3-030-79876-5_20⟩. ⟨hal-03364063⟩

Share

Metrics

Record views

44

Files downloads

35