Dijkstra's algorithm

DefinitionEndpoint-weight sum along a vertex list#✓fully proved

Given a weight \(w(u, v) \in \mathbb{N}\) for each ordered pair of vertices, the weight of a list of vertices \(v_0, v_1, \dots, v_k\) is \(w(v_0, v_1) + w(v_1, v_2) + \dots + w(v_{k-1}, v_k)\). In particular the empty list and every one-vertex list have weight \(0\).

@[expose] public def pathWeight (weight : V → V → Nat) : List V → Nat
  | [] | [_] => 0
  | source :: target :: rest =>
      weight source target + pathWeight weight (target :: rest)

Used by 17

Used byDijkstra'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 · Relaxation count of dense Dijkstra · Dijkstra's path reconstruction fails exactly at infinite distance · Reconstructed Dijkstra paths are simple and have the output weight · Dijkstra's predecessor pointers satisfy the distance equation · Walks of a given weight · Reachability via weighted walks · Correctness of Johnson's algorithm · A* with a consistent heuristic is optimal · A*'s finite path weights are realized by paths · The final keys of A* · A*'s predecessor paths are simple and realize its path weights · A*'s predecessor edges are tight · A consistent heuristic that vanishes at the goal is admissible · Reduced weights telescope along paths

DefinitionWalks of a given weight#✓fully proved

Let \(G\) be a directed graph given by adjacency lists, let \(w(u, v) \in \mathbb{N}\) be a weight for each ordered pair of vertices, let \(s\) and \(t\) be vertices and let \(d\) be a natural number. Then \(s\) reaches \(t\) with weight \(d\) when there is a nonempty list of vertices \(v_0, v_1, \dots, v_k\) with \(v_0 = s\), \(v_k = t\) and each \(v_{i+1}\) in the adjacency list of \(v_i\), such that \(w(v_0, v_1) + \dots + w(v_{k-1}, v_k) = d\).

@[expose] public def HasPathWeight (graph : DirectedAdjacency V) (weight : V → V → Nat)
    (source target : V) (distance : Nat) : Prop :=
  ∃ path, path.IsChainFromTo graph.Edge source target ∧
    pathWeight weight path = distance

Uses 3 · Used by 15

Statement usesDirected adjacency graph · Edge of a directed adjacency graph · Endpoint-weight sum along a vertex list

Used byDijkstra'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 · Relaxation count of dense Dijkstra · Dijkstra's path reconstruction fails exactly at infinite distance · Reconstructed Dijkstra paths are simple and have the output weight · Dijkstra's predecessor pointers satisfy the distance equation · Reachability via weighted walks · Correctness of Johnson's algorithm · A* with a consistent heuristic is optimal · A*'s finite path weights are realized by paths · The final keys of A* · A*'s predecessor edges are tight · Admissible heuristic · A consistent heuristic that vanishes at the goal is admissible

TheoremReachability via weighted walks#✓fully proved

Let \(G\) be a directed graph given by adjacency lists and let \(w(u, v) \in \mathbb{N}\) be a weight for each ordered pair of vertices. For vertices \(s\) and \(t\), \(t\) is reachable from \(s\) in \(G\) if and only if there is a natural number \(d\) such that \(s\) reaches \(t\) with weight \(d\) with respect to \(w\).

public theorem reachable_iff_exists_hasPathWeight (graph : DirectedAdjacency V)
    (weight : V → V → Nat) (source target : V) :
    graph.Reachable source target ↔
      ∃ distance, HasPathWeight graph weight source target distance

Uses 7 · Used by 7

Statement usesDirected adjacency graph · Walks of a given weight · Reachability in a directed graph

Proof usesEdge of a directed adjacency graph · Walks of a given length · Endpoint-weight sum along a vertex list · Reachability by walks

Used byDijkstra'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 · Relaxation count of dense Dijkstra · Dijkstra's path reconstruction fails exactly at infinite distance · Reconstructed Dijkstra paths are simple and have the output weight · Dijkstra's predecessor pointers satisfy the distance equation

