#include <UDAlgorithms/utility.h> #include <UDAlgorithms/graph.h> void bfs(sequence<number> d, sequence<vertex> p, graph G, vertex s) { // solve (unweighted undirected graph) SSSP problem. vertex u, v; edge e; number w; index n = size(G); l0: std::queue<vertex> Q; l1: for (index i = 1; i <= n; ++i) { l2: d[i] = infinity; p[i] = nil; } l3: d[s] = 0; p[s] = nil; Q.push_back(s); // insert l4: while ( not Q.empty() ) l5: v = Q.front(); Q.pop_front(); // extract_min l6: for_each_neighbor(u, v, G) { l7: len = d[v] + 1; // length of path s to u via v. l8: if (d[u] > len) { l9: d[u] = len; p[u] = v; Q.push_back(u); } } } void bfs(sequence<number> d, sequence<vertex> p, graph G, vertex s) { // Dijkstra's algorithm: solves (weighted directed graph) SSSP problem. vertex u, v; edge e; number w; index n = size(G); l0: min_priority_queue<vertex> Q; l1: for (vertex v = 1; v <= n; ++v) { l2: d[v] = infinity; p[v] = nil; Q.insert(v, d[v]); } l3: d[s] = 0; p[s] = nil; Q.decrease_key(s, d[s]); l4: while ( not Q.empty() ) l5: v = Q.extract_min(); l6: for_each_out_edge(e, v, G) { l7: u = e.tip; len = d[v] + e.weight; // length of path s to u via v. l8: if (d[u] > len) { l9: d[u] = len; p[u] = v; Q.decrease_key(u, d[u]); } } }Invariant for Dijkstra's algorithm:
White nodes:
A node is labeled white if no path to s has been found.
Black nodes:
A node is labeled black if and only if the following are true:
Gray nodes:
A gray node v has one or more black neighbors and d[v], p[v] describe a shortest path from v among all possible paths that are black from p[v] onwards.
Claim: The properties above hold after ever iteration of the while loop and also just before entry to the while loop.
Proof:
Corollary: Dijkstra's algorithm correctly identifies shortest paths from every node to s.
Proof: At the end the claim is true and all nodes are black. The result follows from property 2 of black nodes.
k If v is a black node, the following are trueit has been extracted from the A shortest path <