Chapter 34 — NP-Completeness

CLRS, fourth edition · Lean 4 formalization

The proofs below use the models and assumptions described in the scope and implementation notes.

Imports

import CLRSLean.Chapter_34.Section_34_1_Polynomial_Time

34.1. Polynomial Time

This canonical fourth-edition reader page presents the deterministic polynomial-time framework used throughout Chapter 34.

Main results

Polynomial-time functions compose.
P is closed under complement, union, and intersection.
The concrete TM2 model connects executable machines to polynomial running bounds.

Implementation source

The complete theorem-bearing module is available in the Chapter 34 compatibility source.

Definitions and proofs

CLRSLean.Chapter_34.Section_34_1_Polynomial_Time

noncomputable sectionopen Computability StateTransition

34.1 Polynomial Time

CLRS §34.1: the complexity class P — languages that can be decided in polynomial time. We build on Mathlib's Turing.TM2ComputableInPolyTime (machine-level polynomial-time computability, using Polynomial ℕ time bounds) to define languages, polynomial-time decision, and the class P.

Main results:

Definition Language: a set of strings over an alphabet.
Definition PolyTimeComputable: a function computable by a TM2 machine in time bounded by a polynomial in the input length.
Definition PolyTimeDecidable: a language decided by a polynomial-time decision function.
Definition ClassP: the class of polynomial-time decidable languages.
Theorem PolyTimeComputable.comp: P is closed under function composition (via Turing.TM2Comp.comp_scratch).
Theorem PolyTimeDecidable.compl / ClassP_compl: P is closed under complement.
Theorem PolyTimeDecidable.union / ClassP_union: P is closed under union (via the AND/OR machine Turing.TM2AndOr).
Theorem PolyTimeDecidable.inter / ClassP_inter: P is closed under intersection.

The framework is deliberately abstract: the decision machine is existential. Concrete machine constructions and the closure properties (composition, complement, union, intersection) are developed in the sections that follow. Open problems (whether P = NP) are intentionally not addressed.

namespace CLRSnamespace Chapter34

A language over an alphabet Γ is a set of finite strings over Γ.

abbrev Language (Γ : Type) := Set (List Γ)

A function f : α → β is polynomial-time computable if there is a TM2 machine computing f (via the input/output encodings ea/eb) whose running time is bounded by a polynomial in the length of the encoded input.

def PolyTimeComputable {α β αΓ βΓ : Type} (ea : α → List αΓ) (eb : β → List βΓ)
    (f : α → β) : Prop :=
  Nonempty (Turing.TM2ComputableInPolyTime ea eb f)

Encode a Boolean decision result as a one-symbol string over Bool.

abbrev boolEncoding : Bool → List Bool := Turing.TM2Comp.boolEncoding

Encode a pair of strings over Γ as a single string over Option Γ, using none as a separator. The length is |x| + |y| + 1.

def pairEncoding {Γ : Type} (x y : List Γ) : List (Option Γ) :=
  List.map some x ++ [none] ++ List.map some y

A language L over Γ is polynomial-time decidable (L ∈ P) when there is a polynomial-time computable decision function f : List Γ → Bool such that x ∈ L iff f x = true (CLRS §34.1).

def PolyTimeDecidable {Γ : Type} (L : Language Γ) : Prop :=
  ∃ f : List Γ → Bool,
    PolyTimeComputable (id : List Γ → List Γ) boolEncoding f ∧
      ∀ x : List Γ, (f x = true) ↔ x ∈ L

The complexity class P: the languages decidable in polynomial time.

def ClassP (Γ : Type) : Set (Language Γ) :=
  { L | PolyTimeDecidable (Γ := Γ) L }

A language is in P iff it is polynomial-time decidable.

theorem mem_ClassP {Γ : Type} (L : Language Γ) : L ∈ ClassP Γ ↔ PolyTimeDecidable L := by
  rfl

Theorem (composition closure). The composition of two polynomial-time computable functions is polynomial-time computable (CLRS §34.1, closure of P under function composition). Backed by Turing.TM2ComputableInPolyTime.comp (via Turing.TM2Comp.comp_scratch).

theorem PolyTimeComputable.comp {α β γ αΓ βΓ γΓ : Type}
    {ea : α → List αΓ} {eb : β → List βΓ} {ec : γ → List γΓ} {f : α → β} {g : β → γ}
    (hf : PolyTimeComputable ea eb f) (hg : PolyTimeComputable eb ec g) :
    PolyTimeComputable ea ec (g ∘ f) := by
  rcases hf with ⟨M₁⟩
  rcases hg with ⟨M₂⟩
  exact Turing.TM2Comp.TM2ComputableInPolyTime.comp_scratch M₁ M₂

Closure under complement. The complement of a polynomial-time decidable language is polynomial-time decidable (CLRS §34.1): negate the decider.


