Hard Clique Formulas for Resolution

Abstract

We show how to convert any unsatisfiable 3-CNF formula which is sparse and exponentially hard to refute in Resolution into a negative instance of the $k$-clique problem whose corresponding natural encoding as a CNF formula is $n^{\hat{I}\text{c◯}(k)}$-hard to refute in Resolution. This applies to any function $k=k(n)$ of the number $n$ of vertices, provided $k_0\le k\le n^{1/c_0}$, where $k_0$ and $c_0$ are small constants. We establish this by demonstrating that Resolution can simulate the correctness proof of a particular kind of reduction from 3-SAT to the parameterized clique problem. This also re-establishes the known conditional hardness result for $k$-clique which states that if the Exponential Time Hypothesis (ETH) holds, then the $k$-clique problem cannot be solved in time $n^{o(k)}$. Since it is known that the analogue of ETH holds for Resolution, unconditionally and with explicit hard instances, this gives a way to obtain explicit instances of $k$-clique that are unconditionally $n^{\hat{I}\text{c◯}(k)}$-hard to refute in Resolution. This solves an open problem that appeared published in the literature at least twice.

The size analysis in the final section is bogus (undercounts) and therefore the main claim Theorem 1 remains unproved. The open problem remains open