A sharp threshold in proof complexity
Dimitris Achlioptas, Paul W. Beame, Michael S. O. Molloy · 2001
We give the first example of a sharp threshold in proof complexity. More precisely, we show that for any sufficiently small � and � � �, random formulas consisting of 2-clauses and 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 2-clauses (and 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.