The resolution complexity of random graph k-colorability Original Research Article

We consider the resolution proof complexity of propositional formulas which encode random instances of graph k-colorability. We obtain a tradeoff between the graph density and the resolution proof complexity. For random graphs with linearly many edges we obtain linear-exponential lower bounds on the size of resolution refutations. For random graphs with n vertices and any image, we obtain a lower-bound tradeoff between graph density and refutation size that implies subexponential lower bounds of the form image for some image for non-k-colorability proofs of graphs with n vertices and image edges. We obtain sharper lower bounds for Davis–Putnam–DPLL proofs and for proofs in a system considered by McDiarmid.