Download PDFOpen PDF in browser

Linear Refutation and Clause Splitting

EasyChair Preprint 9423

10 pagesDate: December 5, 2022

Abstract

Linear resolution is one of the ancient methods for first-order theorem proving. We extend linear resolution with clause splitting, producing subgoals dispatched independently. An incremental SAT solver keeps track of refutations and thus provides a “lemma” mechanism. We describe some implementation considerations, present some initial experimental results, and discuss future directions for this approach.

Keyphrases: Boolean satisfiability, clause splitting, linear resolution

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@booklet{EasyChair:9423,
  author    = {Michael Rawson},
  title     = {Linear Refutation and Clause Splitting},
  howpublished = {EasyChair Preprint 9423},
  year      = {EasyChair, 2022}}
Download PDFOpen PDF in browser