Floyd–Warshall algorithm

DefinitionWeight of a vertex path in an extended-integer weight matrix#✓fully proved

Let \(w\) assign to each ordered pair of vertices in \(\{0, \dots, n-1\}\) a weight in \(\mathbb{Z} \cup \{\infty\}\). The weight of a list of vertices \(v_0, v_1, \dots, v_m\) with \(m \ge 1\) is \(w(v_0, v_1) + w(v_1, v_2) + \cdots + w(v_{m-1}, v_m)\), computed in \(\mathbb{Z} \cup \{\infty\}\) where adding \(\infty\) gives \(\infty\). The empty list and every single-vertex list have weight \(0\).

def pathWeight {n : Nat} (weight : Fin n → Fin n → WithTop Int) :
    List (Fin n) → WithTop Int
  | [] => 0
  | [_] => 0
  | source :: target :: rest =>
      weight source target + pathWeight weight (target :: rest)

Used by 13

Used byFASTER-APSP computes shortest-path weights · Shortest path weight with at most \(r\) edges · Characterization of the shortest path weight with at most \(r\) edges · One min-plus multiplication extends shortest paths by one edge · Min-plus matrix powers give shortest path weights with at most \(r\) edges · SLOW-APSP computes shortest-path weights · Floyd–Warshall reports \(\infty\) exactly for unreachable pairs · No path is shorter than the Floyd–Warshall distance · Finite Floyd–Warshall distances are attained · Floyd–Warshall computes shortest-path distances · A negative diagonal entry in Floyd–Warshall reveals a negative cycle · Negative cycles · Stage-\(k\) shortest-path weight

DefinitionFinite-weight vertex path in a weight matrix#✓fully proved

Let \(w\) assign to each ordered pair of vertices in \(\{0, \dots, n-1\}\) a weight in \(\mathbb{Z} \cup \{\infty\}\), and let \(s\) and \(t\) be vertices. A list of vertices \(p\) is a weighted path from \(s\) to \(t\) when \(p\) is nonempty, its first entry is \(s\), its last entry is \(t\), and \(w(u, v) \ne \infty\) for every pair of consecutive entries \(u, v\) of \(p\).

def IsWeightedPath {n : Nat} (weight : Fin n → Fin n → WithTop Int)
    (source target : Fin n) (path : List (Fin n)) : Prop :=
  path.IsChainFromTo (fun left right => weight left right ≠ ⊤) source target

Used by 13

Used byFASTER-APSP computes shortest-path weights · Shortest path weight with at most \(r\) edges · Characterization of the shortest path weight with at most \(r\) edges · One min-plus multiplication extends shortest paths by one edge · Min-plus matrix powers give shortest path weights with at most \(r\) edges · SLOW-APSP computes shortest-path weights · Floyd–Warshall reports \(\infty\) exactly for unreachable pairs · No path is shorter than the Floyd–Warshall distance · Finite Floyd–Warshall distances are attained · Floyd–Warshall computes shortest-path distances · A negative diagonal entry in Floyd–Warshall reveals a negative cycle · Negative cycles · Stage-\(k\) shortest-path weight

DefinitionIntermediate vertices below a bound#✓fully proved

For a natural number \(k\), a list of vertices in \(\{0, \dots, n - 1\}\) has all its intermediate vertices below \(k\) when every entry of the list other than its first and its last is less than \(k\).

def InternalVerticesBelow {n : Nat} (k : Nat) (path : List (Fin n)) : Prop :=
  ∀ vertex ∈ path.tail.dropLast, vertex.val < k

Used by 9

Used byFASTER-APSP computes shortest-path weights · SLOW-APSP computes shortest-path weights · Floyd–Warshall reports \(\infty\) exactly for unreachable pairs · No path is shorter than the Floyd–Warshall distance · Finite Floyd–Warshall distances are attained · Floyd–Warshall computes shortest-path distances · Stage-\(k\) shortest-path weight · Correctness of the transitive-closure algorithm · Invariant of the transitive-closure stages

DefinitionStage-\(k\) shortest-path weight#✓fully proved

