Skip to content
  1. CLRS-Lean
  2. Chapter 25. All-Pairs Shortest Paths
Browse chapters
Imports
import CLRSLean.Chapter_25.Section_25_1_All_Pairs_Model import CLRSLean.Chapter_25.Section_25_2_Floyd_Warshall import CLRSLean.Chapter_25.Section_25_3_Johnsons_Algorithm

Chapter 25 - All-Pairs Shortest Paths

Chapter 25 generalises the single-source shortest-path machinery of Chapter 24 to the all-pairs setting: compute the shortest-path distance for every ordered pair of vertices. The chapter formalises three main families of algorithms:

  1. Repeated squaring of the min-plus matrix product (Section 25.1, this section).

  2. The Floyd-Warshall algorithm (Section 25.2).

  3. Johnson's sparse-graph algorithm (Section 25.3).

Sections

  • 25.1 All-pairs shortest paths model and repeated-squaring DP. Main declarations: CLRS.Chapter24.WeightedGraph.weightMatrix, CLRS.Chapter24.WeightedGraph.minPlusMul, CLRS.Chapter24.WeightedGraph.extendShortestPaths, CLRS.Chapter24.WeightedGraph.L, CLRS.Chapter24.WeightedGraph.fasterAPSP, CLRS.Chapter24.WeightedGraph.lemma_25_1, CLRS.Chapter24.WeightedGraph.L_sq_eq_minPlusMul (Lemma 25.2), CLRS.Chapter24.WeightedGraph.fasterAPSP_eq_L, CLRS.Chapter24.WeightedGraph.fasterAPSP_eq_shortestDist, CLRS.Chapter24.WeightedGraph.minPlusMulCost, CLRS.Chapter24.WeightedGraph.fasterAPSPCost, CLRS.Chapter24.WeightedGraph.fasterAPSPCost_le_n_cubed_log (O(V³ log V)), and CLRS.Chapter24.WeightedGraph.fasterAPSPCost_le_n_four.

  • 25.2 Floyd-Warshall (Section_25_2_Floyd_Warshall). Main declarations: CLRS.Chapter24.WeightedGraph.fwStep, CLRS.Chapter24.WeightedGraph.D, CLRS.Chapter24.WeightedGraph.floydWarshall, CLRS.Chapter24.WeightedGraph.floydWarshall_O_cubed.

  • 25.3 Johnson's algorithm (Section_25_3_Johnsons_Algorithm). Main declarations: CLRS.Chapter24.WeightedGraph.johnsonAugmentedGraph, CLRS.Chapter24.WeightedGraph.reweightedGraph, CLRS.Chapter24.WeightedGraph.reweightedWalkWeight_eq, CLRS.Chapter24.WeightedGraph.reweightedWeight_nonneg, CLRS.Chapter24.WeightedGraph.johnsonCost_eq (O(V² log V + V E log V)), and CLRS.Chapter24.WeightedGraph.johnsonCost_le.

Current Shape

Section 25.1 defines the edge-weight matrix W, the min-plus matrix product A ◁ B, and the inductive sequence L^(m) of shortest-path weights using at most m edges. It then defines FASTER-APSP as repeated squaring (via Function.iterate) and proves:

  • Lemma 25.1: L^(m+1)_ij = min_k (L^m_ik + w_kj).

  • Lemma 25.2 (squaring identity): L^(2m) = L^m ◁ L^m.

  • Under no negative-weight cycles, L^m = L^{|V|-1} for all m ≥ |V|-1.

  • fasterAPSP = L^{|V|-1} = δ, the all-pairs shortest-path matrix (fasterAPSP_eq_shortestDist).

Section 25.2 defines the Floyd-Warshall DP recurrence D and the floydWarshall algorithm, and proves its correctness (Lemma 25.7, Theorem 25.8, CLRS Theorem 25.3). The predecessor matrix Pi, path reconstruction fwReconstructPath (walk validity and weight equality), and valid-input distance results are proved. The legacy zero diagonal masks negative self-edges. The canonical fourth-edition chapter adds a cycle-safe initializer and a complete negative-diagonal equivalence.

Section 25.3 defines Johnson's augmented graph and reweighted graph, constructs the Bellman-Ford potential h(v) = δ(none, some v), proves the triangle inequality h(v) ≤ h(u) + w(u, v), proves reweighted edge-weight nonnegativity, packages the end-to-end Johnson correctness theorem johnsonDist_isShortestDist (CLRS Theorem 25.5), under global NoNegCycle. There is no negative-cycle failure branch. The johnsonCost_eq / johnsonCost_le binary-heap expressions are independent backend budgets.

Running-time layer

The legacy formulas count table-update or backend budgets; the recursive function-valued specifications alone do not establish cached evaluation. The canonical fourth-edition chapter imports stored matrix execution with actual Floyd/min-plus counters, separate initialization writes and diagonal scan. Johnson's stored scan-queue companion retains potentials, reweighted edges and source rows and supplies its own cubic scalar-operation bound. Its queue is not a binary heap. Exact-real arithmetic, graph/index access and selected queue operations are primitives; allocation and bit costs are excluded.