Hard Clique Formulas for Resolution

TL;DR

This paper constructs explicit hard instances of the k-clique problem for Resolution proof systems, linking their difficulty to the hardness of refuting certain sparse, unsatisfiable 3-CNF formulas, and establishing new unconditional lower bounds.

Contribution

It introduces a method to convert hard unsatisfiable 3-CNF formulas into hard instances of the k-clique problem for Resolution, providing explicit, unconditional lower bounds.

Findings

Resolution can simulate correctness proofs of reductions from 3-SAT to k-clique.

Conditional hardness of k-clique under ETH is established for Resolution.

Explicit instances of k-clique are proven to be hard to refute in Resolution, unconditionally.

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^{\Omega(k)}$-hard to refute in Resolution. This applies to any function $k = k(n)$ of the number $n$ of vertices, provided $k_0 \leq k \leq 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^{\Omega(k)}$-hard to refute in Resolution. This solves an open problem that appeared published in the literature at least twice.