Let \(w\) assign to each ordered pair of vertices in \(\{0, \dots, n-1\}\) a weight in \(\mathbb{Z} \cup \{\infty\}\), let \(k\) be a natural number, let \(s\) and \(t\) be vertices and let \(d \in \mathbb{Z} \cup \{\infty\}\). A weighted path from \(s\) to \(t\) is a nonempty list of vertices that starts at \(s\), ends at \(t\) and has \(w(u, v) \ne \infty\) for every pair of consecutive vertices \(u, v\); its weight is the sum of these values \(w(u, v)\), and its intermediate vertices are all its entries except the first and the last. Then \(d\) is the stage-\(k\) shortest-path weight from \(s\) to \(t\) when \(d\) is at most the weight of every weighted path from \(s\) to \(t\) whose intermediate vertices are all less than \(k\), and either \(d = \infty\) or some such path has weight exactly \(d\).

def IsStageShortestPathWeight {n : Nat} (weight : Fin n → Fin n → WithTop Int)
    (k : Nat) (source target : Fin n) (distance : WithTop Int) : Prop :=
  (∀ path, IsWeightedPath weight source target path → InternalVerticesBelow k path →
    distance ≤ pathWeight weight path) ∧
  (distance = ⊤ ∨ ∃ path, IsWeightedPath weight source target path ∧
    InternalVerticesBelow k path ∧ pathWeight weight path = distance)

Uses 3 · Used by 3

Statement usesIntermediate vertices below a bound · Finite-weight vertex path in a weight matrix · Weight of a vertex path in an extended-integer weight matrix

Used byFASTER-APSP computes shortest-path weights · SLOW-APSP computes shortest-path weights · Floyd–Warshall computes shortest-path distances

DefinitionNegative cycles#✓fully proved

For an \(n \times n\) matrix \(w\) of weights in \(\mathbb{Z} \cup \{+\infty\}\), a list of vertices \(v_0, \dots, v_m\) is a negative cycle when \(m \ge 1\), \(v_m = v_0\), every weight \(w_{v_i v_{i+1}}\) with \(i < m\) is finite, the vertices \(v_0, \dots, v_{m-1}\) are pairwise distinct, and the path weight \(\sum_{i < m} w_{v_i v_{i+1}}\) is negative.

def IsNegativeCycle {n : Nat} (weight : Fin n → Fin n → WithTop Int)
    (cycle : List (Fin n)) : Prop :=
  ∃ base, IsWeightedPath weight base base cycle ∧ 2 ≤ cycle.length ∧
    cycle.dropLast.Nodup ∧ pathWeight weight cycle < 0

Uses 2 · Used by 5

Statement usesFinite-weight vertex path in a weight matrix · Weight of a vertex path in an extended-integer weight matrix

Used bySLOW-APSP computes shortest-path weights · No path is shorter than the Floyd–Warshall distance · Floyd–Warshall computes shortest-path distances · A negative diagonal entry in Floyd–Warshall reveals a negative cycle · Matrices with a negative cycle

DefinitionMatrices with a negative cycle#✓fully proved

An \(n \times n\) matrix \(w\) of weights in \(\mathbb{Z} \cup \{+\infty\}\) has a negative cycle when some list of vertices is a negative cycle for \(w\).

def HasNegativeCycle {n : Nat} (weight : Fin n → Fin n → WithTop Int) : Prop :=
  ∃ cycle, IsNegativeCycle weight cycle

Uses 1 · Used by 5

Statement usesNegative cycles

Used bySLOW-APSP computes shortest-path weights · No path is shorter than the Floyd–Warshall distance · Floyd–Warshall computes shortest-path distances · A negative diagonal entry in Floyd–Warshall reveals a negative cycle · Weight matrices without negative cycles

DefinitionWeight matrices without negative cycles#✓fully proved

Let \(w\) assign to each ordered pair of vertices in \(\{0, \dots, n-1\}\) a weight in \(\mathbb{Z} \cup \{\infty\}\). Then \(w\) has no negative cycle when there is no list of vertices \(v_0, v_1, \dots, v_m\) with \(m \ge 1\) such that \(v_m = v_0\), the vertices \(v_0, \dots, v_{m-1}\) are pairwise distinct, \(w(v_{i-1}, v_i) \ne \infty\) for \(1 \le i \le m\), and \(w(v_0, v_1) + \cdots + w(v_{m-1}, v_m) < 0\).

def NoNegativeCycle {n : Nat} (weight : Fin n → Fin n → WithTop Int) : Prop :=
  ¬HasNegativeCycle weight

