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^{Ω(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^{Ω(k)}$-hard to refute in Resolution. This solves an open problem that appeared published in the literature at least twice.

翻译：我们展示了如何将任何稀疏且在归结证明中难以反驳的不可满足3-CNF公式，转化为参数化团问题的负例实例，其对应的CNF编码公式在归结证明中具有$n^{Ω(k)}$级别的反驳难度。这一转化适用于顶点数$n$的任意函数$k = k(n)$，只要满足$k_0 \leq k \leq n^{1/c_0}$，其中$k_0$和$c_0$为小常数。我们通过证明归结证明能够模拟从3-SAT到参数化团问题的特定归约的正确性证明来确立这一结论。这也重新确立了关于$k$-团问题的已知条件硬度结果：若指数时间假设（ETH）成立，则$k$-团问题无法在$n^{o(k)}$时间内求解。由于已知ETH的类比在归结证明中无条件成立且存在显式难解实例，这提供了一种方法，可以获得在归结证明中无条件具有$n^{Ω(k)}$级别反驳难度的显式$k$-团问题实例。该研究解决了至少两次出现在公开文献中的开放性问题。