Asymmetric traveling salesperson problem

AbbreviationAsymmetric TSP instances#✓fully proved

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

abbrev AsymmetricTspInstance := ℕ × List (List ℕ) × ℕ

Used by 3

Used byThe asymmetric traveling salesperson decision problem · Feasible asymmetric TSP instances · Well-formed asymmetric TSP instances

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

Let \(w\) be a weight matrix, given as a list of rows of natural numbers, and let \(t = (t_0, \dots, t_{L-1})\) be a list of natural numbers. The length of the tour \(t\) under \(w\) is \(\sum_{j=0}^{L-1} w_{t_j, t_{(j+1) \bmod L}}\), the sum of the weights along the closed walk including the return edge from \(t_{L-1}\) to \(t_0\), where \(w_{a,b}\) denotes the entry in row \(a\) and column \(b\) of \(w\), taken to be \(0\) when that entry does not exist. In particular the empty tour 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 asymmetric TSP instances

DefinitionWell-formed asymmetric TSP instances#✓fully proved

An asymmetric TSP instance \((n, w, B)\), with \(n\) the number of cities, \(w\) the weight matrix and \(B\) the bound, is well formed when \(n > 0\), \(w\) has exactly \(n\) rows, every row of \(w\) has length \(n\), and the diagonal entry \(w_{a,a}\) in row \(a\) and column \(a\) is \(0\) for every \(a < n\).

def WellFormed (i : AsymmetricTspInstance) : Prop :=
  0 < i.1 ∧ i.2.1.length = i.1 ∧ (∀ row ∈ i.2.1, row.length = i.1) ∧
    ∀ a < i.1, (i.2.1.getD a []).getD a 0 = 0

Uses 1 · Used by 1

Statement usesAsymmetric TSP instances

Used byThe asymmetric traveling salesperson decision problem

DefinitionFeasible asymmetric TSP instances#✓fully proved

An asymmetric TSP instance \((n, w, B)\) is feasible when there is a list \(t\) of natural numbers with no repeated entries, of length \(n\) and containing every \(v < n\) (so \(t\) lists the cities \(0, \dots, n - 1\) in some order), whose tour length under \(w\) is at most \(B\).

def AsymmetricTspFeasible
    (i : AsymmetricTspInstance) : 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 usesAsymmetric TSP instances · Length of a tour in the asymmetric TSP

Used byThe asymmetric traveling salesperson decision problem

DefinitionThe asymmetric traveling salesperson decision problem#✓fully proved

The asymmetric TSP decision problem accepts a bitstring \(x\) when \(x\) decodes, under the canonical bitstring encoding of asymmetric TSP instances, to an instance \((n, w, B)\) that is well formed and feasible, and rejects \(x\) otherwise; in particular it rejects every bitstring that does not decode to an instance.

noncomputable def asymmetricTspDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := AsymmetricTspInstance) x with
  | some i => decide (WellFormed i ∧ AsymmetricTspFeasible 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 asymmetric TSP instances · Asymmetric TSP instances · Well-formed asymmetric TSP instances · Decision problems

Used byTRAVELING SALESPERSON (ASYMMETRIC) is NP-complete

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

The asymmetric 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 asymmetricTsp_npComplete :
    asymmetricTspDec ∈ MetaMathlibExt.ComplexityTheory.NP ∧
      ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
        L ∈ MetaMathlibExt.ComplexityTheory.NP →
          Cslib.CookLevin.PolyManyOneRed L asymmetricTspDec

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), TRAVELING SALESPERSON PROBLEM (asymmetric).

Uses 5

Statement usesPolynomial-time many-one reduction · The asymmetric traveling salesperson decision problem · Complexity classes · Decision problems · The complexity class NP

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.