Uses 1 · Used by 5

Statement usesMatrices with a negative cycle

Used byFASTER-APSP computes shortest-path weights · SLOW-APSP computes shortest-path weights · No path is shorter than the Floyd–Warshall distance · Floyd–Warshall computes shortest-path distances · Without negative cycles, Floyd–Warshall finds no negative diagonal entry

StructureFloyd–Warshall cost record#✓fully proved

A cost record for the Floyd–Warshall algorithm is a pair of natural numbers: the number of initialization events (input matrix cells copied into the initial distance table) and the number of min-plus transition events (table entries updated).

structure Cost where
  /-- Input matrix cells copied and diagonal-normalized. -/
  initializations : Nat
  /-- Executed min-plus table transitions. -/
  transitions : Nat
deriving DecidableEq, Repr

Used by 11

Used byFloyd–Warshall algorithm · Floyd–Warshall reports \(\infty\) exactly for unreachable pairs · No path is shorter than the Floyd–Warshall distance · Finite Floyd–Warshall distances are attained · Floyd–Warshall computes shortest-path distances · Without negative cycles, Floyd–Warshall finds no negative diagonal entry · A negative diagonal entry in Floyd–Warshall reveals a negative cycle · Initialization count of Floyd–Warshall · Floyd–Warshall performs \(n^2 + n^3\) steps · Transition count of Floyd–Warshall · Total Floyd–Warshall cost

DefinitionTotal Floyd–Warshall cost#✓fully proved

The total of a Floyd–Warshall cost record is its number of initialization events plus its number of min-plus transition events.

def Cost.total (cost : Cost) : Nat := cost.initializations + cost.transitions

Uses 1 · Used by 1

Statement usesFloyd–Warshall cost record

Used byFloyd–Warshall performs \(n^2 + n^3\) steps

DefinitionFloyd–Warshall algorithm#✓fully proved

Given an \(n \times n\) matrix \(w\) of weights in \(\mathbb{Z} \cup \{+\infty\}\) indexed by the vertices \(0, \dots, n - 1\), the Floyd–Warshall algorithm starts from the table with \(d^{(0)}_{ii} = \min(w_{ii}, 0)\) and \(d^{(0)}_{ij} = w_{ij}\) for \(i \ne j\), and for \(k = 0, \dots, n - 1\) computes the table \(d^{(k+1)}_{ij} = \min\bigl(d^{(k)}_{ij}, d^{(k)}_{ik} + d^{(k)}_{kj}\bigr)\). It returns the matrix \(d^{(n)}\) together with its cost: one initialization event for each entry of \(d^{(0)}\) and one transition event for each entry of each table \(d^{(k+1)}\).

Cslib.Algorithms.Lean.FloydWarshall.floydWarshall · 47 lines

@[no_expose]
def floydWarshall {n : Nat} (weight : Fin n → Fin n → WithTop Int) :
    TimeM Cost (Fin n → Fin n → WithTop Int) :=
  let Table := Vector (Vector (WithTop Int) n) n
  let tableGet (table : Table) (i j : Fin n) : WithTop Int := (table.get i).get j
  let rec initializeRow (rowIndex : Fin n) :
      (j : Nat) → j ≤ n → TimeM Cost (Vector (WithTop Int) j)
    | 0, _ => pure #v[]
    | j + 1, hj => do
        let row ← initializeRow rowIndex j (by omega)
        TimeM.tick ⟨1, 0⟩
        let column : Fin n := ⟨j, by omega⟩
        let value := min (weight rowIndex column) (if rowIndex = column then 0 else ⊤)
        pure (row.push value)
  let rec buildInitial :
      (i : Nat) → i ≤ n → TimeM Cost (Vector (Vector (WithTop Int) n) i)
    | 0, _ => pure #v[]
    | i + 1, hi => do
        let table ← buildInitial i (by omega)
        let row ← initializeRow ⟨i, by omega⟩ n (by omega)
        pure (table.push row)
  let rec buildStageRow (previous : Table) (pivot rowIndex : Fin n) :
      (j : Nat) → j ≤ n → TimeM Cost (Vector (WithTop Int) j)
    | 0, _ => pure #v[]
    | j + 1, hj => do
        let row ← buildStageRow previous pivot rowIndex j (by omega)
        TimeM.tick ⟨0, 1⟩
        let column : Fin n := ⟨j, by omega⟩
        let value := min (tableGet previous rowIndex column)
          (tableGet previous rowIndex pivot + tableGet previous pivot column)
        pure (row.push value)
  let rec buildStage (previous : Table) (pivot : Fin n) :
      (i : Nat) → i ≤ n → TimeM Cost (Vector (Vector (WithTop Int) n) i)
    | 0, _ => pure #v[]
    | i + 1, hi => do
        let table ← buildStage previous pivot i (by omega)
        let row ← buildStageRow previous pivot ⟨i, by omega⟩ n (by omega)
        pure (table.push row)
  let rec runStages (initial : Table) : (k : Nat) → k ≤ n → TimeM Cost Table
    | 0, _ => pure initial
    | k + 1, hk => do
        let previous ← runStages initial k (by omega)
        buildStage previous ⟨k, by omega⟩ n (by omega)
  do
    let initial ← buildInitial n (by omega)
    let final ← runStages initial n (by omega)
    pure fun i j => tableGet final i j

