Traveling salesperson problem

DefinitionHamiltonian-cycle to TSP converter#✓fully proved

The Hamiltonian-cycle to TSP converter takes a Boolean array \(x\) and, starting from the empty array, scans \(x\) from left to right and appends the negation of each cell, charging one time unit before and one time unit after each append (one read and one write per cell). It returns the resulting array of negated cells together with the total time charged.

def hamiltonianCycleToTsp (x : Array Bool) : TimeM Nat (Array Bool) :=
  x.foldlM (fun out bit => do
    TimeM.tick (1 : Nat)
    let out := out.push (!bit)
    TimeM.tick (1 : Nat)
    pure out) #[]
Used by 7
Used byCosts produced by the Hamiltonian-cycle to TSP converter · Hamiltonian cycles of the source graph give zero-cost tours · The Hamiltonian-cycle to TSP converter negates every cell · Correctness of the Hamiltonian-cycle to TSP reduction · Tours of cost zero give Hamiltonian cycles of the source graph · The Hamiltonian-cycle to TSP converter preserves length · Running time of the Hamiltonian-cycle to TSP converter

TheoremThe Hamiltonian-cycle to TSP converter preserves length#✓fully proved

For every Boolean array \(x\), the array output by the Hamiltonian-cycle to TSP converter on \(x\) has the same length as \(x\).

No assumption that \(x\) encodes a graph is needed.

theorem hamiltonianCycleToTsp_size (x : Array Bool) :
    (hamiltonianCycleToTsp x).ret.size = x.size
Uses 1
Statement usesHamiltonian-cycle to TSP converter

TheoremThe Hamiltonian-cycle to TSP converter negates every cell#✓fully proved

For every Boolean array \(x\) and every index \(k\), the array output by the Hamiltonian-cycle to TSP converter on \(x\) has a cell at index \(k\) exactly when \(x\) does, and that cell is the negation of the cell of \(x\) at index \(k\).

theorem hamiltonianCycleToTsp_getElem? (x : Array Bool) (k : Nat) :
    (hamiltonianCycleToTsp x).ret[k]? = x[k]?.map Bool.not
Uses 1 · Used by 1
Statement usesHamiltonian-cycle to TSP converter
Used byCosts produced by the Hamiltonian-cycle to TSP converter

TheoremRunning time of the Hamiltonian-cycle to TSP converter#✓fully proved

For every Boolean array \(x\), the time charged by the Hamiltonian-cycle to TSP converter on \(x\) is \(2m\), where \(m\) is the length of \(x\): one unit for reading and one unit for writing each cell.

theorem hamiltonianCycleToTsp_time (x : Array Bool) :
    (hamiltonianCycleToTsp x).time = 2 * x.size
Uses 1
Statement usesHamiltonian-cycle to TSP converter

TheoremCosts produced by the Hamiltonian-cycle to TSP converter#✓fully proved

Let \(G\) be a simple graph on the vertex set \(\{0, \dots, n-1\}\), let \(x\) be a Boolean array of length \(n^2\) such that for all \(i, j < n\) the cell of \(x\) at index \(in + j\) exists and is true exactly when \(i\) and \(j\) are adjacent in \(G\), and let \(y\) be the array output by the Hamiltonian-cycle to TSP converter on \(x\), with a Boolean cell read as \(1\) if true and \(0\) if false. Then for all \(i, j < n\) the cell of \(y\) at index \(in + j\) exists and equals \(0\) if \(i\) and \(j\) are adjacent in \(G\) and \(1\) otherwise; for every \(i < n\) the cell of \(y\) at index \(in + i\) exists and equals \(1\); and for all \(i, j < n\) the cells of \(y\) at indices \(in + j\) and \(jn + i\) are equal.