theorem PolyTimeDecidable.compl {Γ : Type} (L : Language Γ) (hL : PolyTimeDecidable L) :
    PolyTimeDecidable (Lᶜ) := by
  rcases hL with ⟨f, hf, hf_iff⟩
  refine ⟨fun x => !f x, ?comp, ?iff⟩
  · exact PolyTimeComputable.comp hf ⟨Turing.TM2Comp.notComputableInPolyTime⟩
  · intro x
    simp only [Set.mem_compl_iff]
    rw [← hf_iff x]
    by_cases h : f x = true <;> simp [h, This simp argument is unused:
  Bool.not_eq_true

Hint: Omit it from the simp argument list.
  simp [h,̵ ̵B̵o̵o̵l̵.̵n̵o̵t̵_̵e̵q̵_̵t̵r̵u̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Bool.not_eq_true]

Closure under complement. P is closed under complement: L ∈ P implies Lᶜ ∈ P.

theorem ClassP_compl {Γ : Type} (L : Language Γ) (hL : L ∈ ClassP Γ) : Lᶜ ∈ ClassP Γ := by
  exact (mem_ClassP (Lᶜ)).mpr (PolyTimeDecidable.compl L hL)

Closure under union. The union of two polynomial-time decidable languages is polynomial-time decidable (CLRS §34.1): the decider ORs the two decision functions, run on the duplicated input by the AND/OR machine.

theorem PolyTimeDecidable.union {Γ : Type} [Inhabited Γ] (L₁ L₂ : Language Γ)
    (h₁ : PolyTimeDecidable L₁) (h₂ : PolyTimeDecidable L₂) :
    PolyTimeDecidable (L₁ ∪ L₂) := by
  rcases h₁ with ⟨f₁, hf₁, hf₁_iff⟩
  rcases h₂ with ⟨f₂, hf₂, hf₂_iff⟩
  rcases hf₁ with ⟨M₁⟩
  rcases hf₂ with ⟨M₂⟩
  letI : Fintype (M₁.tm.Γ M₁.tm.k₀) := M₁.tm.Γk₀Fin
  letI : Fintype Γ := Fintype.ofEquiv (M₁.tm.Γ M₁.tm.k₀) M₁.inputAlphabet
  refine ⟨fun x => f₁ x || f₂ x, ?comp, ?iff⟩
  · exact ⟨Turing.TM2AndOr.andOrComputableInPolyTime (M₁ := M₁) (M₂ := M₂) (op := Bool.or)⟩
  · intro x
    simp [hf₁_iff x, hf₂_iff x]

Closure under union. P is closed under union: L₁ ∈ P and L₂ ∈ P imply L₁ ∪ L₂ ∈ P.

theorem ClassP_union {Γ : Type} [Inhabited Γ] (L₁ L₂ : Language Γ)
    (h₁ : L₁ ∈ ClassP Γ) (h₂ : L₂ ∈ ClassP Γ) : L₁ ∪ L₂ ∈ ClassP Γ := by
  exact (mem_ClassP (L₁ ∪ L₂)).mpr (PolyTimeDecidable.union L₁ L₂ h₁ h₂)

Closure under intersection. The intersection of two polynomial-time decidable languages is polynomial-time decidable (CLRS §34.1): the decider ANDs the two decision functions.

theorem PolyTimeDecidable.inter {Γ : Type} [Inhabited Γ] (L₁ L₂ : Language Γ)
    (h₁ : PolyTimeDecidable L₁) (h₂ : PolyTimeDecidable L₂) :
    PolyTimeDecidable (L₁ ∩ L₂) := by
  rcases h₁ with ⟨f₁, hf₁, hf₁_iff⟩
  rcases h₂ with ⟨f₂, hf₂, hf₂_iff⟩
  rcases hf₁ with ⟨M₁⟩
  rcases hf₂ with ⟨M₂⟩
  letI : Fintype (M₁.tm.Γ M₁.tm.k₀) := M₁.tm.Γk₀Fin
  letI : Fintype Γ := Fintype.ofEquiv (M₁.tm.Γ M₁.tm.k₀) M₁.inputAlphabet
  refine ⟨fun x => f₁ x && f₂ x, ?comp, ?iff⟩
  · exact ⟨Turing.TM2AndOr.andOrComputableInPolyTime (M₁ := M₁) (M₂ := M₂) (op := Bool.and)⟩
  · intro x
    simp [hf₁_iff x, hf₂_iff x]

Closure under intersection. P is closed under intersection: L₁ ∈ P and L₂ ∈ P imply L₁ ∩ L₂ ∈ P.

theorem ClassP_inter {Γ : Type} [Inhabited Γ] (L₁ L₂ : Language Γ)
    (h₁ : L₁ ∈ ClassP Γ) (h₂ : L₂ ∈ ClassP Γ) : L₁ ∩ L₂ ∈ ClassP Γ := by
  exact (mem_ClassP (L₁ ∩ L₂)).mpr (PolyTimeDecidable.inter L₁ L₂ h₁ h₂)

end Chapter34end CLRS

Imports

import CLRSLean.Chapter_34.Section_34_2_Polynomial_Time_Verification

34.2. Polynomial-Time Verification

This reader page presents polynomial-time verification, bounded certificates, and the inclusion P ⊆ NP.

Main results

Deterministic polynomial-time decision procedures yield NP verifiers.
Polynomially bounded certificates characterize the chapter's NP languages.
Pair projections preserve the polynomial bounds needed by verifier inputs.

Implementation source

See the complete theorem-bearing source.

Definitions and proofs

CLRSLean.Chapter_34.Section_34_2_Polynomial_Time_Verification

34.2 Polynomial-Time Verification

CLRS §34.2: the complexity class NP — languages whose membership can be verified in polynomial time given a polynomial-size certificate.

Main results:

Definition PolyTimeVerifiable: a language verifiable by a polynomial-time verifier with polynomial-size certificates.
Definition ClassNP: the class of polynomially verifiable languages.
Theorem PolyTimeVerifiable.of_decidable: every P language is verifiable (the decider is a verifier that ignores the certificate).
Theorem ClassP_subset_ClassNP: P ⊆ NP (CLRS Theorem 34.2).

The verifier takes a certificate and an input (encoded as a single string with a separator); the certificate is required to have length bounded by a polynomial in the input length.

namespace CLRSnamespace Chapter34

A language L is polynomially verifiable (L ∈ NP) when there is a polynomial-time computable verifier V : List Γ → List Γ → Bool and a polynomial p such that x ∈ L iff some certificate c of length at most p(|x|) satisfies V c x = true (CLRS §34.2).

def PolyTimeVerifiable {Γ : Type} (L : Language Γ) : Prop :=
  ∃ V : List Γ → List Γ → Bool, ∃ p : Polynomial ℕ,
    PolyTimeComputable (fun pr : List Γ × List Γ => pairEncoding pr.1 pr.2)
      boolEncoding (fun pr : List Γ × List Γ => V pr.1 pr.2) ∧
    (∀ x : List Γ, x ∈ L ↔ ∃ c : List Γ, c.length ≤ p.eval x.length ∧ V c x = true)

The complexity class NP: polynomially verifiable languages.

def ClassNP (Γ : Type) : Set (Language Γ) :=
  { L | PolyTimeVerifiable (Γ := Γ) L }

A language is in NP iff it is polynomially verifiable.

theorem mem_ClassNP {Γ : Type} (L : Language Γ) : L ∈ ClassNP Γ ↔ PolyTimeVerifiable L := by
  rfl

Theorem 34.2 (P ⊆ NP). A polynomial-time decidable language is polynomially verifiable: the decider f is a verifier V c x := f x that ignores the certificate, run on the pair-encoded input via the projection machine Turing.Prj.prjComputableInPolyTime.


theorem PolyTimeVerifiable.of_decidable {Γ : Type} [Inhabited Γ] (L : Language Γ)
    (hL : PolyTimeDecidable L) :
    PolyTimeVerifiable L := by
  rcases hL with ⟨f, hf, hf_iff⟩
  have hf' := hf
  rcases hf with ⟨M⟩
  letI : Fintype (M.tm.Γ M.tm.k₀) := M.tm.Γk₀Fin
  letI : Fintype Γ := Fintype.ofEquiv (M.tm.Γ M.tm.k₀) M.inputAlphabet
  refine ⟨fun c x => f x, 0, ?comp, ?iff⟩
  · -- the verifier machine is the projection machine composed with the decider
    exact PolyTimeComputable.comp ⟨Turing.Prj.prjComputableInPolyTime (Γ := Γ)⟩ hf'
  · intro x
    rw [← hf_iff x]
    constructor
    · intro hfx
      exact ⟨[], by simpa using hfx⟩
    · rintro ⟨c, hc, hfx⟩
      exact hfx

Theorem 34.2: P ⊆ NP (CLRS §34.2).

theorem ClassP_subset_ClassNP {Γ : Type} [Inhabited Γ] : ClassP Γ ⊆ ClassNP Γ := by
  intro L hL
  exact (mem_ClassNP L).mpr (PolyTimeVerifiable.of_decidable (L := L) hL)

end Chapter34end CLRS

Imports

import CLRSLean.Chapter_34.Section_34_3_NP_Completeness_And_Reducibility

34.3. NP-Completeness and Reducibility

This reader page presents polynomial-time many-one reducibility and the transport principles used by every later NP-completeness proof.

Main results

Polynomial-time reductions compose transitively.
NP-hardness transports through a polynomial-time reduction.
A language in NP that is NP-hard is NP-complete.

Implementation source

See the complete theorem-bearing source.

Definitions and proofs

CLRSLean.Chapter_34.Section_34_3_NP_Completeness_And_Reducibility.Core

34.3 Core definitions for NP-completeness and reducibility

CLRS §34.3: polynomial-time reducibility and the definitions of NP-hard and NP-complete languages.

Main results:

Definition PolyTimeReducible: L₁ ≤_P L₂ — a polynomial-time computable reduction maps L₁ into L₂.
Definition NPHard: every polynomially verifiable language reduces to L.
Definition NPComplete: L ∈ NP and L is NP-hard.
Theorem PolyTimeReducible.trans: ≤_P is transitive (via the composition of polynomial-time machines).

namespace CLRSnamespace Chapter34

A language L₁ over Γ₁ is polynomial-time reducible to L₂ over Γ₂ (L₁ ≤_P L₂) when there is a polynomial-time computable function f with x ∈ L₁ iff f x ∈ L₂ (CLRS §34.3).

def PolyTimeReducible {Γ₁ Γ₂ : Type} (L₁ : Language Γ₁) (L₂ : Language Γ₂) : Prop :=
  ∃ f : List Γ₁ → List Γ₂,
    PolyTimeComputable (id : List Γ₁ → List Γ₁) (id : List Γ₂ → List Γ₂) f ∧
    (∀ x : List Γ₁, x ∈ L₁ ↔ f x ∈ L₂)

A language L is NP-hard when every polynomially verifiable language is polynomial-time reducible to L.

def NPHard {Γ : Type} (L : Language Γ) : Prop :=
  ∀ (Γ' : Type) (L' : Language Γ'), PolyTimeVerifiable L' → PolyTimeReducible L' L

A language L is NP-complete when L ∈ NP and L is NP-hard.

def NPComplete {Γ : Type} (L : Language Γ) : Prop :=
  PolyTimeVerifiable L ∧ NPHard L

Membership in the class of NP-complete languages.

def ClassNPC (Γ : Type) : Set (Language Γ) :=
  { L | NPComplete (Γ := Γ) L }

Theorem (transitivity of ≤_P). Polynomial-time reducibility is transitive (CLRS §34.3): if L₁ ≤_P L₂ and L₂ ≤_P L₃ then L₁ ≤_P L₃, by composing the two reductions with PolyTimeComputable.comp.

theorem PolyTimeReducible.trans {Γ₁ Γ₂ Γ₃ : Type} {L₁ : Language Γ₁} {L₂ : Language Γ₂}
    {L₃ : Language Γ₃} (h₁₂ : PolyTimeReducible L₁ L₂) (h₂₃ : PolyTimeReducible L₂ L₃) :
    PolyTimeReducible L₁ L₃ := by
  rcases h₁₂ with ⟨f, hf, hf_iff⟩
  rcases h₂₃ with ⟨g, hg, hg_iff⟩
  refine ⟨g ∘ f, ?comp, ?iff⟩
  · exact PolyTimeComputable.comp hf hg
  · intro x
    change x ∈ L₁ ↔ g (f x) ∈ L₃
    exact (hf_iff x).trans (hg_iff (f x))

end Chapter34end CLRS

CLRSLean.Chapter_34.Section_34_3_NP_Completeness_And_Reducibility.Hardness

NP-hardness transport

Polynomial-time reductions transport polynomial-time decidability and NP-hardness, and expose the two components of an NP-completeness proof.

Main results:

Theorem PolyTimeDecidable.of_reducible: decidability transports backward along a polynomial-time reduction.
Theorem NPHard.of_reducible: NP-hardness transports forward along a polynomial-time reduction.
Theorem NPComplete.of_reducible: a verifiable target of a reduction from an NP-complete language is NP-complete.
Theorems NPComplete.verifiable and NPComplete.hard: direct projections from NP-completeness.

namespace CLRSnamespace Chapter34

Polynomial-time decidability transports backward along a polynomial-time reduction: deciding the target after computing the reduction decides the source language.

theorem PolyTimeDecidable.of_reducible {Γ₁ Γ₂ : Type}
    {L₁ : Language Γ₁} {L₂ : Language Γ₂}
    (hred : PolyTimeReducible L₁ L₂)
    (hdec : PolyTimeDecidable L₂) :
    PolyTimeDecidable L₁ := by
  rcases hred with ⟨f, hf, hiff⟩
  rcases hdec with ⟨d, hd, hdiff⟩
  exact ⟨d ∘ f, PolyTimeComputable.comp hf hd,
    fun x => (hdiff (f x)).trans (hiff x).symm⟩

NP-hardness transports forward along a polynomial-time reduction from an NP-hard source language.

theorem NPHard.of_reducible {Γ₁ Γ₂ : Type} {L₁ : Language Γ₁}
    {L₂ : Language Γ₂} (hhard : NPHard L₁)
    (hred : PolyTimeReducible L₁ L₂) : NPHard L₂ := by
  intro Γ L hL
  exact (hhard Γ L hL).trans hred

A polynomially verifiable target is NP-complete when an NP-complete language reduces to it in polynomial time.

theorem NPComplete.of_reducible {Γ₁ Γ₂ : Type} {L₁ : Language Γ₁}
    {L₂ : Language Γ₂} (hcomplete : NPComplete L₁)
    (hred : PolyTimeReducible L₁ L₂)
    (hmem : PolyTimeVerifiable L₂) : NPComplete L₂ :=
  ⟨hmem, NPHard.of_reducible hcomplete.2 hred⟩

Extract polynomial-time verifiability from an NP-completeness proof.

theorem NPComplete.verifiable {Γ : Type} {L : Language Γ}
    (h : NPComplete L) : PolyTimeVerifiable L := h.1

Extract NP-hardness from an NP-completeness proof.

theorem NPComplete.hard {Γ : Type} {L : Language Γ}
    (h : NPComplete L) : NPHard L := h.2

end Chapter34end CLRS

Imports

import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs

34.4. NP-Completeness Proofs

This reader page presents Cook--Levin and the first concrete NP-completeness reductions in the textbook chain.

Main results

Cook--Levin reduces every NP language to general circuit satisfiability.
CIRCUIT-SAT ≤_P SAT ≤_P 3-CNF-SAT ≤_P CLIQUE.
SAT and 3-CNF-SAT have total raw assignment checkers with linear certificate bounds, fixed reduction-backed verifier machines, and standalone NP-completeness theorems.
General circuit satisfiability and the public graph-plus-k CLIQUE language are NP-complete.

Implementation source

See the complete theorem-bearing source.

Definitions and proofs

CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.CircuitSAT

CIRCUIT-SAT: the language of satisfiable circuits, encoded as gate lists.

def CIRCUIT_SAT : Language Gate :=
  { gates | CircuitSatisfiable gates }

SAT: the language of satisfiable boolean formulas, encoded as prefix-polish symbol lists (decoded via decode). Membership is defined through the decoder so that reductions on encoded lists stay total.

def SAT : Language FormulaSym :=
  { syms | Formula.Satisfiable (decode syms) }

Theorem (CIRCUIT-SAT poly-reduces to SAT, CLRS Lemma 34.6). A circuit is satisfiable iff the formula produced by circuitToFormulaList is satisfiable.


theorem circuitSAT_reducible_to_SAT : PolyTimeReducible CIRCUIT_SAT SAT := by
  refine ⟨circuitToFormulaList, ?comp, ?iff⟩
  · exact ⟨Turing.TM2CS.csComputableInPolyTime⟩
  · intro gates
    rw [circuitToFormulaList_eq_enc]
    constructor
    · intro hc
      have hsat := (circuitSatisfiable_iff_satisfiable_circuitToFormula gates).1 hc
      change Formula.Satisfiable (decode (enc (circuitToFormula gates)))
      simpa [decode_enc] using hsat
    · intro hs
      have hsat' : Formula.Satisfiable (circuitToFormula gates) := by
        change Formula.Satisfiable (decode (enc (circuitToFormula gates))) at hs
        simpa [decode_enc] using hs
      exact (circuitSatisfiable_iff_satisfiable_circuitToFormula gates).2 hsat'

CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.GeneralCircuit.Basic

A well-formed general circuit is satisfiable when some assignment of its declared input bits makes the designated output gate true.

def GeneralCircuitSatisfiable (c : Circuit) : Prop :=
  c.WellFormed ∧
    ∃ assignment : Fin c.inputCount → Bool,
      c.eval (fun i => if hi : i < c.inputCount then assignment ⟨i, hi⟩ else false) = true

CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.GeneralCircuit.Encoding

The language of exactly decoded, well-formed, satisfiable general circuits.

def GeneralCircuitSAT : Language CircuitSym :=
  { input | ∃ c, decodeCircuit input = some c ∧ GeneralCircuitSatisfiable c }

CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.GeneralCircuit.NP

GeneralCircuitSAT has polynomial-size assignment certificates checked by the concrete polynomial-time verifier machine.

theorem generalCircuitSAT_polyTimeVerifiable :
    PolyTimeVerifiable GeneralCircuitSAT := by
  refine ⟨generalCircuitVerifier, Polynomial.X, ?_, ?_⟩
  · exact ⟨Turing.GeneralCircuitVerifier.generalCircuitVerifierComputableInPolyTime⟩
  · intro input
    simpa using mem_generalCircuitSAT_iff_exists_certificate input

The honest serialized general-circuit satisfiability language belongs to the complexity class NP.

theorem generalCircuitSAT_mem_ClassNP :
    GeneralCircuitSAT ∈ ClassNP CircuitSym :=
  (mem_ClassNP GeneralCircuitSAT).2 generalCircuitSAT_polyTimeVerifiable

CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.CookLevin.MainTheorem

The concrete Cook--Levin map is a polynomial-time many-one reduction for every normalized verifier witness.

theorem cookLevin_polyTimeReducible
    {Γ : Type} {L : Language Γ} (W : VerifierWitness L) :
    PolyTimeReducible L GeneralCircuitSAT :=
  cookLevin_polyTimeReducible_of_computable W
    (cookLevinMap_polyTimeComputable W)

Cook--Levin theorem. Every polynomially verifiable language reduces in polynomial time to general Boolean-circuit satisfiability.

theorem cookLevin_theorem {Γ : Type} {L : Language Γ}
    (hL : PolyTimeVerifiable L) :
    PolyTimeReducible L GeneralCircuitSAT :=
  cookLevin_polyTimeReducible (VerifierWitness.ofPolyTimeVerifiable hL)

General circuit satisfiability is NP-hard.

theorem generalCircuitSAT_npHard : NPHard GeneralCircuitSAT := by
  intro Γ L hL
  exact cookLevin_theorem hL

General circuit satisfiability is NP-complete.

theorem generalCircuitSAT_npComplete : NPComplete GeneralCircuitSAT :=
  ⟨generalCircuitSAT_polyTimeVerifiable, generalCircuitSAT_npHard⟩

CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.GeneralCircuit.ToSAT.Reduction

The direct consistency-formula construction is a genuine polynomial-time many-one reduction on the honest raw languages.

theorem generalCircuitSAT_reducible_to_SAT :
    PolyTimeReducible GeneralCircuitSAT SAT := by
  refine ⟨generalCircuitToSATMap,
    ⟨Turing.GeneralCircuitToSAT.computableInPolyTime⟩, ?_⟩
  intro input
  exact (generalCircuitToSATMap_mem_SAT_iff input).symm

SAT is NP-hard, obtained directly from the completed Cook--Levin target and the verified general-circuit-to-formula machine.

theorem SAT_npHard : NPHard SAT :=
  NPHard.of_reducible Turing.CookLevin.generalCircuitSAT_npHard
    generalCircuitSAT_reducible_to_SAT

CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.SatTo3CNFSat

A CNF is in the project's 3-CNF normal form when every clause contains at most three literals. The at-most-three convention includes the unit and binary clauses emitted by the concrete Tseitin machine.

def IsThreeCNF (f : CNF) : Prop :=
  ∀ c ∈ f, c.length ≤ 3

3-CNF-SAT: the language of satisfiable CNF formulas whose clauses have at most three literals, encoded as symbol lists (decoded via decodeCNF).

def ThreeCNFSat : Language CNFSym :=
  { syms | IsThreeCNF (decodeCNF syms) ∧ CnfSatisfiable (decodeCNF syms) }

CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.SatTo3CNFMachine

Lemma 34.7 (computational form). SAT polynomial-time reduces to 3-CNF-SAT through the concrete, length-indexed Tseitin encoder.


theorem sat_reducible_to_threeCNFSat :
    PolyTimeReducible SAT ThreeCNFSat := by
  refine ⟨fun x => encCNF (to3CNF_len (decode x) x.length), ?_, ?_⟩
  · exact ⟨satTo3CNFComputableInPolyTime⟩
  · intro x
    change Formula.Satisfiable (decode x) ↔
      IsThreeCNF (decodeCNF (encCNF (to3CNF_len (decode x) x.length))) ∧
        CnfSatisfiable (decodeCNF (encCNF (to3CNF_len (decode x) x.length)))
    rw [decodeCNF_encCNF]
    constructor
    · intro hsat
      exact ⟨isThreeCNF_to3CNF_len (decode x) x.length,
        (cnfSatisfiable_to3CNF_len_iff (decode x) x.length
          (numVars_decode_le x)).2 hsat⟩
    · intro h
      exact (cnfSatisfiable_to3CNF_len_iff (decode x) x.length
        (numVars_decode_le x)).1 h.2

CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.SAT.Verification

Check a finite serialized assignment against a raw encoded SAT formula.

def satVerifier (certificate input : List FormulaSym) : Bool :=
  certificate.all isFormulaAssignmentSymbol &&
    Formula.eval (decode input) (formulaAssignmentInputs certificate)

Exact all-input acceptance semantics of the serialized SAT checker.

theorem satVerifier_accepts_iff (certificate input : List FormulaSym) :
    satVerifier certificate input = true ↔
      certificate.all isFormulaAssignmentSymbol = true ∧
        Formula.eval (decode input)
          (formulaAssignmentInputs certificate) = true := by
  simp [satVerifier]

Any certificate containing a non-literal formula symbol is rejected.

theorem satVerifier_eq_false_of_malformed
    {certificate input : List FormulaSym}
    (hmalformed : certificate.all isFormulaAssignmentSymbol ≠ true) :
    satVerifier certificate input = false := by
  simp [satVerifier, hmalformed]

Membership in raw SAT is exactly acceptance by some canonical assignment certificate whose length is at most the raw formula length.


theorem mem_SAT_iff_exists_bounded_certificate (input : List FormulaSym) :
    input ∈ SAT ↔
      ∃ certificate : List FormulaSym,
        certificate.length ≤ input.length ∧
          satVerifier certificate input = true := by
  constructor
  · rintro ⟨assignment, heval⟩
    let certificate := encodeFormulaAssignment input.length assignment
    refine ⟨certificate, ?_, ?_⟩
    · simp [certificate]
    · apply (satVerifier_accepts_iff certificate input).2
      refine ⟨by simp [certificate], ?_⟩
      have hagree : ∀ index,
          index < numVars (decode input) →
            assignment index = formulaAssignmentInputs certificate index := by
        intro index hindex
        have hlength : index < input.length :=
          lt_of_lt_of_le hindex (numVars_decode_le input)
        symm
        simpa [certificate] using
          formulaAssignmentInputs_encodeFormulaAssignment_of_lt
            input.length assignment index hlength
      have heq := Formula.eval_eq_of_agree
        (decode input) assignment (formulaAssignmentInputs certificate) hagree
      rwa [← heq]
  · rintro ⟨certificate, _hlength, haccept⟩
    refine ⟨formulaAssignmentInputs certificate, ?_⟩
    exact (satVerifier_accepts_iff certificate input).1 haccept |>.2

CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.SAT.NPCompleteness

Raw SAT has a concrete polynomial-time verifier and a polynomial certificate bound.

theorem SAT_polyTimeVerifiable : PolyTimeVerifiable SAT := by
  refine ⟨satReductionVerifier, satReductionCertificatePolynomial, ?_, ?_⟩
  · exact ⟨Turing.SATVerifier.reductionVerifierComputableInPolyTime⟩
  · exact mem_SAT_iff_exists_reduction_certificate

Raw SAT belongs to NP.

theorem SAT_mem_ClassNP : SAT ∈ ClassNP FormulaSym :=
  (mem_ClassNP SAT).2 SAT_polyTimeVerifiable

Raw SAT is NP-complete.

theorem SAT_npComplete : NPComplete SAT :=
  ⟨SAT_polyTimeVerifiable, SAT_npHard⟩

CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.ThreeCNF.Verification

Boolean evaluation of one clause under an assignment.

def evalClauseBool (assignment : Nat → Bool) (clause : Clause) : Bool :=
  clause.any (evalLitBool assignment)

Boolean evaluation of a CNF formula under an assignment.

def evalCNFBool (assignment : Nat → Bool) (formula : CNF) : Bool :=
  formula.all (evalClauseBool assignment)

Boolean recognition of the project's at-most-three-literals CNF shape.

def isThreeCNFBool (formula : CNF) : Bool :=
  formula.all fun clause => decide (clause.length ≤ 3)

Check a finite serialized assignment against a raw encoded 3-CNF formula.

def threeCNFSatVerifier (certificate input : List CNFSym) : Bool :=
  certificate.all isCNFAssignmentSymbol &&
    isThreeCNFBool (decodeCNF input) &&
      evalCNFBool (cnfAssignmentInputs certificate) (decodeCNF input)

Exact all-input acceptance semantics of the serialized 3-CNF-SAT checker.

theorem threeCNFSatVerifier_accepts_iff
    (certificate input : List CNFSym) :
    threeCNFSatVerifier certificate input = true ↔
      certificate.all isCNFAssignmentSymbol = true ∧
        IsThreeCNF (decodeCNF input) ∧
          evalCNF (cnfAssignmentInputs certificate) (decodeCNF input) := by
  simp [threeCNFSatVerifier, and_assoc]

Any certificate containing a symbol other than posMark or negMark is rejected.

theorem threeCNFSatVerifier_eq_false_of_malformed
    {certificate input : List CNFSym}
    (hmalformed : certificate.all isCNFAssignmentSymbol ≠ true) :
    threeCNFSatVerifier certificate input = false := by
  simp [threeCNFSatVerifier, hmalformed]

Membership in raw ThreeCNFSat is exactly acceptance by some canonical assignment certificate whose length is at most the raw formula length.


theorem mem_threeCNFSat_iff_exists_bounded_certificate
    (input : List CNFSym) :
    input ∈ ThreeCNFSat ↔
      ∃ certificate : List CNFSym,
        certificate.length ≤ input.length ∧
          threeCNFSatVerifier certificate input = true := by
  constructor
  · rintro ⟨hthree, assignment, heval⟩
    let certificate := encodeCNFAssignment input.length assignment
    refine ⟨certificate, ?_, ?_⟩
    · simp [certificate]
    · apply (threeCNFSatVerifier_accepts_iff certificate input).2
      refine ⟨by simp [certificate], hthree, ?_⟩
      have hagree : ∀ index,
          index < input.length →
            assignment index = cnfAssignmentInputs certificate index := by
        intro index hindex
        symm
        simpa [certificate] using
          cnfAssignmentInputs_encodeCNFAssignment_of_lt
            input.length assignment index hindex
      exact (evalCNF_of_agree assignment (cnfAssignmentInputs certificate)
        input.length (decodeCNF input) (decodeCNF_indices_lt input) hagree).1
          heval
  · rintro ⟨certificate, _hlength, haccept⟩
    rcases (threeCNFSatVerifier_accepts_iff certificate input).1 haccept with
      ⟨_hcertificate, hthree, heval⟩
    exact ⟨hthree, cnfAssignmentInputs certificate, heval⟩

CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.ThreeCNF.NPCompleteness

Raw 3-CNF-SAT has a concrete polynomial-time verifier and a polynomial certificate bound.

theorem threeCNFSat_polyTimeVerifiable :
    PolyTimeVerifiable ThreeCNFSat := by
  refine ⟨threeCNFReductionVerifier,
    threeCNFReductionCertificatePolynomial, ?_, ?_⟩
  · exact ⟨Turing.ThreeCNFVerifier.reductionVerifierComputableInPolyTime⟩
  · exact mem_threeCNFSat_iff_exists_reduction_certificate

Raw 3-CNF-SAT belongs to NP.

theorem threeCNFSat_mem_ClassNP : ThreeCNFSat ∈ ClassNP CNFSym :=
  (mem_ClassNP ThreeCNFSat).2 threeCNFSat_polyTimeVerifiable

Raw 3-CNF-SAT is NP-complete.

theorem threeCNFSat_npComplete : NPComplete ThreeCNFSat :=
  ⟨threeCNFSat_polyTimeVerifiable, threeCNFSat_npHard⟩

CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.GeneralClique.Instance

A finite undirected graph together with the requested clique size. Edges use natural-number vertex names and are stored in normalized order.

structure CliqueInstance where
  vertexCount : Nat
  targetSize : Nat
  edges : List (Nat × Nat)
  deriving DecidableEq, Repr

A CLIQUE instance is well formed when the target fits in the vertex set and every stored edge is normalized and in range.

Repeated edge records are accepted: adjacency is defined by membership, so duplicates do not change the represented simple graph or its cliques. Edge list uniqueness remains available as a separate serialization-canonicality predicate when a downstream construction needs it.

def WellFormed (I : CliqueInstance) : Prop :=
  I.targetSize ≤ I.vertexCount ∧
    ∀ e ∈ I.edges, e.1 < e.2 ∧ e.2 < I.vertexCount

Symmetric adjacency induced by the normalized edge list.

def Adj (I : CliqueInstance) (u v : Nat) : Prop :=
  if u < v then (u, v) ∈ I.edges
  else if v < u then (v, u) ∈ I.edges
  else False

The graph contains a clique with exactly the requested number of vertices.

def HasClique (I : CliqueInstance) : Prop :=
  ∃ vertices : Finset Nat,
    vertices.card = I.targetSize ∧
      (∀ v ∈ vertices, v < I.vertexCount) ∧
      ∀ u ∈ vertices, ∀ v ∈ vertices, u ≠ v → I.Adj u v

CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.GeneralClique.Language

General graph-plus-k CLIQUE over the unique CliqueSym grammar.

def GeneralCLIQUE : Language CliqueSym :=
  { input |
      ∃ I, decodeCliqueInstance input = some I ∧ I.WellFormed ∧ I.HasClique }

CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.GeneralClique.Public

The textbook general graph-plus-k CLIQUE language.

abbrev CLIQUE : Language CliqueSym := GeneralCLIQUE

The concrete polynomial-time reduction from 3-CNF-SAT to textbook general CLIQUE.

theorem threeCNFSat_reducible_to_CLIQUE :
    PolyTimeReducible ThreeCNFSat CLIQUE :=
  threeCNFSat_reducible_to_generalCLIQUE

CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.GeneralClique.NP

The honest general CLIQUE language has a concrete polynomial-time verifier with quadratically bounded certificates.

theorem generalCLIQUE_polyTimeVerifiable :
    PolyTimeVerifiable GeneralCLIQUE := by
  refine ⟨cliqueVerifier, (Polynomial.X + 1) ^ 2, ?_, ?_⟩
  · exact ⟨Turing.GeneralCliqueVerifier.cliqueVerifierComputableInPolyTime⟩
  · intro input
    simpa [Polynomial.eval_add, Polynomial.eval_pow, Polynomial.eval_X] using
      mem_generalCLIQUE_iff_exists_certificate input

Textbook general CLIQUE belongs to NP.

theorem generalCLIQUE_mem_ClassNP : GeneralCLIQUE ∈ ClassNP CliqueSym :=
  (mem_ClassNP GeneralCLIQUE).2 generalCLIQUE_polyTimeVerifiable

CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.GeneralClique.Completeness

3-CNF-SAT is NP-hard through the concrete SAT-to-3-CNF machine.

theorem threeCNFSat_npHard : NPHard ThreeCNFSat :=
  NPHard.of_reducible SAT_npHard
    Turing.TM3CNF.sat_reducible_to_threeCNFSat

The honest serialized graph-plus-k CLIQUE language is NP-hard.

theorem generalCLIQUE_npHard : NPHard GeneralCLIQUE :=
  NPHard.of_reducible threeCNFSat_npHard
    Turing.TMClique.threeCNFSat_reducible_to_generalCLIQUE

The honest serialized graph-plus-k CLIQUE language is NP-complete.

theorem generalCLIQUE_npComplete : NPComplete GeneralCLIQUE :=
  ⟨generalCLIQUE_polyTimeVerifiable, generalCLIQUE_npHard⟩

Public textbook spelling of the general CLIQUE NP-completeness theorem.

theorem CLIQUE_npComplete : NPComplete CLIQUE :=
  generalCLIQUE_npComplete

Imports

import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems

34.5. NP-Complete Problems

This reader page presents the selected textbook chain beyond CLIQUE.

Main results

VERTEX-COVER is NP-complete.
HAM-CYCLE is NP-complete.
Decision-TSP is NP-complete.
SUBSET-SUM is NP-complete.

Each result combines an honest serialized language, bounded certificate semantics, a fixed polynomial-time verifier, and a total polynomial-time reduction machine.

Implementation source

See the complete theorem-bearing source.

Definitions and proofs

CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.VertexCover.Instance

VERTEX-COVER uses the same honest graph-plus-target instance structure as general CLIQUE.

abbrev VertexCoverInstance := CliqueInstance

A finite set is a vertex cover when all of its vertices are in range and it contains at least one endpoint of every stored graph edge.

def IsVertexCover (I : CliqueInstance) (vertices : Finset Nat) : Prop :=
  (∀ v ∈ vertices, v < I.vertexCount) ∧
    ∀ e ∈ I.edges, e.1 ∈ vertices ∨ e.2 ∈ vertices

A graph-plus-k instance is a VERTEX-COVER yes-instance when it has a vertex cover containing at most k vertices.

def HasVertexCover (I : CliqueInstance) : Prop :=
  ∃ vertices : Finset Nat,
    vertices.card ≤ I.targetSize ∧ I.IsVertexCover vertices

CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.VertexCover.Language

General graph-plus-target VERTEX-COVER over the shared CliqueSym grammar.

def GeneralVERTEXCOVER : Language VertexCoverSym :=
  { input |
      ∃ I, decodeVertexCoverInstance input = some I ∧
        I.WellFormed ∧ I.HasVertexCover }

The textbook serialized VERTEX-COVER language.

abbrev VERTEXCOVER : Language VertexCoverSym := GeneralVERTEXCOVER

CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.VertexCover.NP

The honest serialized VERTEX-COVER language has a fixed polynomial-time verifier and quadratically bounded certificates.

theorem generalVERTEXCOVER_polyTimeVerifiable :
    PolyTimeVerifiable GeneralVERTEXCOVER := by
  refine ⟨vertexCoverCliqueVerifier, (Polynomial.X + 1) ^ 2, ?_, ?_⟩
  · exact ⟨Turing.VertexCover.VerifierMachine.computableInPolyTime⟩
  · intro input
    simpa [Polynomial.eval_add, Polynomial.eval_pow, Polynomial.eval_X] using
      mem_generalVERTEXCOVER_iff_exists_bounded_cliqueCertificate input

Textbook VERTEX-COVER belongs to NP.

theorem VERTEXCOVER_mem_ClassNP : VERTEXCOVER ∈ ClassNP VertexCoverSym :=
  (mem_ClassNP VERTEXCOVER).2 generalVERTEXCOVER_polyTimeVerifiable

CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.VertexCover.Reduction

The textbook graph-complement construction is a concrete polynomial-time many-one reduction from general CLIQUE to VERTEX-COVER.

theorem generalCLIQUE_reducible_to_VERTEXCOVER :
    PolyTimeReducible GeneralCLIQUE VERTEXCOVER := by
  refine ⟨cliqueToVertexCoverMap,
    ⟨Turing.VertexCover.ComplementMachine.Total.computableInPolyTime⟩, ?_⟩
  intro input
  exact (cliqueToVertexCoverMap_mem_VERTEXCOVER_iff input).symm

General VERTEX-COVER is NP-hard.

theorem VERTEXCOVER_npHard : NPHard VERTEXCOVER :=
  NPHard.of_reducible generalCLIQUE_npHard
    generalCLIQUE_reducible_to_VERTEXCOVER

CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.VertexCover.NPCompleteness

The honest serialized graph-plus-k VERTEX-COVER language is NP-complete.

theorem VERTEXCOVER_npComplete : NPComplete VERTEXCOVER :=
  ⟨generalVERTEXCOVER_polyTimeVerifiable, VERTEXCOVER_npHard⟩

CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.Instance

Finite undirected Hamiltonian-cycle instances

HAM-CYCLE reuses the chapter's normalized finite undirected graph structure. The existing targetSize field is required to equal vertexCount by the raw language, giving a canonical graph-only subgrammar without adding another alphabet. A cycle is represented by an ordered list of all vertices.

              namespace CLRS.Chapter34abbrev HamiltonianCycleInstance := CliqueInstanceabbrev HamiltonianCycleSym := CliqueSymabbrev encodeHamiltonianCycleInstance := encodeCliqueInstanceabbrev decodeHamiltonianCycleInstance := decodeCliqueInstancenamespace CliqueInstance

Adjacency of every consecutive pair along a list path.

def PathAdjacent (I : CliqueInstance) : List Nat → Prop
  | [] => True
  | [_] => True
  | u :: v :: rest => I.Adj u v ∧ I.PathAdjacent (v :: rest)

Last element of a nonempty list, expressed without proof arguments.

def lastFrom (current : Nat) : List Nat → Nat
  | [] => current
  | next :: rest => lastFrom next rest

Every path edge and the closing last-to-first edge are present.

def CycleAdjacent (I : CliqueInstance) : List Nat → Prop
  | [] => False
  | first :: rest =>
      I.PathAdjacent (first :: rest) ∧ I.Adj (lastFrom first rest) first

A list is a Hamiltonian cycle when it lists every vertex exactly once and all path and closing edges exist. Requiring at least three vertices matches the textbook simple-cycle convention.

def ListRepresentsHamiltonianCycle
    (I : CliqueInstance) (vertices : List Nat) : Prop :=
  3 ≤ I.vertexCount ∧
    vertices.Nodup ∧
    vertices.length = I.vertexCount ∧
    (∀ v ∈ vertices, v < I.vertexCount) ∧
    I.CycleAdjacent vertices

The graph has a Hamiltonian cycle.

def HasHamiltonianCycle (I : CliqueInstance) : Prop :=
  ∃ vertices, I.ListRepresentsHamiltonianCycle vertices

CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.Language

Canonical graph-only HAM-CYCLE instances use the shared graph encoding with targetSize = vertexCount.

def GeneralHAMCYCLE : Language HamiltonianCycleSym :=
  { input |
      ∃ I, decodeHamiltonianCycleInstance input = some I ∧
        I.WellFormed ∧ I.targetSize = I.vertexCount ∧
        I.HasHamiltonianCycle }

              theorem mem_generalHAMCYCLE_iff (input : List HamiltonianCycleSym) :
    input ∈ GeneralHAMCYCLE ↔
      ∃ I, decodeHamiltonianCycleInstance input = some I ∧
        I.WellFormed ∧ I.targetSize = I.vertexCount ∧
        I.HasHamiltonianCycle := by
  rfl

theorem encodeHamiltonianCycleInstance_mem_iff (I : HamiltonianCycleInstance) :
    encodeHamiltonianCycleInstance I ∈ GeneralHAMCYCLE ↔
      I.WellFormed ∧ I.targetSize = I.vertexCount ∧
        I.HasHamiltonianCycle := by
  constructor
  · rintro ⟨J, hdecode, hJ, htarget, hcycle⟩
    have hJI : J = I := by
      have : some J = some I := hdecode.symm.trans
        (decode_encodeCliqueInstance I)
      exact Option.some.inj this
    subst J
    exact ⟨hJ, htarget, hcycle⟩
  · rintro ⟨hI, htarget, hcycle⟩
    exact ⟨I, decode_encodeCliqueInstance I, hI, htarget, hcycle⟩abbrev HAMCYCLE : Language HamiltonianCycleSym := GeneralHAMCYCLEend CLRS.Chapter34

CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.NP

The honest serialized HAM-CYCLE language has a fixed polynomial-time verifier and quadratically bounded ordered-cycle certificates.

theorem generalHAMCYCLE_polyTimeVerifiable :
    PolyTimeVerifiable GeneralHAMCYCLE := by
  refine ⟨hamiltonianCycleVerifier, (Polynomial.X + 1) ^ 2, ?_, ?_⟩
  · exact ⟨Turing.HamiltonianCycle.VerifierMachine.computableInPolyTime⟩
  · intro input
    constructor
    · intro hmem
      rcases (mem_generalHAMCYCLE_iff_exists_bounded_certificate input).1 hmem
        with ⟨certificate, hlength, hverify⟩
      refine ⟨certificate, ?_, hverify⟩
      simpa [Polynomial.eval_add, Polynomial.eval_pow, Polynomial.eval_X] using
        hlength
    · rintro ⟨certificate, hlength, hverify⟩
      exact (mem_generalHAMCYCLE_iff_exists_bounded_certificate input).2
        ⟨certificate, by
          simpa [Polynomial.eval_add, Polynomial.eval_pow,
            Polynomial.eval_X] using hlength, hverify⟩

Textbook HAM-CYCLE belongs to NP.

theorem HAMCYCLE_mem_ClassNP : HAMCYCLE ∈ ClassNP HamiltonianCycleSym :=
  (mem_ClassNP HAMCYCLE).2 generalHAMCYCLE_polyTimeVerifiable

CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.NPCompleteness

The fixed guarded edge-gadget machine is a polynomial-time many-one reduction from the honest serialized VERTEX-COVER language to HAM-CYCLE.

theorem VERTEXCOVER_reducible_to_HAMCYCLE :
    PolyTimeReducible VERTEXCOVER HAMCYCLE := by
  refine ⟨Turing.HamiltonianCycle.ReductionMachine.RawTotal.machineVertexCoverToHamiltonianMap,
    ⟨Turing.HamiltonianCycle.ReductionMachine.computableInPolyTime⟩, ?_⟩
  intro input
  exact (Turing.HamiltonianCycle.ReductionMachine.RawTotal.machineVertexCoverToHamiltonianMap_mem_HAMCYCLE_iff
    input).symm

The honest serialized HAM-CYCLE language is NP-hard.

theorem HAMCYCLE_npHard : NPHard HAMCYCLE :=
  NPHard.of_reducible VERTEXCOVER_npHard
    VERTEXCOVER_reducible_to_HAMCYCLE

The honest serialized HAM-CYCLE language is NP-complete.

theorem HAMCYCLE_npComplete : NPComplete HAMCYCLE :=
  ⟨generalHAMCYCLE_polyTimeVerifiable, HAMCYCLE_npHard⟩

CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.TravelingSalesperson.Instance

A finite complete weighted graph together with a tour-cost budget.

structure TSPInstance where
  vertexCount : Nat
  budget : Nat
  weight : Fin vertexCount → Fin vertexCount → Nat

Read an edge weight using natural-number vertex names. Out-of-range names receive weight zero; valid tour certificates never use that fallback.

def edgeWeight (I : TSPInstance) (u v : Nat) : Nat :=
  if hu : u < I.vertexCount then
    if hv : v < I.vertexCount then
      I.weight ⟨u, hu⟩ ⟨v, hv⟩
    else 0
  else 0

Last element of a nonempty list, without carrying a proof argument.

def lastFrom (current : Nat) : List Nat → Nat
  | [] => current
  | next :: rest => lastFrom next rest

Cost of all consecutive edges in a vertex list.

def pathCost (I : TSPInstance) : List Nat → Nat
  | [] => 0
  | [_] => 0
  | u :: v :: rest => I.edgeWeight u v + I.pathCost (v :: rest)

Cost of the cyclic tour obtained by adding the last-to-first edge.

def tourCost (I : TSPInstance) : List Nat → Nat
  | [] => 0
  | first :: rest =>
      I.pathCost (first :: rest) + I.edgeWeight (lastFrom first rest) first

A decision-TSP certificate lists every vertex exactly once and has total cyclic cost at most the instance budget.

def ListRepresentsTour (I : TSPInstance) (vertices : List Nat) : Prop :=
  3 ≤ I.vertexCount ∧
    vertices.Nodup ∧
    vertices.length = I.vertexCount ∧
    (∀ v ∈ vertices, v < I.vertexCount) ∧
    I.tourCost vertices ≤ I.budget

The decision-TSP instance admits a tour within its budget.

def HasTour (I : TSPInstance) : Prop :=
  ∃ vertices, I.ListRepresentsTour vertices

CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.TravelingSalesperson.Encoding.Basic

Proof-free complete-matrix representation decoded from a finite word.

structure TSPData where
  vertexCount : Nat
  budget : Nat
  weights : List Nat
deriving DecidableEq, Repr

The matrix contains exactly one weight for every ordered vertex pair and the two orientations of every off-diagonal pair agree. This is the standard symmetric decision-TSP input model used by CLRS.

def WellFormed (data : TSPData) : Prop :=
  data.weights.length = data.vertexCount * data.vertexCount ∧
    OrientationPairsEqual (data.weights.drop data.vertexCount)

Interpret the canonical complete-pair order as the existing typed decision-TSP model. Malformed short matrices use a zero fallback, but the raw language separately requires WellFormed, so accepted instances never observe it.

def toInstance (data : TSPData) : TSPInstance where
  vertexCount := data.vertexCount
  budget := data.budget
  weight u v := lookupTSPWeight (tspPairOrder data.vertexCount)
    data.weights u.val v.val

Honest raw decision semantics.

def HasTour (data : TSPData) : Prop :=
  data.WellFormed ∧ data.toInstance.HasTour

CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.TravelingSalesperson.Language

A word belongs to decision-TSP exactly when it canonically decodes to a well-formed complete weight matrix admitting a tour within its budget.

def GeneralTSP : Language TSPSym :=
  { input | ∃ data, decodeTSPData input = some data ∧ data.HasTour }

Textbook name for the honest serialized decision problem.

abbrev TSP : Language TSPSym := GeneralTSP

CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.TravelingSalesperson.NP

The honest serialized decision-TSP language has a fixed polynomial-time verifier and quadratically bounded unary ordered-tour certificates.

theorem generalTSP_polyTimeVerifiable :
    PolyTimeVerifiable GeneralTSP := by
  refine ⟨fun certificate input =>
      Turing.TSPVerifier.Final.concreteTSPVerifier (certificate, input),
    (Polynomial.X + 1) ^ 2, ?_, ?_⟩
  · exact ⟨Turing.TSPVerifier.Final.computableInPolyTime⟩
  · intro input
    simpa [Polynomial.eval_add, Polynomial.eval_pow, Polynomial.eval_X] using
      mem_generalTSP_iff_exists_bounded_unary_certificate input

Textbook decision-TSP belongs to NP.

theorem TSP_mem_ClassNP : TSP ∈ ClassNP TSPSym :=
  (mem_ClassNP TSP).2 generalTSP_polyTimeVerifiable

CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.TravelingSalesperson.Hardness

The complete-matrix 1/2-weight construction is a concrete polynomial- time many-one reduction from honest serialized HAM-CYCLE to decision-TSP.

theorem HAMCYCLE_reducible_to_TSP :
    PolyTimeReducible HAMCYCLE TSP := by
  refine ⟨TSPReduction.rawHamiltonianToTSP,
    ⟨Turing.TSPReduction.RawTotal.computableInPolyTime⟩, ?_⟩
  intro input
  exact TSPReduction.rawHamiltonianToTSP_correct input

Honest serialized decision-TSP is NP-hard.

theorem TSP_npHard : NPHard TSP :=
  NPHard.of_reducible HAMCYCLE_npHard HAMCYCLE_reducible_to_TSP

CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.TravelingSalesperson.NPCompleteness

The honest serialized decision-TSP language is NP-complete.

theorem TSP_npComplete : NPComplete TSP :=
  ⟨generalTSP_polyTimeVerifiable, TSP_npHard⟩

CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.SubsetSum.Encoding.Basic

Proof-free indexed SUBSET-SUM data. List positions distinguish equal numerical values.

structure SubsetSumData where
  target : Nat
  values : List Nat
deriving DecidableEq, Repr

Sum the values at a list of selected indices. Out-of-range indices use zero, but accepted certificates separately prove the range condition.

def selectedSum (data : SubsetSumData) (indices : List Nat) : Nat :=
  (indices.map fun index => data.values.getD index 0).sum

Honest indexed subset semantics.

def HasSubsetSum (data : SubsetSumData) : Prop :=
  ∃ indices : List Nat,
    indices.Nodup ∧
      (∀ index ∈ indices, index < data.values.length) ∧
      data.selectedSum indices = data.target

CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.SubsetSum.Language

Raw compact SUBSET-SUM strings whose decoded indexed values admit an exact target subfamily.

def GeneralSUBSETSUM : Language SubsetSumSym :=
  { input | ∃ data,
      decodeSubsetSumData input = some data ∧ data.HasSubsetSum }

Textbook public name for the honest raw language.

abbrev SUBSETSUM : Language SubsetSumSym := GeneralSUBSETSUM

CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.SubsetSum.NP

General SUBSET-SUM is in NP

              namespace CLRS.Chapter34

private theorem exists_bounded_mask_certificate_of_mem
    {input : List SubsetSumSym} (hmem : input ∈ GeneralSUBSETSUM) :
    ∃ certificate,
      certificate.length ≤ input.length + 2 ∧
      Turing.SubsetSumVerifier.Final.concreteSubsetSumVerifier
        (certificate, input) = true := by
  rcases hmem with ⟨data, hdecode, hhas⟩
  rcases (hasSubsetSum_iff_exists_finset data).1 hhas with ⟨chosen, hsum⟩
  let mask := subsetMaskOfFinset chosen
  have hmask : data.MaskSumsTo mask := by
    rw [SubsetSumData.MaskSumsTo, subsetSumMaskOfFinset_sum]
    exact hsum
  refine ⟨encodeSubsetSumMask mask, ?_, ?_⟩
  · rw [encodeSubsetSumMask_length]
    have hmaskLength : mask.length = data.values.length := by
      simp [mask, subsetMaskOfFinset]
    rw [hmaskLength]
    exact Nat.add_le_add_right (subsetSum_valueCount_le_input_length hdecode) 2
  · exact
      (Turing.SubsetSumVerifier.Final.concreteSubsetSumVerifier_eq_true_iff
        _ _).2 ⟨data, mask, hdecode, rfl, hmask⟩theorem mem_generalSUBSETSUM_iff_exists_bounded_mask_certificate
    (input : List SubsetSumSym) :
    input ∈ GeneralSUBSETSUM ↔
      ∃ certificate,
        certificate.length ≤ input.length + 2 ∧
        Turing.SubsetSumVerifier.Final.concreteSubsetSumVerifier
          (certificate, input) = true := by
  constructor
  · exact exists_bounded_mask_certificate_of_mem
  · rintro ⟨certificate, _, haccept⟩
    exact
      (Turing.SubsetSumVerifier.Final.mem_generalSUBSETSUM_iff_exists_concrete_certificate
        input).2
        ⟨certificate, haccept⟩theorem generalSUBSETSUM_polyTimeVerifiable :
    PolyTimeVerifiable GeneralSUBSETSUM := by
  refine ⟨fun certificate input =>
      Turing.SubsetSumVerifier.Final.concreteSubsetSumVerifier
        (certificate, input),
    Polynomial.X + 2, ?_, ?_⟩
  · exact ⟨Turing.SubsetSumVerifier.Final.computableInPolyTime⟩
  · intro input
    simpa [Polynomial.eval_add, Polynomial.eval_X] using
      mem_generalSUBSETSUM_iff_exists_bounded_mask_certificate inputtheorem SUBSETSUM_mem_ClassNP : SUBSETSUM ∈ ClassNP SubsetSumSym :=
  (mem_ClassNP SUBSETSUM).2 generalSUBSETSUM_polyTimeVerifiableend CLRS.Chapter34

CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.SubsetSum.Hardness

The textbook digit construction is a concrete polynomial-time many-one reduction from serialized three-CNF satisfiability to honest SUBSET-SUM.

theorem threeCNFSat_reducible_to_SUBSETSUM :
    PolyTimeReducible ThreeCNFSat SUBSETSUM := by
  refine ⟨SubsetSumReduction.rawThreeCNFToSubsetSum,
    ⟨Turing.SubsetSumReduction.rawThreeCNFToSubsetSum_computableInPolyTime⟩,
    ?_⟩
  intro input
  exact SubsetSumReduction.rawThreeCNFToSubsetSum_correct input

Honest serialized SUBSET-SUM is NP-hard.

theorem SUBSETSUM_npHard : NPHard SUBSETSUM :=
  NPHard.of_reducible threeCNFSat_npHard
    threeCNFSat_reducible_to_SUBSETSUM

CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.SubsetSum.NPCompleteness

The honest serialized textbook SUBSET-SUM language is NP-complete.

theorem SUBSETSUM_npComplete : NPComplete SUBSETSUM :=
  ⟨generalSUBSETSUM_polyTimeVerifiable, SUBSETSUM_npHard⟩

Scope and implementation notes

Imports

import CLRSLean.FourthEdition.Chapter_34.Section_34_1_Polynomial_Time
import CLRSLean.FourthEdition.Chapter_34.Section_34_2_Polynomial_Time_Verification
import CLRSLean.FourthEdition.Chapter_34.Section_34_3_NP_Completeness_And_Reducibility
import CLRSLean.FourthEdition.Chapter_34.Section_34_4_NP_Completeness_Proofs
import CLRSLean.FourthEdition.Chapter_34.Section_34_5_NP_Complete_Problems

Chapter 34 develops the proof language of polynomial-time computation, verification, and reduction, then uses it to establish the textbook's main NP-completeness chain. The canonical reader is organized into the five CLRS sections below; implementation-heavy support modules remain available through the compatibility source links on each section page.

Chapter map

34.1 Polynomial Time introduces the deterministic polynomial-time machine model and closure properties of P.
34.2 Polynomial-Time Verification formalizes bounded certificates, verifiers, and P ⊆ NP.
34.3 NP-Completeness and Reducibility proves reduction transitivity and the transport rules for NP-hardness and NP-completeness.
34.4 NP-Completeness Proofs contains Cook--Levin and the reductions through SAT, 3-CNF-SAT, and CLIQUE.
34.5 NP-Complete Problems continues the chain through VERTEX-COVER, HAM-CYCLE, decision-TSP, and SUBSET-SUM.

Main theorem chain

The formalization packages the textbook argument in four layers:

Polynomial-time functions compose, P ⊆ NP, and polynomial-time many-one reductions are transitive.
Cook--Levin gives a fixed polynomial-time reduction from every NP language to a well-formed general-circuit satisfiability instance, establishing generalCircuitSAT_npComplete.
Concrete total reduction machines establish CIRCUIT-SAT ≤_P SAT ≤_P 3-CNF-SAT ≤_P CLIQUE; the public CLIQUE target is the honest serialized graph-plus-k language.
The selected §34.5 chain closes strict NP-completeness for VERTEX-COVER, HAM-CYCLE, decision-TSP, and SUBSET-SUM.

Coverage boundary

Status: main-proof-complete. Every represented section has an explicit reader page, concrete polynomial-time machines where the advertised reduction or verifier claim requires one, exact all-input semantic bridges, and the corresponding public NP-completeness theorem. Standalone SAT and 3-CNF-SAT now also have exact total assignment checkers, linear certificate bounds, reduction-backed fixed verifier machines, and public NP-completeness theorems. Directly lowering the smaller assignment checkers to machines remains an optional implementation refinement.

See docs/clrs-fourth-edition-map.csv for the section-level ledger, docs/migrations/clrs4.md for compatibility policy, and CLRSLean.Chapter_34, rendered as the complete compatibility chapter, for the full implementation module tree.

CLRS, fourth edition · Chapter 34 of 35