Uses 1 · Used by 9

Statement usesFloyd–Warshall cost record

Used byFloyd–Warshall reports \(\infty\) exactly for unreachable pairs · No path is shorter than the Floyd–Warshall distance · Finite Floyd–Warshall distances are attained · Floyd–Warshall computes shortest-path distances · Without negative cycles, Floyd–Warshall finds no negative diagonal entry · A negative diagonal entry in Floyd–Warshall reveals a negative cycle · Initialization count of Floyd–Warshall · Floyd–Warshall performs \(n^2 + n^3\) steps · Transition count of Floyd–Warshall

DefinitionNegative-diagonal test#✓fully proved

For an \(n \times n\) matrix \(d\) with entries in \(\mathbb{Z} \cup \{+\infty\}\), the negative-diagonal test on \(d\) is the Boolean value that is true exactly when \(d_{vv} < 0\) for some vertex \(v\).

def hasNegativeDiagonal {n : Nat} (distance : Fin n → Fin n → WithTop Int) : Bool :=
  (List.finRange n).any fun vertex => decide (distance vertex vertex < 0)

Used by 3

Used byWithout negative cycles, Floyd–Warshall finds no negative diagonal entry · A negative diagonal entry in Floyd–Warshall reveals a negative cycle · Characterization of the negative-diagonal test

TheoremInitialization count of Floyd–Warshall#✓fully proved

For every \(n\) and every \(n \times n\) matrix of weights in \(\mathbb{Z} \cup \{+\infty\}\), the Floyd–Warshall algorithm performs exactly \(n^2\) initialization events, one for each ordered pair of vertices.

theorem floydWarshall_initializations {n : Nat} (weight : Fin n → Fin n → WithTop Int) :
    (floydWarshall weight).time.initializations = n ^ 2

Uses 2 · Used by 1

Statement usesFloyd–Warshall cost record · Floyd–Warshall algorithm

Used byFloyd–Warshall performs \(n^2 + n^3\) steps

TheoremTransition count of Floyd–Warshall#✓fully proved

For every \(n\) and every \(n \times n\) matrix of weights in \(\mathbb{Z} \cup \{+\infty\}\), the Floyd–Warshall algorithm performs exactly \(n^3\) min-plus transition events, one for each triple \((k, i, j)\) of vertices.

theorem floydWarshall_transitions {n : Nat} (weight : Fin n → Fin n → WithTop Int) :
    (floydWarshall weight).time.transitions = n ^ 3

Uses 2 · Used by 1

Statement usesFloyd–Warshall cost record · Floyd–Warshall algorithm

Used byFloyd–Warshall performs \(n^2 + n^3\) steps

TheoremFloyd–Warshall performs \(n^2 + n^3\) steps#✓fully proved

For every \(n\) and every \(n \times n\) matrix of weights in \(\mathbb{Z} \cup \{+\infty\}\), the total number of events counted by the Floyd–Warshall algorithm, initialization events plus min-plus transition events, is exactly \(n^2 + n^3\).

theorem floydWarshall_time {n : Nat} (weight : Fin n → Fin n → WithTop Int) :
    (floydWarshall weight).time.total = n ^ 2 + n ^ 3

Uses 5

Statement usesFloyd–Warshall cost record · Total Floyd–Warshall cost · Floyd–Warshall algorithm

