A phase transition in proof complexity and its implications for satisfiability search

Paul Beame
University of Washington
Comp Sci & Eng

We prove that random 3-CNF formulas, at clause-to-variable ratios below 4 and thus presumed to be satisfiable almost certainly, almost certainly cause natural backtracking search algorithms (also known as Davis-Putnam or DPLL algorithms) to take exponential time to find satisfying assignments.

We derive these results by giving the first example of a sharp threshold in proof complexity. More precisely, we show that for any sufficiently small epsilon>0 and D > 2.28, random formulas consisting of (1-epsilon)n 2-clauses and D 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+epsilon)n 2-clauses (and D n 3-clauses) have linear size proofs of unsatisfiability almost certainly.

We also outline how improvements in the bounds for the clause-variable ratios at which mixed formulas involving both 2- and 3-clauses become unsatisfiable to match their empirical values would imply that the DPLL algorithms we study (and their resolution-based extensions) would have sharp thresholds in their running time behavior on random 3-CNF formulas between linear time and exponential time and that these thresholds would be well below the empirical values of the satisfiability threshold.

Presentation (PowerPoint File)

Back to Phase Transitions And Algorithmic Complexity