A sharp threshold in proof complexity

We give the first example of a sharp threshold in proof complexity. More precisely, we show that for any sufficiently small ε>0 and Δ>2.28 , random formulas consisting of (1-ε)n 2-clauses and &Dgr n 3-clauses, which are known to be unsatisfiable almost certainly, almost certainly require resolution and Davis-Putnam proofs of unsatisfiability of exponential size, whereas it is easily seen that random formulas with (1+ε)n 2-clauses (and Δ n 3 clauses) have linear size proofs of unsatisfiability almost certainly. A consequence of our result also yields the first proof that typical random 3-CNF formulas at ratios below the generally accepted range of the satisfiability threshold (and thus expected to be satisfiable almost certainly) cause natural Davis-Putnam algorithms to take exponential time to find satisfying assignments.

Authors

• Dimitris Achlioptas
• Paul Beame
• Michael Molloy 0001

Keywords

No keywords are indexed for this paper.