Clique Is Hard on Average for Regular Resolution

TL;DR

This paper proves that regular resolution proof systems require superpolynomial length to refute certain Erdős-Rényi graphs lacking large cliques, establishing tight lower bounds and implications for clique-finding algorithms.

Contribution

It establishes tight lower bounds on regular resolution proof length for clique non-existence in Erdős-Rényi graphs, linking proof complexity with algorithmic hardness.

Findings

Regular resolution requires length n^{Ω(k)} for certain graphs.

Lower bounds are optimal up to constants in the exponent.

Implications for the running time of maximum clique algorithms.

Abstract

We prove that for $k \ll \sqrt[4]{n}$ regular resolution requires length $n^{\Omega(k)}$ to establish that an Erd\H{o}s-R\'enyi graph with appropriately chosen edge density does not contain a $k$-clique. This lower bound is optimal up to the multiplicative constant in the exponent, and also implies unconditional $n^{\Omega(k)}$ lower bounds on running time for several state-of-the-art algorithms for finding maximum cliques in graphs.