2.9. 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 CslibFrontier/Computability/Complexity/Problems/Clique.lean.
2.9.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 // v ∈ x.graph.vertices},
x.graph.induced.IsNClique x.m S} :=
rfl
2.9.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 encCliqueInstance Polynomial.X
Clique.verifier Clique := ⊢ IsVerifier encCliqueInstance Polynomial.X Clique.verifier Clique
h:IsVerifier (encPair encGraph encNat) Polynomial.X (Graph.verifySubset Graph.adjBool)
{x | ∃ S, ((↑S).Pairwise fun u v => x.1.toSimpleGraph.Adj ↑u ↑v) ∧ S.card = x.2}⊢ IsVerifier encCliqueInstance Polynomial.X Clique.verifier Clique
h:IsVerifier (encPair encGraph encNat) Polynomial.X (Graph.verifySubset Graph.adjBool)
{x | ∃ S, ((↑S).Pairwise fun u v => x.1.toSimpleGraph.Adj ↑u ↑v) ∧ S.card = x.2}x:CliqueInstance⊢ x ∈ Clique ↔ ∃ w, w.length = Polynomial.eval (encCliqueInstance x).length Polynomial.X ∧ Clique.verifier (x, w) = true
h:IsVerifier (encPair encGraph encNat) Polynomial.X (Graph.verifySubset Graph.adjBool)
{x | ∃ S, ((↑S).Pairwise fun u v => x.1.toSimpleGraph.Adj ↑u ↑v) ∧ S.card = x.2}x:CliqueInstancehx:(x.graph, x.m) ∈ {x | ∃ S, ((↑S).Pairwise fun u v => x.1.toSimpleGraph.Adj ↑u ↑v) ∧ S.card = x.2} ↔
∃ w,
w.length = Polynomial.eval ((encPair encGraph encNat) (x.graph, x.m)).length Polynomial.X ∧
Graph.verifySubset Graph.adjBool ((x.graph, x.m), w) = true⊢ x ∈ Clique ↔ ∃ w, w.length = Polynomial.eval (encCliqueInstance x).length Polynomial.X ∧ Clique.verifier (x, w) = true
h:IsVerifier (encPair encGraph encNat) Polynomial.X (Graph.verifySubset Graph.adjBool)
{x | ∃ S, ((↑S).Pairwise fun u v => x.1.toSimpleGraph.Adj ↑u ↑v) ∧ S.card = x.2}x:CliqueInstancehx:(x.graph, x.m) ∈ {x | ∃ S, ((↑S).Pairwise fun u v => x.1.toSimpleGraph.Adj ↑u ↑v) ∧ S.card = x.2} ↔
∃ w,
w.length = Polynomial.eval ((encPair encGraph encNat) (x.graph, x.m)).length Polynomial.X ∧
Graph.verifySubset Graph.adjBool ((x.graph, x.m), w) = true⊢ (∃ S, (↑S).Pairwise x.graph.induced.Adj ∧ S.card = x.m) ↔
∃ w,
w.length = Polynomial.eval (encCliqueInstance x).length Polynomial.X ∧
Graph.verifySubset Graph.adjBool ((x.graph, x.m), w) = true
h:IsVerifier (encPair encGraph encNat) Polynomial.X (Graph.verifySubset Graph.adjBool)
{x | ∃ S, ((↑S).Pairwise fun u v => x.1.toSimpleGraph.Adj ↑u ↑v) ∧ S.card = x.2}x:CliqueInstancehx:(x.graph, x.m) ∈ {x | ∃ S, ((↑S).Pairwise fun u v => x.1.toSimpleGraph.Adj ↑u ↑v) ∧ S.card = x.2} ↔
∃ w,
w.length = Polynomial.eval ((encPair encGraph encNat) (x.graph, x.m)).length Polynomial.X ∧
Graph.verifySubset Graph.adjBool ((x.graph, x.m), w) = true⊢ (∃ S, (↑S).Pairwise x.graph.induced.Adj ∧ S.card = x.m) ↔
∃ w,
w.length = Polynomial.eval (encCliqueInstanceFields (x.graph, x.m)).length Polynomial.X ∧
Graph.verifySubset Graph.adjBool ((x.graph, x.m), w) = true
All 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:
#eval Clique.verifier
(⟨⟨[0, 1, 2], [(0, 1), (1, 2), (0, 2)]⟩, 3⟩, [true, true, true])
2.9.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 encCliqueInstance encBits) encBool := ⊢ ComputableInPolyTime Clique.verifier (encPair encCliqueInstance encBits) encBool
All goals completed! 🐙
example : Clique ∈ NP encCliqueInstance :=
⟨Polynomial.X, Clique.verifier, ⊢ ComputableInPolyTime Clique.verifier (encPair encCliqueInstance encBits) encBool All goals completed! 🐙, Clique.isVerifier⟩
2.9.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.vertices, G.vertices.flatMap fun u =>
(G.vertices.filter fun v =>
decide (u ≠ v ∧ (u, v) ∉ G.edges ∧ (v, u) ∉ G.edges)).map
fun v => (u, v)⟩ :=
rfl
2.9.5. The Reduction's Cost
Unfolding the complement exposes list operations and membership tests, which polytime
certifies:
example : ComputableInPolyTime Graph.compl encGraph encGraph := ⊢ ComputableInPolyTime Graph.compl encGraph encGraph
⊢ ComputableInPolyTime
(fun G =>
{ vertices := G.vertices,
edges :=
List.flatMap
(fun u =>
List.map (fun v => (u, v))
(List.filter (fun v => decide (u ≠ v ∧ (u, v) ∉ G.edges ∧ (v, u) ∉ G.edges)) G.vertices))
G.vertices })
encGraph encGraph
All goals completed! 🐙
2.9.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 encIndependentSetInstance
encCliqueInstance IndependentSet Clique :=
⟨independentSetToClique, computableInPolyTime_independentSetToClique,
fun x => (independentSetToClique_mem_iff x).symm⟩
example : NPComplete encCliqueInstance 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
CslibFrontier/Computability/Complexity/Problems/, next to the problems it reduces from.