Marijn Heule, Benjamin Kiesl, Armin Biere,
"Strong Extension-Free Proof Systems"
, in Journal of Automated Reasoning, Vol. 64, Nummer 3, Springer, Seite(n) 533-554, 3-2020, ISSN: 0168-7433
Original Titel:
Strong Extension-Free Proof Systems
Sprache des Titels:
Englisch
Original Kurzfassung:
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 satis?ability. To guarantee that these added clauses are redundant, we consider various e?ciently decidable redundancy criteria which we obtain by ?rst 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 e?cient 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.
Sprache der Kurzfassung:
Englisch
Journal:
Journal of Automated Reasoning
Veröffentlicher:
Springer
Volume:
64
Number:
3
Seitenreferenz:
533-554
Erscheinungsmonat:
3
Erscheinungsjahr:
2020
ISSN:
0168-7433
Anzahl der Seiten:
22
Reichweite:
international
Publikationstyp:
Aufsatz / Paper in sonstiger referierter Fachzeitschrift
Forschungs-