Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Hard Clique Formulas for Resolution

Albert Atserias

TL;DR

The paper establishes that sparse unsatisfiable 3-CNF formulas hard to refute in Resolution can be transformed into $n$-vertex CNF encodings of the $k$-clique problem that are hard to refute in Resolution, achieving a lower bound of $n^{Ω(k)}$. It achieves this via a reduction from 3-SAT to a $k$-clique instance constructed in a block-partite graph, preserving satisfiability and translating Resolution complexity through an explicit Prover–Adversary framework. The result yields unconditional, explicit hard instances for $k$-clique under Resolution, and revalidates ETH-type hardness in this setting, thereby transferring known exponential-resolution lower bounds to clique encodings. This provides a self-contained hardness transfer mechanism and broadens the understanding of proof complexity interactions between SAT, Resolution, and graph-clique encodings.

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^{Ω(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 answers an open problem that appeared published in the literature at least twice.

Hard Clique Formulas for Resolution

TL;DR

The paper establishes that sparse unsatisfiable 3-CNF formulas hard to refute in Resolution can be transformed into -vertex CNF encodings of the -clique problem that are hard to refute in Resolution, achieving a lower bound of . It achieves this via a reduction from 3-SAT to a -clique instance constructed in a block-partite graph, preserving satisfiability and translating Resolution complexity through an explicit Prover–Adversary framework. The result yields unconditional, explicit hard instances for -clique under Resolution, and revalidates ETH-type hardness in this setting, thereby transferring known exponential-resolution lower bounds to clique encodings. This provides a self-contained hardness transfer mechanism and broadens the understanding of proof complexity interactions between SAT, Resolution, and graph-clique encodings.

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 -clique problem whose corresponding natural encoding as a CNF formula is -hard to refute in Resolution. This applies to any function of the number of vertices, provided , where and 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 -clique which states that if the Exponential Time Hypothesis (ETH) holds, then the -clique problem cannot be solved in time . 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 -clique that are unconditionally -hard to refute in Resolution. This answers an open problem that appeared published in the literature at least twice.
Paper Structure (13 sections, 1 theorem)

This paper contains 13 sections, 1 theorem.

Table of Contents

  1. Introduction
  2. Clique formulas
  3. Map encoding
  4. Block encoding
  5. Resolution complexities
  6. Main result and reduction
  7. Reduction
  8. Only if
  9. If
  10. Setting of parameters
  11. Proof transformation
  12. Prover-Adversary games
  13. Strategy simulation

Key Result

Theorem 1

There exist positive integer constants $k_0$ and $c_0$, such that for every function $k = k(n)$ such that $k_0 \leq k \leq n^{1/c_0}$, there is an infinite family $G(1),G(2),\ldots$ of graphs, where $G = G(n)$ has $O(n)$ vertices and no $k$-cliques, such that every Resolution refutation of the map e

Theorems & Definitions (1)

  • Theorem 1