CISPA
Browse
cispa_all_2942.pdf (410.8 kB)

Strong Extension-Free Proof Systems

Download (410.8 kB)
journal contribution
posted on 2023-11-29, 18:07 authored by Marijn J. H. Heule, Benjamin Kiesl, Armin Biere
We introduce proof systems for propositional logic that admit short proofs of hard formulas as well as the succinct expression of most techniques used by modern SAT solvers. Our proof systems allow the derivation of clauses that are not necessarily implied, but which are redundant in the sense that their addition preserves satisfiability. To guarantee that these added clauses are redundant, we consider various efficiently decidable redundancy criteria which we obtain by first characterizing clause redundancy in terms of a semantic implication relationship and then restricting this relationship so that it becomes decidable in polynomial time. As the restricted implication relation is based on unit propagation—a core technique of SAT solvers—it allows efficient proof checking too. The resulting proof systems are surprisingly strong, even without the introduction of new variables—a key feature of short proofs presented in the proof-complexity literature. We demonstrate the strength of our proof systems on the famous pigeon hole formulas by providing short clausal proofs without new variables.

History

Preferred Citation

Marijn Heule, Benjamin Kiesl and Armin Biere. Strong Extension-Free Proof Systems. In: Journal of Automated Reasoning. 2019.

Primary Research Area

  • Reliable Security Guarantees

Legacy Posted Date

2019-07-03

Journal

Journal of Automated Reasoning

Open Access Type

  • Green

Sub Type

  • Article

BibTeX

@article{cispa_all_2942, title = "Strong Extension-Free Proof Systems", author = "Heule, Marijn J. H. and Kiesl, Benjamin and Biere, Armin", journal="{Journal of Automated Reasoning}", year="2019", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC