Capacitated vehicle routing

AbbreviationCapacitated vehicle routing instances#✓fully proved

A capacitated vehicle routing instance is a tuple \((n, d, D, m, C, K)\) consisting of a natural number \(n\) (the number of customers), a list \(d\) of natural numbers (the demands), a list \(D\) of lists of natural numbers (the distance matrix, whose rows and columns include the depot), and natural numbers \(m\) (the number of vehicles), \(C\) (the capacity) and \(K\) (the bound on the total length).

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

Used by 3

Used byCapacitated vehicle routing as a decision problem · Feasibility of a capacitated vehicle routing instance · Well-formed capacitated vehicle routing instances

DefinitionLength of a route#✓fully proved

Let \(D\) be a list of lists of natural numbers, read as a distance matrix whose entry \(D_{u,v}\) is the entry at position \(v\) of the row at position \(u\) (positions counted from \(0\)), or \(0\) if there is no such entry, and let \(o\) be a natural number, the depot. The length of the empty route is \(0\), and the length of a route given by a list \((r_1, \dots, r_k)\) of natural numbers with \(k \ge 1\) is \(D_{o,r_1} + \sum_{j=1}^{k-1} D_{r_j,r_{j+1}} + D_{r_k,o}\), where the sum is \(0\) when \(k = 1\).

def RouteLength (dist : List (List ℕ)) (depot : ℕ) (route : List ℕ) : ℕ :=
  match route with
  | [] => 0
  | first :: _ =>
    (dist.getD depot []).getD first 0 +
    ((List.zip route route.tail).map (fun p => (dist.getD p.1 []).getD p.2 0)).sum +
    (dist.getD (route.getLast?.getD depot) []).getD depot 0

Used by 1

Used byFeasibility of a capacitated vehicle routing instance

DefinitionWell-formed capacitated vehicle routing instances#✓fully proved

A capacitated vehicle routing instance \((n, d, D, m, C, K)\) is well formed when the demand list \(d\) has length \(n\), the distance matrix \(D\) has \(n + 1\) rows, and every row of \(D\) has length \(n + 1\).

def WellFormed (i : CVRPInstance) : Prop :=
  i.2.1.length = i.1 ∧ i.2.2.1.length = i.1 + 1 ∧
    ∀ row ∈ i.2.2.1, row.length = i.1 + 1

Uses 1 · Used by 1

Statement usesCapacitated vehicle routing instances

Used byCapacitated vehicle routing as a decision problem

DefinitionFeasibility of a capacitated vehicle routing instance#✓fully proved

Let \((n, d, D, m, C, K)\) be a capacitated vehicle routing instance, with customers \(0, \dots, n - 1\) and depot \(n\), and let the demand \(d_c\) of \(c\) be the entry of the list \(d\) at position \(c\) (counting from \(0\)), or \(0\) if \(d\) has no such entry. The instance is feasible when there is a list of at most \(m\) routes, each a list of natural numbers, such that every route has no repeated entries and only entries less than \(n\); every customer \(c < n\) lies on some route, and all routes of the list that contain \(c\) are equal; the demands of the entries of each route sum to at most \(C\); and the lengths of the routes, for the distance matrix \(D\) and depot \(n\), sum to at most \(K\).

def CVRPFeasible
    (i : CVRPInstance) : Prop :=
  ∃ routes : List (List ℕ), routes.length ≤ i.2.2.2.1 ∧
    (∀ route ∈ routes, route.Nodup ∧ ∀ c ∈ route, c < i.1) ∧
    (∀ c < i.1, ∃ route ∈ routes, c ∈ route ∧
      ∀ route' ∈ routes, c ∈ route' → route' = route) ∧
    (∀ route ∈ routes, (route.map (fun c => i.2.1.getD c 0)).sum ≤ i.2.2.2.2.1) ∧
    (routes.map (fun route => RouteLength i.2.2.1 i.1 route)).sum ≤ i.2.2.2.2.2

Uses 2 · Used by 1

Statement usesCapacitated vehicle routing instances · Length of a route

Used byCapacitated vehicle routing as a decision problem

DefinitionCapacitated vehicle routing as a decision problem#✓fully proved

The decision problem CAPACITATED VEHICLE ROUTING accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a capacitated vehicle routing instance that is well formed and feasible; it rejects every bitstring that does not decode.

noncomputable def cvrpDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := CVRPInstance) x with
  | some i => decide (WellFormed i ∧ CVRPFeasible 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 · Feasibility of a capacitated vehicle routing instance · Capacitated vehicle routing instances · Well-formed capacitated vehicle routing instances · Decision problems

Used byCAPACITATED VEHICLE ROUTING is NP-complete

TheoremCAPACITATED VEHICLE ROUTING is NP-complete#●ready to prove

The decision problem CAPACITATED VEHICLE ROUTING lies in NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

public theorem_wanted cvrp_npComplete :
    cvrpDec ∈ MetaMathlibExt.ComplexityTheory.NP ∧
      ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
        L ∈ MetaMathlibExt.ComplexityTheory.NP →
          Cslib.CookLevin.PolyManyOneRed L cvrpDec

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), VEHICLE ROUTING (capacitated); G. B. Dantzig and J. H. Ramser, "The truck dispatching problem" (1959).

Uses 5

Statement usesPolynomial-time many-one reduction · Capacitated vehicle routing as a 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.