The traveling salesman problem

TSP is the decision version of the traveling salesman problem Papadimitriou, Section 9.3: an instance x : TSPInstance is a distance matrix x.dist, given as a list of rows (row i lists the distances from city i), together with a budget x.bound, and it belongs to TSP when some closed tour visiting every city exactly once has length at most x.bound. The conventions are the following.

• The cities are the row indices 0, …, D.length - 1. Rows may have any length: an entry missing from a ragged or short matrix reads 0 (TSP.dist).
• Distances need not be symmetric, and the diagonal entries are only used by the tour of a single city, which costs TSP.dist D 0 0. The matrix without rows is a yes-instance, through the empty tour of length 0.
• A tour is a permutation p of the cities, and its length TSP.tourLength D p is the sum of the distances from each city of p to the next one, the last city returning to the first.
• Distances and the budget are binary (encTSP).

TSP is in NP. As for the Hamiltonian problems, a certificate names an ordering of the cities, decoded by Graph.decodeVertexList from the list 0, …, D.length - 1 of cities; it has length m ^ 2 for instances of encoded length m. The verifier checks that the ordering lists every city exactly once, and compares the length of its tour with the budget using the binary arithmetic of CslibFrontier/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Binary.lean, so distances and budgets of any size are handled without unary expansion.

The reduction HamCycle.toTSP from HamCycle takes the distinct declared vertices of a graph as cities, at distance 1 when they are adjacent and 2 otherwise, with the number n of cities as the budget. A closed tour has n steps of length at least 1, so it has length at most n exactly when every step joins adjacent vertices, that is, when it is a Hamiltonian cycle. Graphs with fewer than three vertices have no Hamiltonian cycle and are mapped to a fixed no-instance.

Main definitions

• Cslib.Complexity.TSPInstance, Cslib.Complexity.encTSP: traveling salesman instances and their binary encoding.
• Cslib.Complexity.TSP.dist, Cslib.Complexity.TSP.tourLength, Cslib.Complexity.TSP.
• Cslib.Complexity.TSP.verifier.
• Cslib.Complexity.HamCycle.toTSP.

Main results

• Cslib.Complexity.TSP.tourLength_eq_sum: the tour length as a sum over the positions of the tour.
• Cslib.Complexity.TSP.computableInPolyTime_tourLength: tour lengths are polynomial-time.
• Cslib.Complexity.TSP.isVerifier, Cslib.Complexity.TSP.mem_NP: TSP ∈ NP encTSP.
• Cslib.Complexity.HamCycle.toTSP_mem_iff: toTSP G ∈ TSP ↔ G ∈ HamCycle.
• Cslib.Complexity.HamCycle.computableInPolyTime_toTSP: the reduction is polynomial-time.
• Cslib.Complexity.polyTimeReducible_HamCycle_TSP, Cslib.Complexity.TSP_npHard: HamCycle reduces to TSP in polynomial time, so TSP is NP-hard.
• Cslib.Complexity.TSP_npComplete: TSP is NP-complete.

References

• M. R. Garey and D. S. Johnson, Computers and Intractability
• C. H. Papadimitriou, Computational Complexity

structure Cslib.Complexity.TSPInstance : Type

An instance of the traveling salesman problem: a distance matrix dist given by its rows and a closed-tour budget bound.

• dist : List (List ℕ)

  The distance matrix, where row i entry j gives the distance from city i to city j.

• bound : ℕ

  The maximum allowed total tour length.

@[instance_reducible]

instance Cslib.Complexity.instDecidableEqTSPInstance : DecidableEq TSPInstance

def Cslib.Complexity.instDecidableEqTSPInstance.decEq (x✝ x✝¹ : TSPInstance) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.instReprTSPInstance : Repr TSPInstance

def Cslib.Complexity.instReprTSPInstance.repr : TSPInstance → ℕ → Std.Format

theorem Cslib.Complexity.encTSP_bound_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → TSPInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encTSP S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).bound) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.encTSP_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → List (List ℕ)} {x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn Turing.MultiTapeTM.encNat budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { dist := x0 x, bound := x1 x }) encIn encTSP budget

theorem Cslib.Complexity.encTSP_bound_inO : Turing.MultiTapeTM.ComputableInO TSPInstance.bound encTSP Turing.MultiTapeTM.encNat (fun (a : TSPInstance) => (encTSP a).length) fun (a : TSPInstance) => (encTSP a).length

theorem Cslib.Complexity.encTSP_dist_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → TSPInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encTSP → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).dist) encIn✝ (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))

theorem Cslib.Complexity.encTSP_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : List (List ℕ) × ℕ) => { dist := p.1, bound := p.2 }) encTSPFields encTSP 1 1

theorem Cslib.Complexity.encTSP_dist_deg : Turing.MultiTapeTM.ComputableInDegree TSPInstance.dist encTSP (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) 1 1

@[simp]

theorem Cslib.Complexity.encTSP_apply (a : TSPInstance) : encTSP a = encTSPFields (a.dist, a.bound)