DefinitionAdjacency entry count#✓fully proved

For a directed graph \(G\) given by an out-neighbour list \(\mathrm{adj}(v)\) for each vertex \(v\), the adjacency entry count of \(G\) is the total length \(\sum_{v} |\mathrm{adj}(v)|\) of these lists over all vertices \(v\), so repeated entries and self-loops are counted with multiplicity.

@[expose] public def adjacencyEntryCount (graph : DirectedAdjacency V) : Nat :=
  (graph.vertices.map fun vertex => (graph.adjacency vertex).length).sum

Uses 1 · Used by 5

Statement usesDirected adjacency graph

Used byRelaxation count of dense Dijkstra · Running time of dense Dijkstra · Cost bound for Johnson's algorithm · Exact cost of a successful run of Johnson's algorithm · Cost of A*

StructureCost of dense Dijkstra#✓fully proved

A Dijkstra cost is a pair of natural numbers that counts two kinds of events separately: the number of vertex entries inspected during minimum selection, and the number of adjacency-list entries inspected during relaxation.

public structure DijkstraCost where
  /-- Vertex entries inspected by minimum selection. -/
  minScans : Nat
  /-- Adjacency entries inspected by relaxation. -/
  edgeRelaxations : Nat
  deriving DecidableEq

Used by 24

Used byDense 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 · Relaxation count of dense Dijkstra · Minimum-selection count of dense Dijkstra · Dijkstra's path reconstruction fails exactly at infinite distance · Reconstructed Dijkstra paths are simple and have the output weight · Dijkstra's predecessor pointers satisfy the distance equation · Running time of dense Dijkstra · Total Dijkstra cost · Johnson's algorithm · Correctness 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 · A* search · A* leaves exactly the unreachable vertices at infinity · A* with a consistent heuristic is optimal · A*'s finite path weights are realized by paths · The final keys of A* · A*'s predecessor paths are simple and realize its path weights · A*'s predecessor edges are tight · Cost of A*

DefinitionTotal Dijkstra cost#✓fully proved

The total of a Dijkstra cost record is its number of vertex entries inspected by minimum selection plus its number of adjacency entries inspected by relaxation.

@[expose] public def DijkstraCost.total (cost : DijkstraCost) : Nat :=
  cost.minScans + cost.edgeRelaxations

Uses 1 · Used by 7

Statement usesCost of dense Dijkstra

Used byRunning time of dense Dijkstra · Johnson's algorithm · Correctness 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 · Cost of A*

StructureOutput of Dijkstra's algorithm#✓fully proved

For vertices \(0, \dots, n-1\), a Dijkstra result consists of a source vertex \(s\), a distance entry \(d(v)\) for each vertex \(v\) that is either a natural number or \(\infty\), and a predecessor entry \(p(v)\) for each vertex \(v\) that is either a vertex or undefined. The entries are stored as arrays of length \(n\); \(d(v)\) is meant as the computed distance from \(s\) to \(v\) and \(p(v)\) as the vertex before \(v\) on a shortest path from \(s\).

public structure DijkstraResult (n : Nat) where
  /-- The starting vertex. -/
  source : Fin n
  /-- Final distance estimates, with `none` denoting infinity. -/
  distance : Vector (Option Nat) n
  /-- Shortest-path predecessor pointers. -/
  predecessor : Vector (Option (Fin n)) n

Used by 26

Used byDense 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 · Relaxation count of dense Dijkstra · Minimum-selection count of dense Dijkstra · Dijkstra's path reconstruction fails exactly at infinite distance · Reconstructed Dijkstra paths are simple and have the output weight · Dijkstra's predecessor pointers satisfy the distance equation · Running time of dense Dijkstra · Path recovery from Dijkstra predecessors · Johnson's algorithm · Correctness 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 · A* search · A* leaves exactly the unreachable vertices at infinity · A* with a consistent heuristic is optimal · A*'s finite path weights are realized by paths · The final keys of A* · A*'s predecessor paths are simple and realize its path weights · A*'s predecessor edges are tight · Cost of A* · Output of A-star search · Path recovered from an A-star result

