The resolution complexity of random graph \(k\)-colorability (Q2581545)

The paper under review studies encoding the statements that a random graph is \(k\)-colourable as statements in conjunctive normal form and discussing lower bounds on the resolution complexity of these statements (roughly, how difficult it is to decide their truth or otherwise). A recurring theme of the paper is that there is a trade-off between the density (or average degree) of the graph and the complexity question: crudely, sparse graphs (whose number of edges is linear in their number of vertices) have exponential bounds on the size of resolution refutations, whereas if the graph has \(O(n^{3/2-1/k-\varepsilon})\) edges, the lower bounds on the size of resolution refutations are subexponential, of the form \(2^{n^{\delta}}\) for some \(\delta>0\). In somewhat more detail, if a graph \(G=(V,E)\) has \(n\) vertices and \(k\) is a number of colours, the authors write down a formula \(\chi(G,k)\) with \(kn\) variables comprising \(n\) positive clauses of width \(k\) and \({k\choose 2}n+k| E|\) negative clauses of width 2. \(\chi(G,k)\) is satisfiable if and only if \(G\) is properly \(k\)-colourable. The random graphs considered are from the model \(G(n,m)\) with labelled vertices \(\{1,2\ldots n\}\) and \(m\) edges, all such graphs being equally likely, (though for technical reasons the dirty work is done with the \(m\) edges chosen with replacement, and duplicates being merged: the practical differences are minimal). The results are worded in terms of \(\Delta(n)=m/n\). A resolution derivation of a clause \(C\) from some set of clauses is a sequence \(\pi=C_{0},\ldots C_{m}=C\) of clauses, each \(C_{i}\) either being in \(\pi\) or derived from two clauses \(C_{j}\) and \(C_{k}\) with \(j\) and \(k\) less than \(i\) by the \` resolution rule\', which allows one to derive the clause \(C\cup D\) from two clauses \(C\cup l\) and \(D\cup \sim l\) (here \(\sim\) denotes negation). The derivation is of size \(m\). A resolution derivation of the empty clause from \(\phi\) is called a refutation of \(\phi\) and there is a refutation of \(\phi\) if and only if \(\phi\) is unsatisfiable. The resolution complexity of \(\phi\), here \(\text{ Res}(\phi)\), is the size of a shortest refutation of \(\phi\). The main lower bound result is Theorem 1: For each \(k\geq 3\) and \(\varepsilon>0\) there are positive constants \(C_{\varepsilon,k}\) and \(C_{\varepsilon,k}>0\) such that, if \(\Delta\geq 1\), then for \(m\leq \Delta n\), \[ \lim_{n\rightarrow\infty}P\left(G=G(n,m)\text{ has Res}(\chi(G,k))\geq \exp(C_{\varepsilon,k}n/\Delta^{2+4/(k-2)+\varepsilon})\right)=1. \] The proof uses an interesting link between the fact that such a \(G\) is, in a suitable sense, locally sparse: this leads to a lower bound on the length of at least one clause in a resolution refutation of \(\chi(G,k)\), and this means that the refutation must take a long time. In the other direction, an upper bound on the resolution complexity is obtained by a quite simple idea: indeed any upper bound \(r'\) on the number of vertices such that random graphs \(G(n,m)\) with \(m\leq \Delta n\) have, with probability \(1-o(1)\), a minimal non-\(k\)-colourable graph of size at most \(r'\) leads to an algorithm for finding such a subgraph. However with a more sophisticated splitting rule in the search tree, the authors find an algorithm which refutes \(\chi(G,k)\) for \(k\geq 3\) for a random graph \(G(n,\Delta n)\) with probability \(1-o(1)\) in time \(\exp(b_{k}n/\Delta^{\alpha_{k}})\) for suitable constants \(a_{k}\) and \(b_{k}\). The basic idea is to show that if a large enough number of 2-variable clauses appear then there is a high probability that an unsatisfiable 2-SAT subformula appears. This is done by showing that the graph has a large connected subgraph which is not 2-colourable. Earlier work from [\textit{E. Ben-Sasson} and \textit{A. Wigderson}, ``Short proofs are narrow -- resolution made simple'', J. ACM 48, 149--169 (2001)] discussed a special class of refutations, called DPLL refutations. The authors use their results to obtain sharper bounds in this proof system, and also in a system considered by \textit{C. McDiarmid} [Ann. Oper. Res. 1, 183--200 (1984; Zbl 0673.05037)]. The paper closes with some discussion of the algorithms they have used, and several open problems.