REPORTS > DETAIL:

### Paper:

TR04-012 | 19th December 2003 00:00

#### The Resolution Complexity of Random Graph $k$-Colorability

TR04-012
Authors: Paul Beame, Joseph Culberson, David Mitchell, Cristopher Moore
Publication: 4th February 2004 16:51
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 length of resolution refutations. For any $\epsilon>0$, we obtain sub-exponential lower bounds of the form $2^{n^\delta}$ for some $\delta>0$ for non-$k$-colorability proofs of graphs with $n$ vertices and $O(n^{\frac{3}{2}-\frac{1}{k}-\epsilon}$ edges. We obtain sharper lower bounds for Davis-Putnam-DPLL proofs and for proofs in a system considered by McDiarmid.