DefinitionPath recovery from Dijkstra predecessors#✓fully proved

Let a Dijkstra result on \(n\) vertices have source \(s\) and predecessor entries \(p\). The path to a vertex \(t\) follows predecessors backwards: starting from \(u_0 = t\), as long as \(u_i \ne s\) it sets \(u_{i+1} = p(u_i)\). If \(u_k = s\) for some \(k \le n\), the result is the list \(u_k, u_{k-1}, \dots, u_0\) from \(s\) to \(t\). If some \(p(u_i)\) is undefined before \(s\) is reached, or \(s\) is not reached within \(n\) steps, there is no result.

public def DijkstraResult.pathTo? {n : Nat} (result : DijkstraResult n) (target : Fin n) :
    Option (List (Fin n)) :=
  let rec @[reducible] go (current : Fin n) : Nat → Option (List (Fin n))
    | 0 => if current = result.source then some [result.source] else none
    | fuel + 1 =>
        if current = result.source then
          some [result.source]
        else
          match result.predecessor.get current with
          | none => none
          | some previous => (go previous fuel).map fun path => path ++ [current]
  go target n

Uses 1 · Used by 4

Statement usesOutput of Dijkstra's algorithm

Used byDijkstra's path reconstruction fails exactly at infinite distance · Reconstructed Dijkstra paths are simple and have the output weight · A*'s predecessor paths are simple and realize its path weights · Path recovered from an A-star result

DefinitionDense Dijkstra's algorithm#✓fully proved

Let \(G\) be a directed graph on the vertices \(0, \dots, n-1\) given by a fixed enumeration of its vertices and adjacency lists, let \(w(u, v) \in \mathbb{N}\) be a weight for each ordered pair of vertices, and let \(s\) be a source vertex. The algorithm starts with \(d(s) = 0\), \(d(v) = \infty\) for \(v \ne s\), no predecessors and no settled vertices, and runs \(n\) rounds. In each round it scans all vertices in the order of the enumeration of \(G\) and selects the first unsettled vertex \(u\) in that order whose value \(d(u)\) is minimal among unsettled vertices; if every vertex is settled the round does nothing. Otherwise it marks \(u\) settled and, for each entry \(v\) of the adjacency list of \(u\) in order, if \(v\) is unsettled, \(d(u)\) is finite and \(d(u) + w(u, v) < d(v)\), it sets \(d(v) := d(u) + w(u, v)\) and makes \(u\) the predecessor of \(v\). The result is \(s\) together with the final distances and predecessors. The cost charges one minimum-selection step for each vertex inspected during selection and one relaxation step for each adjacency entry inspected during relaxation.

Cslib.Algorithms.Lean.DirectedAdjacency.dijkstra · 80 lines

