Marijn Heule, Benjamin Kiesl, Armin Biere,
"Short Proofs Without New Variables"
: Lecture Notes in Computer Science, Serie Lecture Notes in Computer Science, Vol. 10395, Springer, Seite(n) 130-147, 2017
Short Proofs Without New Variables
Sprache des Titels:
Lecture Notes in Computer Science
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.