A minimum-spanning-tree 2-approximation for metric TSP

This module formalizes a 2-approximation for the metric traveling salesman problem built on a minimum spanning tree ([WS11], Section 2.4). The algorithm computes a minimum spanning tree of the complete graph with Kruskal's algorithm (kruskalEdges), then grows a tour from vertex 0: while some tree edge has exactly one endpoint on the tour, the other endpoint is inserted immediately after it.

Model

Vertices are Fin n and δ : Fin n → Fin n → ℕ is an arbitrary cost function. The cost of a closed walk visiting the entries of a list in order is cycleCost δ t (CslibFrontier.Algorithms.Lean.TSP.Walk). The approximation bound assumes only that δ is symmetric and satisfies the triangle inequality for all triples, including i = k, so each diagonal entry is at most twice any cost from its vertex; diagonal entries need not be zero. Costs are natural numbers, hence nonnegative.

Source mapping

[WS11], Section 2.4, proves Lemma 2.10 (a minimum spanning tree costs at most an optimal tour) by deleting an edge of the tour. Here totalWeight_kruskalEdges_le_cycleCost instead compares Kruskal's tree with a spanning forest of the tour's edges, which needs no edge deletion. Theorem 2.11 (nearest addition is a 2-approximation) charges each insertion of a city j after i at most c_ij + c_ji = 2 c_ij, by the triangle inequality; summed over the edges of the spanning tree built by Prim's algorithm, the tour costs at most twice the tree. The same charging argument applies to any spanning tree whose edges guide the insertions, so mstTour uses the tree computed by the library's Kruskal implementation (cycleCost_insertAfter_le, cycleCost_mstTour_le_two_mul_totalWeight). Like the double-tree algorithm of Theorem 2.12, it computes the tree first and then derives the tour from it.

Limitations

The algorithm is a pure Lean function; no machine-level running time is certified. The bound is stated against every tour, in particular an optimal one.

Main definitions

• Cslib.Algorithms.Lean.TSP.insertAfter: insertion immediately after a given vertex.
• Cslib.Algorithms.Lean.TSP.growTour: grow a tour along the edges of a forest.
• Cslib.Algorithms.Lean.TSP.completeEdges: the complete graph weighted by δ.
• Cslib.Algorithms.Lean.TSP.mstTour: the tour grown along Kruskal's minimum spanning tree.

Main results

• cycleCost_insertAfter_le: an insertion costs at most δ u v + δ v u (triangle inequality).
• mstTour_perm: mstTour δ visits every vertex exactly once.
• totalWeight_kruskalEdges_completeEdges_le: Kruskal's tree on the complete graph weighs at most any duplicate-free connected list of its edges.
• totalWeight_kruskalEdges_le_cycleCost: the minimum spanning tree costs at most any tour.
• cycleCost_mstTour_le_two_mul_totalWeight: for n ≥ 2, the tour costs at most twice the tree.
• cycleCost_mstTour_le_two_mul: for symmetric δ with the triangle inequality, the tour costs at most twice any tour.

References

• D. P. Williamson and D. B. Shmoys, The Design of Approximation Algorithms, Section 2.4.

Closed walks and insertion

theorem Cslib.Algorithms.Lean.TSP.cycleCost_append_cons_cons_le {α : Type u_1} (δ : α → α → ℕ) (htri : ∀ (x y z : α), δ x z ≤ δ x y + δ y z) (A B : List α) (u v : α) : cycleCost δ (A ++ u :: v :: B) ≤ cycleCost δ (A ++ u :: B) + (δ u v + δ v u)

The insertion step ([WS11], proof of Theorem 2.11): inserting v right after u in a closed walk costs at most δ u v + δ v u, by the triangle inequality.

def Cslib.Algorithms.Lean.TSP.insertAfter {α : Type u_1} [DecidableEq α] (u v : α) : List α → List α

Insert v immediately after the first occurrence of u in t (at the end if u ∉ t).

theorem Cslib.Algorithms.Lean.TSP.exists_eq_insertAfter {α : Type u_1} [DecidableEq α] {u : α} (v : α) {t : List α} (hu : u ∈ t) : ∃ (A : List α) (B : List α), t = A ++ u :: B ∧ insertAfter u v t = A ++ u :: v :: B