public def dijkstra {n : Nat} (graph : DirectedAdjacency (Fin n))
    (weight : Fin n → Fin n → Nat) (source : Fin n) :
    TimeM DijkstraCost (DijkstraResult n) :=
  let State := Vector (Option Nat) n × Vector (Option (Fin n)) n ×
    Vector Bool n × Vector (Option Nat) n × List (Fin n)
  let update {α : Type} (values : Vector α n) (index : Fin n) (value : α) :
      Vector α n :=
    values.set index.val value index.isLt
  let distanceLess (left right : Option Nat) : Bool :=
    match left, right with
    | some leftDistance, some rightDistance => leftDistance < rightDistance
    | some _, none => true
    | none, _ => false
  let consider (state : State) (best : Option (Fin n))
      (candidate : Fin n) : Option (Fin n) :=
    if state.2.2.1.get candidate then
      best
    else
      match best with
      | none => some candidate
      | some current =>
          if distanceLess (state.1.get candidate) (state.1.get current) then
            some candidate
          else
            best
  let rec @[reducible] selectLoop (state : State) :
      List (Fin n) → Option (Fin n) → TimeM DijkstraCost (Option (Fin n))
    | [], best => pure best
    | candidate :: rest, best => do
        TimeM.tick { minScans := 1, edgeRelaxations := 0 }
        selectLoop state rest (consider state best candidate)
  let relaxOne (previous target : Fin n) (state : State) : State :=
    if state.2.2.1.get target then
      state
    else
      match state.1.get previous with
      | none => state
      | some previousDistance =>
          let candidate := previousDistance + weight previous target
          match state.1.get target with
          | none =>
              (update state.1 target (some candidate),
                update state.2.1 target (some previous), state.2.2.1,
                state.2.2.2.1, state.2.2.2.2)
          | some targetDistance =>
              if candidate < targetDistance then
                (update state.1 target (some candidate),
                  update state.2.1 target (some previous), state.2.2.1,
                  state.2.2.2.1, state.2.2.2.2)
              else
                state
  let rec @[reducible] relaxLoop (previous : Fin n) :
      List (Fin n) → State → TimeM DijkstraCost State
    | [], state => pure state
    | target :: rest, state => do
        TimeM.tick { minScans := 0, edgeRelaxations := 1 }
        relaxLoop previous rest (relaxOne previous target state)
  let rec @[reducible] runRounds : Nat → Nat → State → TimeM DijkstraCost State
    | 0, _, state => pure state
    | remaining + 1, nextRank, state => do
        let selected ← selectLoop state graph.vertices none
        match selected with
        | none => runRounds remaining nextRank state
        | some vertex =>
            let state : State :=
              (state.1, state.2.1, update state.2.2.1 vertex true,
                update state.2.2.2.1 vertex (some nextRank),
                state.2.2.2.2 ++ [vertex])
            let state ← relaxLoop vertex (graph.adjacency vertex) state
            runRounds remaining (nextRank + 1) state
  let initial : State :=
    (Vector.ofFn fun vertex => if vertex = source then some 0 else none,
      Vector.ofFn fun _ => none, Vector.ofFn fun _ => false,
      Vector.ofFn fun _ => none, [])
  let run := runRounds n 0 initial
  { ret :=
      { source := source
        distance := run.ret.1
        predecessor := run.ret.2.1 }
    time := run.time }

Uses 3 · Used by 22

Statement usesDirected adjacency graph · Cost of dense Dijkstra · Output of Dijkstra's algorithm

Used byDijkstra'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 · Relaxation count of dense Dijkstra · Minimum-selection count of dense Dijkstra · Dijkstra's path reconstruction fails exactly at infinite distance · Reconstructed Dijkstra paths are simple and have the output weight · Dijkstra's predecessor pointers satisfy the distance equation · Running time of dense Dijkstra · Johnson's algorithm · Correctness 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 · A* search · A* leaves exactly the unreachable vertices at infinity · A* with a consistent heuristic is optimal · A*'s finite path weights are realized by paths · The final keys of A* · A*'s predecessor paths are simple and realize its path weights · A*'s predecessor edges are tight · Cost of A*

TheoremDijkstra's finite distances are realized by walks#✓fully proved

Let \(G\) be a directed graph on the vertices \(0, \dots, n-1\), let \(w(u, v)\) be a natural-number weight for every ordered pair of vertices, and let \(s\) and \(t\) be vertices. If Dijkstra's algorithm on \(G\) with weights \(w\) from source \(s\) outputs a finite distance \(d\) for \(t\), then \(G\) has a walk \(s = v_0, v_1, \dots, v_k = t\), with an edge from each \(v_{i-1}\) to \(v_i\), of weight \(\sum_{i=1}^{k} w(v_{i-1}, v_i) = d\).

