2.8. Proving a Problem NP-Complete🔗

A proof that a problem is NP-complete has five parts: a verifier, its cost, a reduction from a known NP-complete problem, the reduction's cost, and the combination. Here they are for Clique, following Complexity/Computability/Complexity/Problems/Clique.lean.

2.8.1. The Problem🔗

An instance is a graph and a target size. The graph has a clique of that size when some set of its declared vertices is pairwise adjacent and has exactly that many elements:

example : Clique = {x | ∃ S : Finset ℕ,
    (∀ v ∈ S, v ∈ x.1.1) ∧ x.1.toSimpleGraph.IsNClique x.2 S} :=
  rfl

2.8.2. The Verifier🔗

The certificate is a mask over the vertex list. The verifier keeps the masked vertices, checks that there are as many as the target, and checks that each two of them are adjacent. Graph problems that ask for a set of vertices with a pairwise property share this verifier, Graph.verifySubset, and its correctness lemma Graph.isVerifier_verifySubset, which leaves only the pairwise test to check:

example : IsVerifier (encPair encGraph encNat) Polynomial.X
    Clique.verifier Clique := by⊢ IsVerifier (encPair encGraph encNat) Polynomial.X Clique.verifier Clique
  have h := Graph.isVerifier_verifySubset (rel := Graph.adjBool)
    (P := fun G u v => G.toSimpleGraph.Adj u v)
    (fun G u v _ => byG:Graphu:ℕv:ℕx✝:u ≠ v⊢ G.adjBool u v = true ↔ G.toSimpleGraph.Adj u v rw [Graph.adjBool_eq_true_iffG:Graphu:ℕv:ℕx✝:u ≠ v⊢ G.toSimpleGraph.Adj u v ↔ G.toSimpleGraph.Adj u v]All goals completed! 🐙)h:IsVerifier (encPair encGraph encNat) Polynomial.X (Graph.verifySubset Graph.adjBool)
  {x | ∃ S, (∀ v ∈ S, v ∈ x.1.1) ∧ ((↑S).Pairwise fun u v => x.1.toSimpleGraph.Adj u v) ∧ S.card = x.2}⊢ IsVerifier (encPair encGraph encNat) Polynomial.X Clique.verifier Clique
  intro xh:IsVerifier (encPair encGraph encNat) Polynomial.X (Graph.verifySubset Graph.adjBool)
  {x | ∃ S, (∀ v ∈ S, v ∈ x.1.1) ∧ ((↑S).Pairwise fun u v => x.1.toSimpleGraph.Adj u v) ∧ S.card = x.2}x:Graph × ℕ⊢ x ∈ Clique ↔
  ∃ w, w.length = Polynomial.eval ((encPair encGraph encNat) x).length Polynomial.X ∧ Clique.verifier (x, w) = true
  simpa only [Clique, Set.mem_ofPred_eq, SimpleGraph.isNClique_iff,
    SimpleGraph.IsClique, Clique.verifier] using h xAll goals completed! 🐙

The certificate length is Polynomial.X, one bit per bit of the encoded instance, which is at least one bit per vertex. The verifier is executable, so you can test it on a triangle:

true#eval Clique.verifier
  ((([0, 1, 2], [(0, 1), (1, 2), (0, 2)]), 3), [true, true, true])

true

2.8.3. The Verifier's Cost🔗

The verifier is written with certified operations, so its cost is automatic, and the two parts give membership in NP:

example : ComputableInPolyTime Clique.verifier
    (encPair (encPair encGraph encNat) encBits) encBool := by⊢ ComputableInPolyTime Clique.verifier (encPair (encPair encGraph encNat) encBits) encBool
  fun_propAll goals completed! 🐙

example : Clique ∈ NP (encPair encGraph encNat) :=
  ⟨Polynomial.X, Clique.verifier, by⊢ ComputableInPolyTime Clique.verifier (encPair (encPair encGraph encNat) encBits) encBool fun_propAll goals completed! 🐙, Clique.isVerifier⟩

2.8.4. The Reduction🔗

A set of vertices is independent in a graph exactly when it is a clique in the complement graph on the same vertices (Graph.compl), so complementing reduces IndependentSet to Clique. The correctness half is Graph.compl_mem_Clique_iff. The complement keeps every pair of distinct declared vertices that no edge joins:

example (G : Graph) : G.compl = (G.1, G.1.flatMap fun u =>
    (G.1.filter fun v => decide (u ≠ v ∧ (u, v) ∉ G.2 ∧ (v, u) ∉ G.2)).map
      fun v => (u, v)) :=
  rfl

2.8.5. The Reduction's Cost🔗

Unfolding the complement exposes list operations and membership tests, which polytime certifies:

example : ComputableInPolyTime Graph.compl encGraph encGraph := by⊢ ComputableInPolyTime Graph.compl encGraph encGraph
  unfold Graph.compl⊢ ComputableInPolyTime
  (fun G =>
    (G.1,
      List.flatMap
        (fun u => List.map (fun v => (u, v)) (List.filter (fun v => decide (u ≠ v ∧ (u, v) ∉ G.2 ∧ (v, u) ∉ G.2)) G.1))
        G.1))
  encGraph encGraph
  polytimeAll goals completed! 🐙

2.8.6. Putting It Together🔗

The reduction is the triple of map, cost and correctness. Hardness transfers from IndependentSet, and membership with hardness is completeness:

example : PolyTimeReducible (encPair encGraph encNat)
    (encPair encGraph encNat) IndependentSet Clique :=
  ⟨fun x => (x.1.compl, x.2), by⊢ ComputableInPolyTime (fun x => (x.1.compl, x.2)) (encPair encGraph encNat) (encPair encGraph encNat) fun_propAll goals completed! 🐙,
    fun ⟨G, m⟩ => (Graph.compl_mem_Clique_iff G m).symm⟩

example : NPComplete (encPair encGraph encNat) Clique :=
  ⟨Clique.mem_NP,
    IndependentSet_npHard.trans polyTimeReducible_IndependentSet_Clique⟩

A new problem follows the same outline. Define it with its encoding, give a verifier and prove IsVerifier, certify the verifier, give a reduction map from a problem in the catalogue and prove it correct, certify the map, and combine. Put it in its own module under Complexity/Computability/Complexity/Problems/, next to the problems it reduces from.