Johnson's algorithm

DefinitionJohnson's algorithm#✓fully proved

Let \(E\) be a list of directed edges on the vertices \(\{0, \dots, n-1\}\) with integer weights. Johnson's algorithm adds a new vertex \(s\) with an edge of weight \(0\) to every original vertex and runs Bellman–Ford from \(s\). If Bellman–Ford reports a negative cycle, the algorithm returns no table. Otherwise let \(h(v)\) be the Bellman–Ford distance of \(v\) (taken to be \(0\) if \(v\) is unreached). Each edge from \(u\) to \(v\) of weight \(w\) gets the new weight \(\max(0, w + h(u) - h(v))\). For each original vertex \(u\) the algorithm runs Dijkstra from \(u\) on the original vertices, where the weight from \(x\) to \(y\) is the least new weight of an edge from \(x\) to \(y\). It returns the table whose entry at \((u, v)\) is \(\infty\) if Dijkstra does not reach \(v\), and \(d'(u, v) + h(v) - h(u)\) otherwise, where \(d'(u, v)\) is the Dijkstra distance.

The cost counts the selected construction, scan, relaxation and decoding actions, not full RAM or bit complexity.

public def johnson {n : Nat} (edges : List (Edge n)) :
    TimeM Nat (Option (Fin n → Fin n → WithTop Int)) := do
  let augmented ← augment edges
  let run := bellmanFord augmented (Fin.last n)
  let result ← ({ ret := run.ret, time := run.time.total } : TimeM Nat _)
  match result with
  | .negativeCycle _ => pure none
  | .distances distances => do
      let potential ← readPotentials distances
      let reweighted ← reweightEdges potential augmented
      let prepared ← prepare edges reweighted
      let rows ← buildVector n (runRow prepared potential)
      pure (some fun source target => (rows.get source).get target)

Uses 12 · Used by 4

Statement usesBellman-Ford cost counters · Total Bellman–Ford cost · Bellman-Ford distance table · Weighted directed edge · Reachable negative cycle witness · Bellman–Ford result · Bellman–Ford algorithm · Directed adjacency graph · Cost of dense Dijkstra · Total Dijkstra cost · Output of Dijkstra's algorithm · Dense Dijkstra's algorithm

Used byCorrectness of Johnson's algorithm · Johnson's algorithm fails exactly on reachable negative cycles · Cost bound for Johnson's algorithm · Exact cost of a successful run of Johnson's algorithm

TheoremJohnson's algorithm fails exactly on reachable negative cycles#✓fully proved

For every list \(E\) of directed edges on the vertices \(\{0, \dots, n-1\}\) with integer weights, Johnson's algorithm on \(E\) returns no table if and only if there is a vertex \(s\) from which a negative cycle of \(E\) is reachable.

public theorem johnson_eq_none_iff {n : Nat} (edges : List (Edge n)) :
    (johnson edges).ret = none ↔ ∃ source : Fin n, HasReachableNegativeCycle edges source

Uses 19

Statement usesWeighted directed edge · Existence of a reachable negative cycle · Johnson's algorithm

Proof usesBellman-Ford cost counters · Total Bellman–Ford cost · Bellman-Ford distance table · Weighted path in an edge list · Reachable negative cycle witness · Bellman–Ford result · Bellman–Ford algorithm · Bellman-Ford succeeds exactly when no negative cycle is reachable · Tail of a weighted path · Vertices of a path · Bellman–Ford path weight · Directed adjacency graph · Cost of dense Dijkstra · Total Dijkstra cost · Output of Dijkstra's algorithm · Dense Dijkstra's algorithm

TheoremCorrectness of Johnson's algorithm#✓fully proved

Let \(E\) be a list of directed edges on the vertices \(\{0, \dots, n-1\}\) with integer weights, and suppose Johnson's algorithm on \(E\) returns a table \(d\). Then for all vertices \(s\) and \(t\), \(d(s, t) = \infty\) if and only if \(t\) is not reachable from \(s\) along edges of \(E\). Moreover, if \(d(s, t)\) is an integer \(x\), then some weighted path in \(E\) from \(s\) to \(t\) has weight \(x\), and every weighted path in \(E\) from \(s\) to \(t\) has weight at least \(x\).

public theorem johnson_distance_spec {n : Nat} (edges : List (Edge n))
    (distance : Fin n → Fin n → WithTop Int) (run : (johnson edges).ret = some distance)
    (source target : Fin n) :
    (distance source target = ⊤ ↔ ¬(toDirectedAdjacency edges).Reachable source target) ∧
      ∀ value : Int, distance source target = (value : WithTop Int) →
        (∃ path, IsWeightedPath edges source target path ∧ pathWeight path = value) ∧
          ∀ path, IsWeightedPath edges source target path → value ≤ pathWeight path

Uses 32

Statement usesWeighted directed edge · Weighted path in an edge list · Bellman–Ford path weight · Weight-forgetting directed graph · Reachability in a directed graph · Johnson's algorithm

Proof usesBellman-Ford cost counters · Total Bellman–Ford cost · Bellman-Ford distance table · Reachable negative cycle witness · Bellman–Ford result · Bellman–Ford algorithm · Bellman-Ford leaves exactly the unreachable vertices at infinite distance · Bellman-Ford distances are lower bounds on walk weights · Bellman-Ford distances are realized by walks · Edges of the weight-forgetting graph · Appending an edge to a weighted path · Tail of a weighted path · Weight of a path with an edge appended · Reachability by weighted paths · Directed adjacency graph · Cost of dense Dijkstra · Total Dijkstra cost · Output of Dijkstra's algorithm · Edge of a directed adjacency graph · Walks of a given weight · Semantically equivalent graphs have the same reachability · Dense Dijkstra's algorithm · Dijkstra's distance is infinite exactly at unreachable vertices · Dijkstra's finite distances are lower bounds on walk weights · Dijkstra's finite distances are realized by walks · Endpoint-weight sum along a vertex list

TheoremExact cost of a successful run of Johnson's algorithm#✓fully proved

Let \(E\) be a list of \(m\) directed edges on the vertices \(\{0, \dots, n-1\}\) with integer weights. If Johnson's algorithm on \(E\) returns a table, then its counted cost is exactly \(n^3 + nm + (n+1)(m+n) + 2n^2 + 4m + 5n + 1\).

public theorem johnson_time_of_success {n : Nat} (edges : List (Edge n))
    (distance : Fin n → Fin n → WithTop Int) (run : (johnson edges).ret = some distance) :
    (johnson edges).time = n^3 + n*edges.length + (n+1)*(edges.length+n) +
      2*n^2 + 4*edges.length + 5*n + 1

Uses 17

Statement usesWeighted directed edge · Johnson's algorithm

Proof usesBellman-Ford cost counters · Total Bellman–Ford cost · Bellman-Ford distance table · Reachable negative cycle witness · Bellman–Ford result · Bellman–Ford algorithm · Bellman-Ford spends no witness steps when it returns distances · Bellman-Ford makes exactly \(n \cdot |E|\) relaxation checks · Directed adjacency graph · Cost of dense Dijkstra · Total Dijkstra cost · Output of Dijkstra's algorithm · Adjacency entry count · Dense Dijkstra's algorithm · Running time of dense Dijkstra

TheoremCost bound for Johnson's algorithm#✓fully proved

For every list \(E\) of \(m\) directed edges on the vertices \(\{0, \dots, n-1\}\) with integer weights, the counted cost of Johnson's algorithm on \(E\), including the case where it extracts a negative cycle, is at most \(n^3 + nm + (n+1)(m+n) + 2n^2 + 4m + 5n + 1 + 3(n+1)\).

public theorem johnson_time_le {n : Nat} (edges : List (Edge n)) :
    (johnson edges).time ≤ n^3 + n*edges.length + (n+1)*(edges.length+n) +
      2*n^2 + 4*edges.length + 5*n + 1 + 3*(n+1)

Uses 18

Statement usesWeighted directed edge · Johnson's algorithm

Proof usesBellman-Ford cost counters · Total Bellman–Ford cost · Bellman-Ford distance table · Reachable negative cycle witness · Bellman–Ford result · Bellman–Ford algorithm · Bellman-Ford spends no witness steps when it returns distances · Bellman-Ford spends at most \(3n\) witness steps · Bellman-Ford makes exactly \(n \cdot |E|\) relaxation checks · Directed adjacency graph · Cost of dense Dijkstra · Total Dijkstra cost · Output of Dijkstra's algorithm · Adjacency entry count · Dense Dijkstra's algorithm · Running time of dense Dijkstra

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.