theorem dijkstra_distance_realized {n : Nat} (graph : DirectedAdjacency (Fin n))
    (weight : Fin n → Fin n → Nat) (source target : Fin n) (distance : Nat)
    (h : (dijkstra graph weight source).ret.distance.get target = some distance) :
    HasPathWeight graph weight source target distance

Uses 9 · Used by 4

Statement usesDirected adjacency graph · Cost of dense Dijkstra · Output of Dijkstra's algorithm · Walks of a given weight · Dense Dijkstra's algorithm

Proof usesEdge of a directed adjacency graph · Reachability in a directed graph · Endpoint-weight sum along a vertex list · Reachability via weighted walks

Used byCorrectness of Johnson's algorithm · A*'s finite path weights are realized by paths · The final keys of A* · A*'s predecessor edges are tight

TheoremDijkstra's finite distances are lower bounds on walk weights#✓fully proved

Let \(G\) be a directed graph on the vertices \(0, \dots, n-1\), let \(w(u, v)\) be a natural-number weight for every ordered pair of vertices, and let \(s\) and \(t\) be vertices. If Dijkstra's algorithm on \(G\) with weights \(w\) from source \(s\) outputs a finite distance \(d\) for \(t\), then \(d \le d'\) for every walk \(s = v_0, v_1, \dots, v_k = t\) in \(G\) (with an edge from each \(v_{i-1}\) to \(v_i\)) of weight \(d' = \sum_{i=1}^{k} w(v_{i-1}, v_i)\).

theorem dijkstra_distance_minimal {n : Nat} (graph : DirectedAdjacency (Fin n))
    (weight : Fin n → Fin n → Nat) (source target : Fin n)
    (distance otherDistance : Nat)
    (h : (dijkstra graph weight source).ret.distance.get target = some distance)
    (path : HasPathWeight graph weight source target otherDistance) :
    distance ≤ otherDistance

Uses 9 · Used by 2

Statement usesDirected adjacency graph · Cost of dense Dijkstra · Output of Dijkstra's algorithm · Walks of a given weight · Dense Dijkstra's algorithm

Proof usesEdge of a directed adjacency graph · Reachability in a directed graph · Endpoint-weight sum along a vertex list · Reachability via weighted walks

Used byCorrectness of Johnson's algorithm · A* with a consistent heuristic is optimal

TheoremDijkstra's distance is infinite exactly at unreachable vertices#✓fully proved

Let \(G\) be a directed graph on the vertices \(0, \dots, n-1\), let \(w(u, v)\) be a natural-number weight for every ordered pair of vertices, and let \(s\) and \(t\) be vertices. The distance to \(t\) output by Dijkstra's algorithm on \(G\) with weights \(w\) from source \(s\) is infinite if and only if \(t\) is not reachable from \(s\) in \(G\).

theorem dijkstra_distance_eq_none_iff {n : Nat} (graph : DirectedAdjacency (Fin n))
    (weight : Fin n → Fin n → Nat) (source target : Fin n) :
    (dijkstra graph weight source).ret.distance.get target = none ↔
      ¬graph.Reachable source target

Uses 9 · Used by 2

Statement usesDirected adjacency graph · Cost of dense Dijkstra · Output of Dijkstra's algorithm · Reachability in a directed graph · Dense Dijkstra's algorithm

Proof usesEdge of a directed adjacency graph · Walks of a given weight · Endpoint-weight sum along a vertex list · Reachability via weighted walks

Used byCorrectness of Johnson's algorithm · A* leaves exactly the unreachable vertices at infinity

TheoremDijkstra's predecessor pointers satisfy the distance equation#✓fully proved

Let \(G\) be a directed graph on the vertices \(0, \dots, n-1\), let \(w(u, v)\) be a natural-number weight for every ordered pair of vertices, and let \(s\), \(t\) and \(p\) be vertices. If Dijkstra's algorithm on \(G\) with weights \(w\) from source \(s\) outputs \(p\) as the predecessor of \(t\), then \(G\) has an edge from \(p\) to \(t\), the distances \(d(p)\) and \(d(t)\) output for \(p\) and \(t\) are both finite, and \(d(t) = d(p) + w(p, t)\).

theorem dijkstra_predecessor_spec {n : Nat} (graph : DirectedAdjacency (Fin n))
    (weight : Fin n → Fin n → Nat) (source target previous : Fin n)
    (h : (dijkstra graph weight source).ret.predecessor.get target = some previous) :
    graph.Edge previous target ∧
      ∃ previousDistance targetDistance,
        (dijkstra graph weight source).ret.distance.get previous = some previousDistance ∧
        (dijkstra graph weight source).ret.distance.get target = some targetDistance ∧
        targetDistance = previousDistance + weight previous target

Uses 9 · Used by 1

Statement usesDirected adjacency graph · Cost of dense Dijkstra · Output of Dijkstra's algorithm · Edge of a directed adjacency graph · Dense Dijkstra's algorithm

Proof usesWalks of a given weight · Reachability in a directed graph · Endpoint-weight sum along a vertex list · Reachability via weighted walks

Used byA*'s predecessor edges are tight

TheoremDijkstra's path reconstruction fails exactly at infinite distance#✓fully proved

Let \(G\) be a directed graph on the vertices \(0, \dots, n-1\), let \(w(u, v)\) be a natural-number weight for every ordered pair of vertices, and let \(s\) and \(t\) be vertices. Reconstructing a path from \(s\) to \(t\) by following, for at most \(n\) steps, the predecessor pointers output by Dijkstra's algorithm on \(G\) with weights \(w\) from source \(s\) fails if and only if the distance output for \(t\) is infinite.

theorem dijkstra_pathTo?_eq_none_iff {n : Nat} (graph : DirectedAdjacency (Fin n))
    (weight : Fin n → Fin n → Nat) (source target : Fin n) :
    (dijkstra graph weight source).ret.pathTo? target = none ↔
      (dijkstra graph weight source).ret.distance.get target = none

Uses 10 · Used by 1

Statement usesDirected adjacency graph · Cost of dense Dijkstra · Output of Dijkstra's algorithm · Path recovery from Dijkstra predecessors · Dense Dijkstra's algorithm

Proof usesEdge of a directed adjacency graph · Walks of a given weight · Reachability in a directed graph · Endpoint-weight sum along a vertex list · Reachability via weighted walks

Used byReconstructed Dijkstra paths are simple and have the output weight

TheoremReconstructed Dijkstra paths are simple and have the output weight#✓fully proved

Let \(G\) be a directed graph on the vertices \(0, \dots, n-1\), let \(w(u, v)\) be a natural-number weight for every ordered pair of vertices, and let \(s\) and \(t\) be vertices. Suppose that following the predecessor pointers output by Dijkstra's algorithm on \(G\) with weights \(w\) from source \(s\) reconstructs a list of vertices \(P\) for \(t\). Then \(P\) is nonempty, say \(P = v_0, \dots, v_k\), with \(v_0 = s\) and \(v_k = t\); there is an edge from each \(v_{i-1}\) to \(v_i\); the \(v_i\) are pairwise distinct; and the distance \(d\) output for \(t\) is finite with \(d = \sum_{i=1}^{k} w(v_{i-1}, v_i)\).

theorem dijkstra_pathTo?_spec {n : Nat} (graph : DirectedAdjacency (Fin n))
    (weight : Fin n → Fin n → Nat) (source target : Fin n) (path : List (Fin n))
    (h : (dijkstra graph weight source).ret.pathTo? target = some path) :
    ∃ distance,
      (dijkstra graph weight source).ret.distance.get target = some distance ∧
      path.head? = some source ∧ path.getLast? = some target ∧
      path.IsChain graph.Edge ∧ path.Nodup ∧ pathWeight weight path = distance

Uses 11 · Used by 1

Statement usesDirected adjacency graph · Cost of dense Dijkstra · Output of Dijkstra's algorithm · Path recovery from Dijkstra predecessors · Edge of a directed adjacency graph · Dense Dijkstra's algorithm · Endpoint-weight sum along a vertex list

Proof usesWalks of a given weight · Reachability in a directed graph · Dijkstra's path reconstruction fails exactly at infinite distance · Reachability via weighted walks

Used byA*'s predecessor paths are simple and realize its path weights

TheoremRelaxation count of dense Dijkstra#✓fully proved

Let \(G\) be a directed graph on the vertices \(0, \dots, n-1\), let \(w(u, v)\) be a natural-number weight for every ordered pair of vertices, and let \(s\) be a vertex. The number of adjacency-list entries that Dijkstra's algorithm on \(G\) with weights \(w\) from source \(s\) inspects during relaxation equals the adjacency entry count of \(G\), the total length of all out-neighbour lists.

theorem dijkstra_edgeRelaxations {n : Nat} (graph : DirectedAdjacency (Fin n))
    (weight : Fin n → Fin n → Nat) (source : Fin n) :
    (dijkstra graph weight source).time.edgeRelaxations = adjacencyEntryCount graph

Uses 10 · Used by 1

Statement usesDirected adjacency graph · Cost of dense Dijkstra · Output of Dijkstra's algorithm · Adjacency entry count · Dense Dijkstra's algorithm

Proof usesEdge of a directed adjacency graph · Walks of a given weight · Reachability in a directed graph · Endpoint-weight sum along a vertex list · Reachability via weighted walks

Used byRunning time of dense Dijkstra

TheoremMinimum-selection count of dense Dijkstra#✓fully proved

Let \(G\) be a directed graph on the vertices \(0, \dots, n-1\), let \(w(u, v)\) be a natural-number weight for every ordered pair of vertices, and let \(s\) be a vertex. Dijkstra's algorithm on \(G\) with weights \(w\) from source \(s\) inspects exactly \(n^2\) vertex entries during minimum selection.

theorem dijkstra_minScans {n : Nat} (graph : DirectedAdjacency (Fin n))
    (weight : Fin n → Fin n → Nat) (source : Fin n) :
    (dijkstra graph weight source).time.minScans = n * n

Uses 4 · Used by 1

Statement usesDirected adjacency graph · Cost of dense Dijkstra · Output of Dijkstra's algorithm · Dense Dijkstra's algorithm

Used byRunning time of dense Dijkstra

TheoremRunning time of dense Dijkstra#✓fully proved

Let \(G\) be a directed graph on the vertices \(0, \dots, n-1\) given by adjacency lists, let \(w(u, v) \in \mathbb{N}\) be a weight for each ordered pair of vertices, and let \(s\) be a vertex. For dense Dijkstra from \(s\), the number of vertex entries inspected by minimum selection plus the number of adjacency entries inspected by relaxation is exactly \(n^2 + m\), where \(m\) is the number of adjacency-list entries of \(G\), counting duplicates and self-loops.

theorem dijkstra_time {n : Nat} (graph : DirectedAdjacency (Fin n))
    (weight : Fin n → Fin n → Nat) (source : Fin n) :
    (dijkstra graph weight source).time.total = n * n + adjacencyEntryCount graph

Uses 8 · Used by 3

Statement usesDirected adjacency graph · Cost of dense Dijkstra · Total Dijkstra cost · Output of Dijkstra's algorithm · Adjacency entry count · Dense Dijkstra's algorithm

Proof usesRelaxation count of dense Dijkstra · Minimum-selection count of dense Dijkstra

Used byCost bound for Johnson's algorithm · Exact cost of a successful run of Johnson's algorithm · Cost of A*

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.