Longest path

AbbreviationLongest-path instances#✓fully proved

A longest-path instance is a tuple \((n, E, K, s, t)\) consisting of a natural number \(n\), the number of vertices; a list \(E\) of pairs of natural numbers, the edges; and natural numbers \(K\), the length bound, \(s\), the start vertex, and \(t\), the target vertex.

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

Used by 4

Used byGraph of a longest-path instance · The LONGEST PATH decision problem · Feasibility of a longest-path instance · Well-formed longest-path instances

DefinitionGraph of a longest-path instance#✓fully proved

For a longest-path instance with vertex count \(n\) and edge list \(E\), its graph is the graph of the edge list \(E\) on \(n\) vertices: the simple graph on \(\{0, \dots, n - 1\}\) in which distinct vertices \(i\) and \(j\) are adjacent when \((i, j)\) or \((j, i)\) belongs to \(E\).

def Graph (i : LongestPathInstance) : SimpleGraph (Fin i.1) :=
  Cslib.Complexity.Karp.edgeGraph i.1 i.2.1

Uses 2 · Used by 1

Statement usesGraph of an edge list · Longest-path instances

Used byFeasibility of a longest-path instance

DefinitionWell-formed longest-path instances#✓fully proved

A longest-path instance \((n, E, K, s, t)\) is well formed when \(s < n\), \(t < n\), the list \(E\) has no repeated entries, and every pair \((u, v)\) in \(E\) satisfies \(u < n\), \(v < n\) and \(u \ne v\), and its reverse \((v, u)\) does not belong to \(E\).

def WellFormed (i : LongestPathInstance) : Prop :=
  i.2.1.Nodup ∧ (∀ e ∈ i.2.1, e.1 < i.1 ∧ e.2 < i.1 ∧ e.1 ≠ e.2 ∧ (e.2, e.1) ∉ i.2.1) ∧
    i.2.2.2.1 < i.1 ∧ i.2.2.2.2 < i.1

Uses 1 · Used by 1

Statement usesLongest-path instances

Used byThe LONGEST PATH decision problem

DefinitionFeasibility of a longest-path instance#✓fully proved

A longest-path instance \((n, E, K, s, t)\) is feasible when the graph of \(E\) on \(n\) vertices has a simple path from \(s\) to \(t\) with at least \(K\) edges, that is, a list \(v_0, \dots, v_m\) of pairwise distinct vertices with \(m \ge K\), \(v_0 = s\) and \(v_m = t\), in which \(v_j\) and \(v_{j+1}\) are adjacent for every \(j < m\).

def LongestPathFeasible
    (i : LongestPathInstance) : Prop :=
  ∃ path : List (Fin i.1), path.Nodup ∧ i.2.2.1 + 1 ≤ path.length ∧
    (path.head?.map fun v => (v : ℕ)) = some i.2.2.2.1 ∧
    (path.getLast?.map fun v => (v : ℕ)) = some i.2.2.2.2 ∧
    ∀ j (h : j + 1 < path.length),
      (Graph i).Adj (path[j]'(by omega)) (path[j + 1]'h)

Uses 2 · Used by 1

Statement usesGraph of a longest-path instance · Longest-path instances

Used byThe LONGEST PATH decision problem

DefinitionThe LONGEST PATH decision problem#✓fully proved

LONGEST PATH is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a longest-path instance \((n, E, K, s, t)\) that is well formed and in which the graph of \(E\) on \(n\) vertices has a simple path from \(s\) to \(t\) with at least \(K\) edges. Bitstrings that do not decode to a longest-path instance are rejected.

noncomputable def longestPathDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := LongestPathInstance) x with
  | some i => decide (WellFormed i ∧ LongestPathFeasible 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 longest-path instance · Longest-path instances · Well-formed longest-path instances · Decision problems

Used byLONGEST PATH is NP-complete

TheoremLONGEST PATH is NP-complete#●ready to prove

The LONGEST PATH decision problem belongs to NP, and every decision problem in NP has a polynomial-time many-one reduction to LONGEST PATH.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), LONGEST PATH.

Uses 5

Statement usesPolynomial-time many-one reduction · The LONGEST PATH 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.