theorem hamiltonianCycleToTsp_costs (x : Array Bool) (n : Nat)
    (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    (_hsize : x.size = n * n)
    (henc : ∀ i j : Fin n, x[i.val * n + j.val]? = some (decide (G.Adj i j))) :
    (∀ i j : Fin n,
      ((hamiltonianCycleToTsp x).ret[i.val * n + j.val]?).map Bool.toNat =
        some (if G.Adj i j then 0 else 1)) ∧
    (∀ i : Fin n,
      ((hamiltonianCycleToTsp x).ret[i.val * n + i.val]?).map Bool.toNat = some 1) ∧
    (∀ i j : Fin n,
      (hamiltonianCycleToTsp x).ret[i.val * n + j.val]? =
        (hamiltonianCycleToTsp x).ret[j.val * n + i.val]?)
Uses 2 · Used by 2
Statement usesHamiltonian-cycle to TSP converter
Proof usesThe Hamiltonian-cycle to TSP converter negates every cell
Used byHamiltonian cycles of the source graph give zero-cost tours · Tours of cost zero give Hamiltonian cycles of the source graph

TheoremHamiltonian cycles of the source graph give zero-cost tours#✓fully proved

Let \(G\) be a simple graph on the vertex set \(\{0, \dots, n-1\}\), let \(x\) be a Boolean array of length \(n^2\) such that for all \(i, j < n\) the cell of \(x\) at index \(in + j\) exists and is true exactly when \(i\) and \(j\) are adjacent in \(G\), and let \(y\) be the array output by the Hamiltonian-cycle to TSP converter on \(x\), with a Boolean cell read as \(1\) if true and \(0\) if false. Let \(p\) be a Hamiltonian cycle in \(G\) based at a vertex \(a\), and let \(p'\) be \(p\) regarded as a closed walk in the complete graph on \(\{0, \dots, n-1\}\). Then \(p'\) is a Hamiltonian cycle, \(p'\) visits the same sequence of vertices as \(p\), and for every directed edge \((u, v)\) traversed by \(p'\) the cell of \(y\) at index \(un + v\) exists, and the sum of these cells over the directed edges of \(p'\) is \(0\).

theorem hamiltonianCycleToTsp_forward (x : Array Bool) (n : Nat)
    (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    (hsize : x.size = n * n)
    (henc : ∀ i j : Fin n, x[i.val * n + j.val]? = some (decide (G.Adj i j)))
    (a : Fin n) (p : G.Walk a a) (hp : p.IsHamiltonianCycle) :
    (p.mapLe (show G ≤ SimpleGraph.completeGraph (Fin n) from le_top)).IsHamiltonianCycle ∧
    (p.mapLe (show G ≤ SimpleGraph.completeGraph (Fin n) from le_top)).support = p.support ∧
    ∃ costs : List Nat,
      (p.mapLe (show G ≤ SimpleGraph.completeGraph (Fin n) from le_top)).darts.mapM
          (fun d => ((hamiltonianCycleToTsp x).ret[d.fst.val * n + d.snd.val]?).map
            Bool.toNat) = some costs ∧ costs.sum = 0
Uses 2 · Used by 1
Statement usesHamiltonian-cycle to TSP converter
Proof usesCosts produced by the Hamiltonian-cycle to TSP converter
Used byCorrectness of the Hamiltonian-cycle to TSP reduction

TheoremTours of cost zero give Hamiltonian cycles of the source graph#✓fully proved

Let \(G\) be a simple graph on the vertex set \(\{0, \dots, n-1\}\), let \(x\) be a Boolean array of length \(n^2\) such that for all \(i, j < n\) the cell of \(x\) at index \(in + j\) exists and is true exactly when \(i\) and \(j\) are adjacent in \(G\), and let \(y\) be the array output by the Hamiltonian-cycle to TSP converter on \(x\), with a Boolean cell read as \(1\) if true and \(0\) if false. Let \(p\) be a Hamiltonian cycle based at a vertex \(a\) in the complete graph on \(\{0, \dots, n-1\}\) such that for every directed edge \((u, v)\) traversed by \(p\) the cell of \(y\) at index \(un + v\) exists and the sum of these cells over the directed edges of \(p\) is at most \(0\). Then there is a Hamiltonian cycle \(q\) in \(G\) based at \(a\) that visits the same sequence of vertices as \(p\).

theorem hamiltonianCycleToTsp_reverse (x : Array Bool) (n : Nat)
    (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    (hsize : x.size = n * n)
    (henc : ∀ i j : Fin n, x[i.val * n + j.val]? = some (decide (G.Adj i j)))
    (a : Fin n) (p : (SimpleGraph.completeGraph (Fin n)).Walk a a)
    (hp : p.IsHamiltonianCycle)
    (hcost : ∃ costs : List Nat,
      p.darts.mapM
        (fun d => ((hamiltonianCycleToTsp x).ret[d.fst.val * n + d.snd.val]?).map
          Bool.toNat) = some costs ∧ costs.sum ≤ 0) :
    ∃ q : G.Walk a a, q.IsHamiltonianCycle ∧ q.support = p.support
Uses 2 · Used by 1
Statement usesHamiltonian-cycle to TSP converter
Proof usesCosts produced by the Hamiltonian-cycle to TSP converter
Used byCorrectness of the Hamiltonian-cycle to TSP reduction

TheoremCorrectness of the Hamiltonian-cycle to TSP reduction#✓fully proved

Let \(G\) be a simple graph on the vertex set \(V = \{0, \dots, n-1\}\), let \(x\) be a Boolean array of length \(n^2\) such that for all \(i, j < n\) the cell of \(x\) at index \(in + j\) exists and is true exactly when \(i\) and \(j\) are adjacent in \(G\), and let \(y\) be the array output by the Hamiltonian-cycle to TSP converter on \(x\), with a Boolean cell read as \(1\) if true and \(0\) if false. Then \(G\) has a Hamiltonian cycle if and only if the complete graph on \(V\) has a Hamiltonian cycle \(p\) such that for every directed edge \((u, v)\) traversed by \(p\) the cell of \(y\) at index \(un + v\) exists and the sum of these cells over the directed edges of \(p\) is at most \(0\).

theorem hamiltonianCycleToTsp_iff (x : Array Bool) (n : Nat)
    (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    (hsize : x.size = n * n)
    (henc : ∀ i j : Fin n, x[i.val * n + j.val]? = some (decide (G.Adj i j))) :
    ((∃ (a : Fin n) (p : G.Walk a a), p.IsHamiltonianCycle) ↔
      ∃ (a : Fin n) (p : (SimpleGraph.completeGraph (Fin n)).Walk a a),
        p.IsHamiltonianCycle ∧ ∃ costs : List Nat,
          p.darts.mapM
            (fun d => ((hamiltonianCycleToTsp x).ret[d.fst.val * n + d.snd.val]?).map
              Bool.toNat) = some costs ∧ costs.sum ≤ 0)
Uses 3
Statement usesHamiltonian-cycle to TSP converter
Proof usesHamiltonian cycles of the source graph give zero-cost tours · Tours of cost zero give Hamiltonian cycles of the source graph

AbbreviationSymmetric TSP instances#✓fully proved

An instance of the symmetric traveling salesperson problem is a triple \((n, w, B)\) of a natural number \(n\), the number of cities, a weight matrix \(w\) given as a finite list of rows, each a finite list of natural numbers, and a natural number \(B\), the bound.

The type itself does not require \(w\) to be an \(n \times n\) symmetric matrix with zero diagonal.

abbrev TspInstance := ℕ × List (List ℕ) × ℕ
Used by 3
Used bySymmetric TSP as a decision problem · Feasible symmetric TSP instances · Well-formed symmetric TSP instances

DefinitionLength of a tour in the symmetric TSP#✓fully proved

Let \(w\) be a matrix of natural numbers given as a list of rows, where an entry \(w_{a,b}\) outside the list (no row \(a\), or row \(a\) too short) is read as \(0\), and rows and columns are numbered from \(0\). The length of a list \((t_0, \dots, t_{k-1})\) of natural numbers with respect to \(w\) is \(\sum_{j\lt k} w_{t_j, t_{(j+1) \bmod k}}\), the total weight of the edges along the cycle \(t_0, t_1, \dots, t_{k-1}, t_0\), including the return edge; the empty list has length \(0\).

def TourLength (w : List (List ℕ)) (tour : List ℕ) : ℕ :=
  ((List.range tour.length).map (fun j =>
    (w.getD (tour.getD j 0) []).getD (tour.getD ((j + 1) % tour.length) 0) 0)).sum
Used by 1
Used byFeasible symmetric TSP instances

DefinitionWell-formed symmetric TSP instances#✓fully proved

A symmetric TSP instance \((n, w, B)\) is well formed when \(n > 0\), the weight matrix \(w\) has exactly \(n\) rows and each row has exactly \(n\) entries, \(w\) is symmetric, that is \(w_{a,b} = w_{b,a}\) for all \(a, b < n\), and \(w\) has zero diagonal, that is \(w_{a,a} = 0\) for all \(a < n\). Rows and columns are numbered from \(0\).

def WellFormed (i : TspInstance) : Prop :=
  0 < i.1 ∧ i.2.1.length = i.1 ∧ (∀ row ∈ i.2.1, row.length = i.1) ∧
    (∀ a < i.1, ∀ b < i.1, (i.2.1.getD a []).getD b 0 = (i.2.1.getD b []).getD a 0) ∧
    ∀ a < i.1, (i.2.1.getD a []).getD a 0 = 0
Uses 1 · Used by 1
Statement usesSymmetric TSP instances
Used bySymmetric TSP as a decision problem

DefinitionFeasible symmetric TSP instances#✓fully proved

A symmetric TSP instance \((n, w, B)\) is feasible when there is a list of \(n\) pairwise distinct natural numbers containing every \(v < n\), that is, an ordering of the cities \(0, 1, \dots, n-1\) visiting each exactly once, whose tour length with respect to \(w\) (the sum of the weights of consecutive edges, including the return edge) is at most \(B\).

def TspFeasible
    (i : TspInstance) : Prop :=
  ∃ tour : List ℕ, tour.Nodup ∧ tour.length = i.1 ∧ (∀ v < i.1, v ∈ tour) ∧
    TourLength i.2.1 tour ≤ i.2.2
Uses 2 · Used by 1
Statement usesLength of a tour in the symmetric TSP · Symmetric TSP instances
Used bySymmetric TSP as a decision problem

DefinitionSymmetric TSP as a decision problem#✓fully proved

The symmetric traveling salesperson problem is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of symmetric TSP instances, to an instance \((n, w, B)\) that is well formed and feasible. Bitstrings that fail to decode, and bitstrings that decode to instances that are not well formed, are rejected.

noncomputable def tspDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := TspInstance) x with
  | some i => decide (WellFormed i ∧ TspFeasible i)
  | none => false
Uses 12 · Used by 1
Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Feasible symmetric TSP instances · Symmetric TSP instances · Well-formed symmetric TSP instances · Decision problems
Used byTRAVELING SALESPERSON (SYMMETRIC) is NP-complete

TheoremTRAVELING SALESPERSON (SYMMETRIC) is NP-complete#●ready to prove

The symmetric traveling salesperson decision problem belongs to NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

public theorem_wanted tsp_npComplete :
    tspDec ∈ MetaMathlibExt.ComplexityTheory.NP ∧
      ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
        L ∈ MetaMathlibExt.ComplexityTheory.NP →
          Cslib.CookLevin.PolyManyOneRed L tspDec
Sources
  • M. R. Garey and D. S. Johnson, Computers and Intractability (1979), TRAVELING SALESPERSON PROBLEM.
Uses 5
Statement usesPolynomial-time many-one reduction · Symmetric TSP as a decision problem · Complexity classes · Decision problems · The complexity class NP
13 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.