Skip to main content


Weitere Artikel dieser Ausgabe durch Wischen aufrufen

22.02.2019 | Ausgabe 3/2020 Open Access

Journal of Automated Reasoning 3/2020

Strong Extension-Free Proof Systems

Journal of Automated Reasoning > Ausgabe 3/2020
Marijn J. H. Heule, Benjamin Kiesl, Armin Biere
Wichtige Hinweise
Disclaimer: The authors strongly disagree with Springer’s typesetting practices. A version with the intended content and typesetting is available on the authors’ websites.
This work has been supported by the National Science Foundation under Grant CCF-1526760 and by the Austrian Science Fund (FWF) under Project W1255-N23.

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.


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.
Über diesen Artikel

Weitere Artikel der Ausgabe 3/2020

Journal of Automated Reasoning 3/2020 Zur Ausgabe

Premium Partner