Inserting after a vertex of the walk splits the walk at that vertex.

theorem Cslib.Algorithms.Lean.TSP.insertAfter_perm {α : Type u_1} [DecidableEq α] {u : α} (v : α) {t : List α} (hu : u ∈ t) : (insertAfter u v t).Perm (v :: t)

Inserting after a vertex of the walk adds exactly the inserted vertex.

theorem Cslib.Algorithms.Lean.TSP.cycleCost_insertAfter_le {α : Type u_1} [DecidableEq α] (δ : α → α → ℕ) (htri : ∀ (x y z : α), δ x z ≤ δ x y + δ y z) {u : α} (v : α) {t : List α} (hu : u ∈ t) : cycleCost δ (insertAfter u v t) ≤ cycleCost δ t + (δ u v + δ v u)

The insertion bound ([WS11], proof of Theorem 2.11): inserting v after a vertex u of a closed walk raises its cost by at most δ u v + δ v u.

Growing a tour along a forest

def Cslib.Algorithms.Lean.TSP.crosses {n : ℕ} {W : Type} (t : List (Fin n)) (e : Kruskal.WeightedEdge n W) : Bool

Whether exactly one endpoint of e is on the tour t.

theorem Cslib.Algorithms.Lean.TSP.crosses_eq_true_iff {n : ℕ} {W : Type} {t : List (Fin n)} {e : Kruskal.WeightedEdge n W} : crosses t e = true ↔ ¬(e.u ∈ t ↔ e.v ∈ t)

def Cslib.Algorithms.Lean.TSP.growStep {n : ℕ} {W : Type} (t : List (Fin n)) (e : Kruskal.WeightedEdge n W) : List (Fin n)

Insert the endpoint of e that is off the tour immediately after the endpoint on it.

def Cslib.Algorithms.Lean.TSP.growTour {n : ℕ} {W : Type} (F : List (Kruskal.WeightedEdge n W)) : ℕ → List (Fin n) → List (Fin n)

Growing a tour along F: while some edge of F has exactly one endpoint on the tour, insert its other endpoint right after it, the first such edge of F first; at most k insertions.

theorem Cslib.Algorithms.Lean.TSP.growStep_spec {n : ℕ} {W : Type} {t : List (Fin n)} {e : Kruskal.WeightedEdge n W} (he : crosses t e = true) : ∃ (a : Fin n) (b : Fin n), (a = e.u ∧ b = e.v ∨ a = e.v ∧ b = e.u) ∧ a ∈ t ∧ b ∉ t ∧ growStep t e = insertAfter a b t

A crossing step inserts the endpoint b off the tour right after the endpoint a on it.

theorem Cslib.Algorithms.Lean.TSP.nodup_growTour {n : ℕ} {W : Type} (F : List (Kruskal.WeightedEdge n W)) (k : ℕ) {t : List (Fin n)} (ht : t.Nodup) : (growTour F k t).Nodup

Growing keeps the tour free of repetitions.

theorem Cslib.Algorithms.Lean.TSP.mem_growTour {n : ℕ} {W : Type} {F : List (Kruskal.WeightedEdge n W)} (hF : ∀ (a b : Fin n), Relation.EqvGen (fun (x y : Fin n) => ∃ e ∈ F, x = e.u ∧ y = e.v) a b) {k : ℕ} {t : List (Fin n)} (ht : t.Nodup) (hne : t ≠ []) (hk : n ≤ t.length + k) (x : Fin n) : x ∈ growTour F k t

Coverage. If the edges of F connect all of Fin n and there is fuel for n vertices, growing a nonempty tour without repetitions reaches every vertex.

The charging argument

The algorithm

def Cslib.Algorithms.Lean.TSP.completeEdges {n : ℕ} (δ : Fin n → Fin n → ℕ) : List (Kruskal.WeightedEdge n ℕ)

The complete graph on Fin n, the edge from i to j weighted by δ i j.

theorem Cslib.Algorithms.Lean.TSP.mem_completeEdges {n : ℕ} {δ : Fin n → Fin n → ℕ} {e : Kruskal.WeightedEdge n ℕ} : e ∈ completeEdges δ ↔ e.weight = δ e.u e.v

