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.
Copyright. All Rights Reserved.