Proof usesInitialization count of Floyd–Warshall · Transition count of Floyd–Warshall

TheoremCharacterization of the negative-diagonal test#✓fully proved

For every \(n \times n\) matrix \(d\) with entries in \(\mathbb{Z} \cup \{+\infty\}\), the negative-diagonal test on \(d\) returns true if and only if \(d_{vv} < 0\) for some vertex \(v\).

theorem hasNegativeDiagonal_eq_true_iff {n : Nat}
    (distance : Fin n → Fin n → WithTop Int) :
    hasNegativeDiagonal distance = true ↔ ∃ vertex, distance vertex vertex < 0

Uses 1 · Used by 1

Statement usesNegative-diagonal test

Used byA negative diagonal entry in Floyd–Warshall reveals a negative cycle

TheoremFloyd–Warshall computes shortest-path distances#✓fully proved

Let \(w\) assign a weight in \(\mathbb{Z} \cup \{\infty\}\) to each ordered pair of vertices in \(\{0, \dots, n-1\}\), suppose that \(w\) has no negative cycle, and let \(D\) be the distance matrix computed by Floyd–Warshall from \(w\). Then for all vertices \(s\) and \(t\), \(D(s, t)\) is at most the weight of every weighted path from \(s\) to \(t\), and either \(D(s, t) = \infty\) or \(D(s, t)\) is the weight of some weighted path from \(s\) to \(t\). Here a weighted path is a nonempty vertex sequence in which every consecutive pair has finite weight, and its weight is the sum of these weights.

Formally this is the stage-\(n\) characterization, which considers only paths whose intermediate vertices are all below \(n\); every path qualifies.

theorem floydWarshall_distance_spec {n : Nat}
    (weight : Fin n → Fin n → WithTop Int) (source target : Fin n)
    (hNoCycle : NoNegativeCycle weight) :
    IsStageShortestPathWeight weight n source target
      ((floydWarshall weight).ret source target)

Uses 9

Statement usesFloyd–Warshall cost record · Stage-\(k\) shortest-path weight · Weight matrices without negative cycles · Floyd–Warshall algorithm

Proof usesMatrices with a negative cycle · Intermediate vertices below a bound · Negative cycles · Finite-weight vertex path in a weight matrix · Weight of a vertex path in an extended-integer weight matrix

TheoremFinite Floyd–Warshall distances are attained#✓fully proved

Let \(w\) assign a weight in \(\mathbb{Z} \cup \{\infty\}\) to each ordered pair of vertices in \(\{0, \dots, n-1\}\), and let \(D\) be the distance matrix computed by Floyd–Warshall from \(w\). If \(D(s, t) = d\) for vertices \(s\), \(t\) and an integer \(d\), then there is a weighted path from \(s\) to \(t\) (a nonempty vertex sequence from \(s\) to \(t\) in which every consecutive pair has finite weight) whose weight, the sum of the weights of its consecutive pairs, is \(d\).

theorem floydWarshall_distance_realized {n : Nat}
    (weight : Fin n → Fin n → WithTop Int) (source target : Fin n) (distance : Int)
    (hDistance : (floydWarshall weight).ret source target = (distance : WithTop Int)) :
    ∃ path, IsWeightedPath weight source target path ∧
      pathWeight weight path = (distance : WithTop Int)

Uses 5 · Used by 2

Statement usesFloyd–Warshall cost record · Finite-weight vertex path in a weight matrix · Floyd–Warshall algorithm · Weight of a vertex path in an extended-integer weight matrix

Proof usesIntermediate vertices below a bound

Used byFloyd–Warshall reports \(\infty\) exactly for unreachable pairs · A negative diagonal entry in Floyd–Warshall reveals a negative cycle

TheoremNo path is shorter than the Floyd–Warshall distance#✓fully proved

Let \(w\) assign a weight in \(\mathbb{Z} \cup \{\infty\}\) to each ordered pair of vertices in \(\{0, \dots, n-1\}\), suppose that \(w\) has no negative cycle, and let \(D\) be the distance matrix computed by Floyd–Warshall from \(w\). Then for all vertices \(s\) and \(t\) and every weighted path \(p\) from \(s\) to \(t\) (a nonempty vertex sequence from \(s\) to \(t\) in which every consecutive pair has finite weight), \(D(s, t)\) is at most the weight of \(p\), the sum of the weights of its consecutive pairs.

