34.4. NP-Completeness 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