34.5. NP-Complete Problems

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⟩