A 2-approximation for metric TSP

The minimum-spanning-tree tour Cslib.Algorithms.Lean.TSP.mstTour, run on the distance matrix of a TSP instance, visits every city exactly once, and on metric matrices its length is at most twice the length of every tour, in particular an optimal one ([WS11], Section 2.4).

Model

The cities, distances and tour lengths are those of Cslib.Complexity.TSP: the cities are the row indices 0, …, D.length - 1, distances are TSP.dist D, and TSP.tourLength D p is the length of the closed tour p. A matrix is metric (TSP.IsMetric) when the distances between cities are symmetric and satisfy the triangle inequality. The triangle inequality is required for all triples of cities, including those with i = k, so each diagonal entry is at most twice any distance from its city. Diagonal entries need not be zero ([WS11] assumes they are); the bound does not need that. Entries outside the city range are irrelevant.

Main definitions

• Cslib.Complexity.TSP.IsMetric: symmetric distances with the triangle inequality.
• Cslib.Complexity.TSP.approxTour: the minimum-spanning-tree tour of the cities.

Main results

• approxTour_perm: the tour visits every city exactly once.
• exists_map_val_eq_of_perm_range: a permutation of the cities is a duplicate-free list of all of Fin n, which transfers bounds stated for tours over Fin n.
• tourLength_approxTour_le_two_mul: on metric matrices, the tour has length at most twice the length of any tour.
• tourLength_approxTour_le_two_mul_of_mem: if x ∈ TSP with x.dist metric, the tour has length at most 2 * x.bound.

Limitations

No machine-level running time is certified for approxTour; that requires a polynomial-time certificate for Kruskal's algorithm on encoded matrices.

References

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

structure Cslib.Complexity.TSP.IsMetric (D : List (List ℕ)) : Prop

A distance matrix is metric when the distances between its cities are symmetric and satisfy the triangle inequality. The triangle inequality covers all triples, including i = k, so each diagonal entry is at most twice any distance from its city; diagonal entries need not be zero.

• symm (i : ℕ) : i < D.length → ∀ j < D.length, dist D i j = dist D j i

  Distances between cities are symmetric.

• triangle (i : ℕ) : i < D.length → ∀ j < D.length, ∀ k < D.length, dist D i k ≤ dist D i j + dist D j k

  Distances between cities satisfy the triangle inequality.

def Cslib.Complexity.TSP.finDist (D : List (List ℕ)) (i j : Fin D.length) : ℕ

The distances between the cities of D, indexed by Fin D.length.

def Cslib.Complexity.TSP.approxTour (D : List (List ℕ)) : List ℕ

The MST tour of the cities of D: grow a tour from city 0 along Kruskal's minimum spanning tree of the complete graph on the cities.

theorem Cslib.Complexity.TSP.tourLength_map_val (D : List (List ℕ)) (q : List (Fin D.length)) : tourLength D (List.map Fin.val q) = Algorithms.Lean.TSP.cycleCost (finDist D) q

Tour lengths of city lists are closed-walk costs.

theorem Cslib.Complexity.TSP.approxTour_perm (D : List (List ℕ)) : (approxTour D).Perm (List.range D.length)

Feasibility. The MST tour visits every city exactly once.

theorem Cslib.Complexity.TSP.exists_map_val_eq_of_perm_range {n : ℕ} {p : List ℕ} (hp : p.Perm (List.range n)) : ∃ (q : List (Fin n)), List.map Fin.val q = p ∧ q.Nodup ∧ ∀ (x : Fin n), x ∈ q

A tour given as a permutation of the cities 0, …, n - 1 lists every element of Fin n exactly once.

theorem Cslib.Complexity.TSP.tourLength_approxTour_le_two_mul {D : List (List ℕ)} (hD : IsMetric D) {p : List ℕ} (hp : p.Perm (List.range D.length)) : tourLength D (approxTour D) ≤ 2 * tourLength D p

The 2-approximation for metric TSP ([WS11], Section 2.4): on a metric matrix, the MST tour has length at most twice the length of any tour, in particular an optimal one.

theorem Cslib.Complexity.TSP.tourLength_approxTour_le_two_mul_of_mem {x : TSPInstance} (hx : IsMetric x.dist) (h : x ∈ TSP) : tourLength x.dist (approxTour x.dist) ≤ 2 * x.bound

The 2-approximation against the decision problem: if a metric instance x belongs to TSP, the MST tour has length at most 2 * x.bound.