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