theorem floydWarshall_distance_minimal {n : Nat}
    (weight : Fin n → Fin n → WithTop Int) (source target : Fin n)
    (path : List (Fin n)) (hNoCycle : NoNegativeCycle weight)
    (hPath : IsWeightedPath weight source target path) :
    (floydWarshall weight).ret source target ≤ pathWeight weight path

Uses 8

Statement usesFloyd–Warshall cost record · Finite-weight vertex path in a weight matrix · Weight matrices without negative cycles · Floyd–Warshall algorithm · Weight of a vertex path in an extended-integer weight matrix

Proof usesMatrices with a negative cycle · Intermediate vertices below a bound · Negative cycles

TheoremFloyd–Warshall reports \(\infty\) exactly for unreachable pairs#✓fully proved

Let \(w\) assign a weight in \(\mathbb{Z} \cup \{\infty\}\) to each ordered pair of vertices in \(\{0, \dots, n-1\}\), and let \(D\) be the distance matrix computed by Floyd–Warshall from \(w\). For all vertices \(s\) and \(t\), \(D(s, t) = \infty\) if and only if there is no weighted path from \(s\) to \(t\), that is, no nonempty vertex sequence from \(s\) to \(t\) in which every consecutive pair has finite weight.

theorem floydWarshall_distance_eq_top_iff {n : Nat}
    (weight : Fin n → Fin n → WithTop Int) (source target : Fin n) :
    (floydWarshall weight).ret source target = ⊤ ↔
      ¬∃ path, IsWeightedPath weight source target path

Uses 6

Statement usesFloyd–Warshall cost record · Finite-weight vertex path in a weight matrix · Floyd–Warshall algorithm

Proof usesIntermediate vertices below a bound · Finite Floyd–Warshall distances are attained · Weight of a vertex path in an extended-integer weight matrix

TheoremA negative diagonal entry in Floyd–Warshall reveals a negative cycle#✓fully proved

Let \(w\) assign a weight in \(\mathbb{Z} \cup \{\infty\}\) to each ordered pair of vertices in \(\{0, \dots, n-1\}\), and let \(D\) be the distance matrix computed by Floyd–Warshall from \(w\). If \(D(v, v) < 0\) for some vertex \(v\), then \(w\) has a negative cycle: a vertex sequence \(v_0, v_1, \dots, v_m\) with \(m \ge 1\) and \(v_m = v_0\), whose vertices \(v_0, \dots, v_{m-1}\) are pairwise distinct, in which every consecutive pair has finite weight, and whose total weight is negative.

theorem floydWarshall_hasNegativeDiagonal_sound {n : Nat}
    (weight : Fin n → Fin n → WithTop Int)
    (hNegative : hasNegativeDiagonal (floydWarshall weight).ret = true) :
    HasNegativeCycle weight

Uses 9 · Used by 1

Statement usesFloyd–Warshall cost record · Matrices with a negative cycle · Floyd–Warshall algorithm · Negative-diagonal test

Proof usesNegative cycles · Finite-weight vertex path in a weight matrix · Finite Floyd–Warshall distances are attained · Characterization of the negative-diagonal test · Weight of a vertex path in an extended-integer weight matrix

Used byWithout negative cycles, Floyd–Warshall finds no negative diagonal entry

TheoremWithout negative cycles, Floyd–Warshall finds no negative diagonal entry#✓fully proved

Let \(w\) assign a weight in \(\mathbb{Z} \cup \{\infty\}\) to each ordered pair of vertices in \(\{0, \dots, n-1\}\), and let \(D\) be the distance matrix computed by Floyd–Warshall from \(w\). If \(w\) has no negative cycle, then the negative-diagonal check on \(D\) returns false, that is, \(D(v, v) \ge 0\) for every vertex \(v\).

theorem floydWarshall_hasNegativeDiagonal_eq_false {n : Nat}
    (weight : Fin n → Fin n → WithTop Int) (hNoCycle : NoNegativeCycle weight) :
    hasNegativeDiagonal (floydWarshall weight).ret = false

Uses 5

Statement usesFloyd–Warshall cost record · Weight matrices without negative cycles · Floyd–Warshall algorithm · Negative-diagonal test

Proof usesA negative diagonal entry in Floyd–Warshall reveals a negative cycle

21 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.