A sharp threshold in proof complexity yields lower bounds for satisfiability search

摘要

Let F(ρn,Δn) denote a random CNF formula consisting of ρn randomly chosen 2-clauses and Δn randomly chosen 3-clauses, for some arbitrary constants ρ,Δ⩾0. It is well-known that, with probability 1−o(1), if ρ>1 then F(ρn,Δn) has a linear-size resolution refutation. We prove that, with probability 1−o(1), if ρ<1 then F(ρn,Δn) has no subexponential-size resolution refutation.Our result also yields the first proof that random 3-CNF formulas with densities well below the generally accepted range of the satisfiability threshold (and thus believed to be satisfiable) cause natural Davis–Putnam algorithms to take exponential time (to find a satisfying assignment).