A polynomial-time WordRAM reduction from 3-SAT to CLIQUE

Proved

CliqueNP.threeSat_ram_clique_reduction

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

3-satcliquecook-levinnp-completenesswordram

There is a restricted-model WordRAM algorithm $A$ computing a string function $f$ in polynomially many steps such that for every bit string $x$ ,

x \in \mathrm{KSAT}_3 \iff f(x) \in \mathrm{CLIQUE}.

Here $\mathrm{KSAT}_3$ is the language of encodings of satisfiable CNF formulas whose clauses have at most $3$ literals, and CLIQUE is the language of encodings of finite simple undirected graphs together with a threshold $k$ such that the graph has a clique of at least $k$ vertices.

The intended construction is Karp's: for a formula with clauses $C_1,\dots,C_m$ , create one vertex per literal occurrence, join two occurrences by an edge iff they lie in different clauses and are not complementary, and set the threshold to $m$ . A clique of size $m$ picks one consistent literal per clause, i.e. a satisfying assignment, and conversely. Strings that do not encode a 3-CNF formula must be mapped to a fixed non-member of CLIQUE (e.g. the empty graph with threshold $1$ ). This is the NP-hardness half of CLIQUE's NP-completeness, in the same format as KSat.sat_ram_threeCNF_normalizer.

Preamble

import Definitions.Def_WordRAM_Complexity_BitIO
import Definitions.Def_KSat_Languages
import Definitions.Def_Clique_Language

set_option autoImplicit false

Formal statement

theorem CliqueNP.threeSat_ram_clique_reduction :
    ∃ (A : WordRAM.Complexity.Algorithm .restricted)
      (f : List Bool → List Bool),
      WordRAM.Complexity.RAMPolyTimeComputable A f ∧
      ∀ x, KSat.KSAT 3 x ↔ CliqueNP.CLIQUE (f x) := by sorry

Source

Richard M. Karp, Reducibility Among Combinatorial Problems, Complexity of Computer Computations, Plenum Press, pp. 85–103, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9 . SAT-to-CLIQUE reduction, p. 97, restricted to clause width at most 3 (the language `KSat.KSAT 3`).

View graph