def Cslib.Algorithms.Lean.TSP.mstTour {n : ℕ} (δ : Fin n → Fin n → ℕ) : List (Fin n)

The MST tour: grow a tour from vertex 0 along the minimum spanning tree that Kruskal's algorithm computes on the complete graph weighted by δ.

theorem Cslib.Algorithms.Lean.TSP.mstTour_of_pos {n : ℕ} (δ : Fin n → Fin n → ℕ) (h : 0 < n) : mstTour δ = growTour (Kruskal.kruskalEdges (completeEdges δ)) n [⟨0, h⟩]

theorem Cslib.Algorithms.Lean.TSP.eqvGen_kruskalEdges_completeEdges {n : ℕ} (δ : Fin n → Fin n → ℕ) (a b : Fin n) : Relation.EqvGen (fun (x y : Fin n) => ∃ e ∈ Kruskal.kruskalEdges (completeEdges δ), x = e.u ∧ y = e.v) a b

Kruskal's tree on the complete graph connects all vertices.

theorem Cslib.Algorithms.Lean.TSP.mstTour_perm {n : ℕ} (δ : Fin n → Fin n → ℕ) : (mstTour δ).Perm (List.finRange n)

Feasibility. The MST tour visits every vertex exactly once.

theorem Cslib.Algorithms.Lean.TSP.cycleCost_mstTour_le_two_mul_totalWeight {n : ℕ} {δ : Fin n → Fin n → ℕ} (hsymm : ∀ (x y : Fin n), δ x y = δ y x) (htri : ∀ (x y z : Fin n), δ x z ≤ δ x y + δ y z) (hn : 2 ≤ n) : cycleCost δ (mstTour δ) ≤ 2 * Kruskal.totalWeight (Kruskal.kruskalEdges (completeEdges δ))

The upper bound ([WS11], proof of Theorem 2.11): for symmetric δ with the triangle inequality and at least two vertices, the MST tour costs at most twice the tree.

The lower bound

theorem Cslib.Algorithms.Lean.TSP.totalWeight_kruskalEdges_completeEdges_le {n : ℕ} (δ : Fin n → Fin n → ℕ) {H : List (Kruskal.WeightedEdge n ℕ)} (hHnd : H.Nodup) (hHw : ∀ e ∈ H, e.weight = δ e.u e.v) (hconn : ∀ (x y : Fin n), Relation.EqvGen (fun (a b : Fin n) => ∃ e ∈ H, a = e.u ∧ b = e.v) x y) : Kruskal.totalWeight (Kruskal.kruskalEdges (completeEdges δ)) ≤ Kruskal.totalWeight H

Kruskal's tree on the complete graph weighs at most any duplicate-free list of its edges that connects all vertices.

theorem Cslib.Algorithms.Lean.TSP.totalWeight_kruskalEdges_le_cycleCost {n : ℕ} (δ : Fin n → Fin n → ℕ) {q : List (Fin n)} (hq : q.Nodup) (hcov : ∀ (x : Fin n), x ∈ q) : Kruskal.totalWeight (Kruskal.kruskalEdges (completeEdges δ)) ≤ cycleCost δ q

The lower bound ([WS11], Lemma 2.10): the minimum spanning tree of the complete graph costs at most any closed walk visiting every vertex exactly once. The tour's edges form a connected subgraph of the complete graph, so Kruskal's forest of them is a spanning forest, which weighs at least the minimum spanning tree and at most the tour.

The factor 2

theorem Cslib.Algorithms.Lean.TSP.cycleCost_mstTour_le_two_mul {n : ℕ} {δ : Fin n → Fin n → ℕ} (hsymm : ∀ (x y : Fin n), δ x y = δ y x) (htri : ∀ (x y z : Fin n), δ x z ≤ δ x y + δ y z) {q : List (Fin n)} (hq : q.Nodup) (hcov : ∀ (x : Fin n), x ∈ q) : cycleCost δ (mstTour δ) ≤ 2 * cycleCost δ q

The MST 2-approximation for metric TSP ([WS11], Section 2.4): for symmetric δ with the triangle inequality, the MST tour costs at most twice any closed walk visiting every vertex exactly once, in particular an optimal tour.