On the complexity of unsatisfiability proofs for random k-CNF formulas

Abstract

The complexity of proving unsatisfiability for random k-CNF formulas with clause density Δ = m/n where m is number of clauses and n is the number of variables is studied. The random 3-CNF formulas of clause density Δ almost certainly have no resolution refutation of size smaller than 2Ω(n/Δ(5+ε)), which implies the same lower bound on any Davis-Putnam algorithm.