Strong Extension-Free Proof Systems

Abstract

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.

Keywords: Clause redundancy; Extended resolution; Pigeon hole problem; Proof checking; Proof complexity; Propositional proof systems; SAT.

Fig. 1

Landscape of redundancy notions of non-empty clauses. $\mathsf{R}$ denotes all redundant clauses and $\mathsf{IMP}$ stands for implied clauses. A path from X to Y indicates that X is more general than Y. The asterisk (${}^{\ast }$) denotes that the exact characterization implies the shown one, e.g., for every set-blocked clause, the property $F|\alpha \supseteq F|{\alpha }_L$ holds, but not vice versa

Fig. 2

Pseudo code of the $\mathsf{PR}$-proof checking algorithm

Fig. 3

Left, ten clauses of $PH{P}_3$ using the notation as elsewhere in this article and next to it the equivalent representation of these clauses in the DIMACS format used by SAT solvers. Right, the full $\mathsf{PR}$ refutation consisting of clause-witness pairs. A repetition of the first literal indicates the start of the optional witness