Marijn Heule, Benjamin Kiesl, Armin Biere,
"Short Proofs Without New Variables"
: Lecture Notes in Computer Science, Serie Lecture Notes in Computer Science (LNCS), Vol. 10395, Springer, Seite(n) 130-147, 2017
Original Titel:
Short Proofs Without New Variables
Sprache des Titels:
Englisch
Original Buchtitel:
Lecture Notes in Computer Science
Original Kurzfassung:
Adding and removing redundant clauses is at the core of state-of-the-art SAT solving. Crucial is the ability to add short clauses whose redundancy can be determined in polynomial time. We present a characterization of the strongest notion of clause redundancy (i.e., addition of the clause preserves satis?ability) in terms of an implication relationship. By using a polynomial-time decidable implication relation based on unit propagation, we thus obtain an e?ciently checkable redundancy notion. A proof system based on this notion is surprisingly strong, even without the introduction of new variables?the key component of short proofs presented in the proof complexity literature. We demonstrate this strength on the famous pigeon hole formulas by providing short clausal proofs without new variables.
Forschungs-