ECCC-Report TR04-012https://eccc.weizmann.ac.il/report/2004/012Comments and Revisions published for TR04-012en-usWed, 04 Feb 2004 16:51:11 +0200
Paper TR04-012
| The Resolution Complexity of Random Graph $k$-Colorability |
Paul Beame,
Joseph Culberson,
David Mitchell,
Cristopher Moore
https://eccc.weizmann.ac.il/report/2004/012We 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.
Wed, 04 Feb 2004 16:51:11 +0200https://eccc.weizmann.ac.il/report/2004/012