The resolution complexity of random graph k-colorability
Paul W. Beame · 2005
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 ε>0, we obtain a lower-bound tradeoff between graph density and refutation size that implies subexponential lower bounds of the form 2nδ for some δ>0 for non-k-colorability proofs of graphs with n vertices and O(n3/2-1/k-ε) edges. We obtain sharper lower bounds for Davis–Putnam–DPLL proofs and for proofs in a system considered by McDiarmid. These proof complexity bounds imply that many natural algorithms for k-coloring or k-colorability have essentially the same exponential tradeoff lower bounds on their running times. We also show that very simple algorithms for k-colorability have upper bounds on their running times that are qualitatively similar to the lower bounds as a function of the graph density.