ECCC
Electronic Colloquium on Computational Complexity
Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR04-012 | 19th December 2003 00:00

The Resolution Complexity of Random Graph $k$-Colorability

RSS-Feed




TR04-012
Authors: Paul Beame, Joseph Culberson, David Mitchell, Cristopher Moore
Publication: 4th February 2004 16:51
Downloads: 1283
Keywords: 


Abstract:

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.

We also show that very simple algorithms achieve qualitatively similar running times.



ISSN 1433-8092 | Imprint