Dijkstra's Algorithm with a Binary Heap in O((m + 1) (⌊log₂ n⌋ + 1)) Time

This file instantiates the black-box outer Dijkstra algorithm (Cslib.Algorithms.WordRAM.Dijkstra.dijkstraCode_exec and Cslib.Algorithms.WordRAM.Dijkstra.dijkstra_of_pq_spec) with the standalone word-RAM binary min-heap package (Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.pkg) to obtain Cslib.Algorithms.WordRAM.Dijkstra.LogLinearSpec and Cslib.Algorithms.WordRAM.Dijkstra.LogLinearStatement with zero priority-queue code coupled to Dijkstra's algorithm.

Main definitions

• Cslib.Algorithms.WordRAM.Dijkstra.heapDijkstra: structured exact-basis Dijkstra program instantiated with PriorityQueue.BinaryHeap.pqCode.

Main results

• Cslib.Algorithms.WordRAM.Dijkstra.heapDijkstra_spec: structured execution bound 200 * (m + 1) * (⌊log₂ n⌋ + 1).
• Cslib.Algorithms.WordRAM.Dijkstra.logLinearSpec: compiled flat-program specification LogLinearSpec (heapDijkstra.program OuterReg.zero) 230.
• Cslib.Algorithms.WordRAM.Dijkstra.logLinearStatement: the log-linear main theorem.

References

• E. W. Dijkstra, A note on two problems in connexion with graphs
• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Dijkstra.heapDijkstra : WordRAM.Code WordRAM.Basis.exact (15 + PriorityQueue.BinaryHeap.rBin)

Structured exact-basis Dijkstra program instantiated with the standalone binary min-heap.

theorem Cslib.Algorithms.WordRAM.Dijkstra.heapDijkstra_spec {G : ListInstance} {w : ℕ} (hw : WordRAM.Fits w (8 * (G.n + G.m + 2) * (G.maxWeight + 2))) : ∃ (y : WordRAM.Data (15 + PriorityQueue.BinaryHeap.rBin)), WordRAM.ExecWithin w heapDijkstra (WordRAM.Data.init G.encode) y (200 * (G.m + 1) * (Nat.log 2 G.n + 1)) ∧ ∀ (v : Fin G.n), y.mem (G.outAddr v) = encodeDist (G.dist G.source v)

Correctness and running time of structured Dijkstra with a binary heap.

theorem Cslib.Algorithms.WordRAM.Dijkstra.logLinearSpec : LogLinearSpec (heapDijkstra.program OuterReg.zero) 230

Dijkstra's algorithm with a binary heap in O((m + 1) (⌊log₂ n⌋ + 1)) time. The compiled program meets Cslib.Algorithms.WordRAM.Dijkstra.LogLinearSpec with K = 230.

theorem Cslib.Algorithms.WordRAM.Dijkstra.logLinearStatement : LogLinearStatement

Log-linear main theorem. Some word-RAM program over the exact basis computes all shortest-path distances from the source of a weighted directed graph with n vertices and m edges, given by adjacency lists, within O((m + 1) (⌊log₂ n⌋ + 1)) instructions.