theorem Cslib.Complexity.encTSP_dist_inO : Turing.MultiTapeTM.ComputableInO TSPInstance.dist encTSP (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (fun (a : TSPInstance) => (encTSP a).length) fun (a : TSPInstance) => (encTSP a).length

theorem Cslib.Complexity.encTSP_bound_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → TSPInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encTSP → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).bound) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.encTSP_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → List (List ℕ)} {x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { dist := x0 x, bound := x1 x }) encIn encTSP

theorem Cslib.Complexity.encTSP_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → List (List ℕ)} {T0 S0 x1 T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn Turing.MultiTapeTM.encNat T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { dist := x0 x, bound := x1 x }) encIn encTSP (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Cslib.Complexity.encTSP_dist_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → TSPInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encTSP S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).dist) encIn✝ (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) S✝

@[reducible, inline]

abbrev Cslib.Complexity.encTSPFields : List (List ℕ) × ℕ ↪ List Bool

The tuple of the fields of encTSP.

theorem Cslib.Complexity.encTSP_bound_deg : Turing.MultiTapeTM.ComputableInDegree TSPInstance.bound encTSP Turing.MultiTapeTM.encNat 1 1

def Cslib.Complexity.encTSP : TSPInstance ↪ List Bool

Instances of the traveling salesman problem, encoded as framed lists of binary distances and a binary budget.

theorem Cslib.Complexity.encTSP_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : TSPInstance) => (a.dist, a.bound)) encTSP encTSPFields 1 1

def Cslib.Complexity.TSP.dist (D : List (List ℕ)) (i j : ℕ) : ℕ

The distance from city i to city j in the matrix D: entry j of row i. Entries missing from a ragged or short matrix read 0.

def Cslib.Complexity.TSP.tourLength (D : List (List ℕ)) (p : List ℕ) : ℕ

The length of the closed tour visiting the cities of p in order: the sum of the distances from each city of p to the next one, the last city returning to the first. A tour of one city c has length dist D c c, and the empty tour has length 0.

def Cslib.Complexity.TSP : Set TSPInstance

The traveling salesman problem: the instances x : TSPInstance such that some closed tour visiting each city 0, …, x.dist.length - 1 exactly once has length at most x.bound Papadimitriou, Section 9.3.

theorem Cslib.Complexity.TSP.tourLength_eq_sum (D : List (List ℕ)) (p : List ℕ) : tourLength D p = (List.map (fun (k : ℕ) => dist D ((p ++ List.take 1 p).getD k 0) ((p ++ List.take 1 p).getD (k + 1) 0)) (List.range p.length)).sum

The tour length as a sum over the positions of the tour: with q = p ++ p.take 1, the tour with its first city repeated at the end, position k pays the distance from entry k of q to entry k + 1.

Membership in NP

theorem Cslib.Complexity.TSP.computableInPolyTime_tourLength : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : List (List ℕ) × List ℕ) => tourLength x.1 x.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) Turing.MultiTapeTM.encNat

The length of a tour is polynomial-time in the distance matrix and the tour, both with binary entries: it is a binary sum over the positions of the tour, and a city beyond the matrix is looked up at an index capped by the number of rows.

def Cslib.Complexity.TSP.verifier : TSPInstance × List Bool → Bool

The verifier for TSP: decode a list of cities from the certificate (Graph.decodeVertexList applied to the cities 0, …, n - 1) and check that it lists every city exactly once and that the closed tour visiting the cities in this order has length at most the budget.

theorem Cslib.Complexity.TSP.isVerifier : IsVerifier encTSP (Polynomial.X ^ 2) verifier TSP

TSP.verifier verifies TSP with certificates of length n ^ 2 for instances of encoded length n.

theorem Cslib.Complexity.TSP.computableInPolyTime_verifier : Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair encTSP Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The TSP verifier is polynomial-time.

theorem Cslib.Complexity.TSP.mem_NP : TSP ∈ NP encTSP

TSP belongs to NP.

The reduction from Hamiltonian cycles

def Cslib.Complexity.HamCycle.toTSP (G : Graph) : TSPInstance

The reduction from HamCycle to TSP Papadimitriou, Section 9.3: the cities are the distinct declared vertices, at distance 1 when they are adjacent and 2 otherwise, and the budget is the number n of cities. When n < 3 the graph has no Hamiltonian cycle, and the reduction returns the no-instance of one city at distance 1 from itself with budget 0.

theorem Cslib.Complexity.HamCycle.toTSP_mem_iff (G : Graph) : toTSP G ∈ TSP ↔ G ∈ HamCycle

Correctness of the reduction to TSP. A graph has a Hamiltonian cycle exactly when its distance matrix has a closed tour of length at most the number of cities.

theorem Cslib.Complexity.HamCycle.computableInPolyTime_toTSP : Turing.MultiTapeTM.ComputableInPolyTime toTSP encGraph encTSP

The reduction toTSP is polynomial-time: the cities are selected from the declared vertices, and the distances and the budget are written in binary.

theorem Cslib.Complexity.polyTimeReducible_HamCycle_TSP : PolyTimeReducible encGraph encTSP HamCycle TSP

HamCycle reduces to TSP in polynomial time via HamCycle.toTSP.

theorem Cslib.Complexity.TSP_npHard : NPHard encTSP TSP

TSP is NP-hard.

theorem Cslib.Complexity.TSP_npComplete : NPComplete encTSP TSP

TSP is NP-complete Papadimitriou, Section 9.3.