Editing Shortest Path Faster Algorithm

The '''Shortest Path Faster Algorithm''' (SPFA) is a [[Shortest_paths#Single-source_shortest_paths|single-source shortest paths]] algorithm whose origin is unknown<sup>[see references]</sup>. It is similar to [[Dijkstra's algorithm]] in that it performs relaxations on nodes popped from some sort of [[queue]], but, unlike Dijkstra's, it is usable on graphs containing edges of negative weight, like the [[Bellman-Ford algorithm]]. Its value lies in the fact that, in the average case, it is likely to outperform Bellman-Ford (although not Dijkstra's). In theory, this should lead to an improved version of [[Johnson's algorithm]] as well.

==The algorithm==
The algorithm works by repeatedly selecting a vertex and using it to relax, if possible, all of its neighbors. If a node was successfully relaxed, then it might in turn be necessary to use it to relax other vertices, and hence it is marked for consideration also. Once there are no vertices left to be considered, the algorithm terminates. Note that a vertex might be considered several times during the course of the algorithm. The usual implementation strategy is to use a [[queue]] to hold the vertices that might be considered next.

====Pseudocode====
<pre>
input G,v
for each u ∈ V(G)
     let dist[u] = ∞
let dist[v] = 0
let Q be an initially empty queue
push(Q,v)
while not empty(Q)
     let u = pop(Q)
     for each (u,w) ∈ E(G)
          if dist[w] > dist[u]+wt(u,w)
               dist[w] = dist[u]+wt(u,w)
               if w is not in Q
                    push(Q,w)
</pre>
'''Note''': We use an array of boolean flags to keep track of which vertices are currently in the queue.

====Proof of correctness====
We will prove that the algorithm terminates and that it computes the correct shortest path lengths.

:''Lemma'': Whenever the queue is checked for emptiness, any vertex currently capable of causing relaxation is in the queue.
:''Proof'': We want to show that if <math>\mathrm{dist}[w] > \mathrm{dist}[u] + \operatorname{wt}(u,w)</math> for any two vertices <math>u</math> and <math>w</math> at the time the condition is checked, <math>u</math> is in the queue. We do so by induction on the number of iterations of the loop that have already occurred. First we note that this certainly holds before the loop is entered: if <math>u \neq v</math>, then relaxation is not possible; relaxation is possible from <math>u = v</math>, and this is added to the queue immediately before the while loop is entered. Now, consider what happens inside the loop. A vertex <math>u</math> is popped, and is used to relax all its neighbors, if possible. Therefore, immediately after that iteration of the loop, <math>u</math> is not capable of causing any more relaxations (and does not have to be in the queue anymore). However, the relaxation by <math>u</math> might cause some other vertices to become capable of causing relaxation. If there exists some <math>x</math> such that <math>\mathrm{dist}[x] > \mathrm{dist}[w] + \operatorname{wt}(w,x)</math> before the current loop iteration, then <math>w</math> is already in the queue. If this condition becomes true ''during'' the current loop iteration, then either <math>\mathrm{dist}[x]</math> increased, which is impossible, or <math>\mathrm{dist}[w]</math> decreased, implying that <math>w</math> was relaxed. But after <math>w</math> is relaxed, it is added to the queue if it is not already present. <math>_{_\blacksquare}</math>

:''Corollary'': The algorithm terminates when and only when no further relaxations are possible.
:''Proof'': If no further relaxations are possible, the algorithm continues to remove vertices from the queue, but does not add any more into the queue, because vertices are added only upon successful relaxations. Therefore the queue becomes empty and the algorithm terminates. If any further relaxations are possible, the queue is not empty, and the algorithm continues to run. <math>_{_\blacksquare}</math>

The algorithm fails to terminate if and only if negative-weight cycles are reachable from the source. See [[Bellman–Ford algorithm#Proof of detection of negative-weight cycles|here]] for a proof that relaxations are always possible when negative-weight cycles exist. In a graph with no cycles of negative weight, when no more relaxations are possible, the correct shortest paths have been computed ([[Shortest path#Relaxation|proof]]). Therefore in graphs containing no cycles of negative weight, the algorithm always terminates and always computes the correct shortest path lengths.

==References==
Details of the algorithm were obtained from code written by Gelin Zhou (University of Waterloo) who himself attributes the algorithm to a slide presented in a computer science class at MIT. The contributors to this article are unable to find a reference to it in the informatics literature. The algorithm almost certainly either originated among or was popularized by Chinese informatics competitors.
@@ Line 23: / Line 23: @@
 ====Proof of correctness====
-We will prove that the algorithm never computes incorrect shortest path lengths.
+We will prove that the algorithm terminates and that it computes the correct shortest path lengths.
 :''Lemma'': Whenever the queue is checked for emptiness, any vertex currently capable of causing relaxation is in the queue.
@@ Line 31: / Line 31: @@
 :''Proof'': If no further relaxations are possible, the algorithm continues to remove vertices from the queue, but does not add any more into the queue, because vertices are added only upon successful relaxations. Therefore the queue becomes empty and the algorithm terminates. If any further relaxations are possible, the queue is not empty, and the algorithm continues to run. <math>_{_\blacksquare}</math>
-The algorithm fails to terminate if negative-weight cycles are reachable from the source. See [[Bellman–Ford algorithm#Proof of detection of negative-weight cycles|here]] for a proof that relaxations are always possible when negative-weight cycles exist. In a graph with no cycles of negative weight, when no more relaxations are possible, the correct shortest paths have been computed ([[Shortest path#Relaxation|proof]]). Therefore in graphs containing no cycles of negative weight, the algorithm will never terminate with incorrect shortest path lengths.
+The algorithm fails to terminate if and only if negative-weight cycles are reachable from the source. See [[Bellman–Ford algorithm#Proof of detection of negative-weight cycles|here]] for a proof that relaxations are always possible when negative-weight cycles exist. In a graph with no cycles of negative weight, when no more relaxations are possible, the correct shortest paths have been computed ([[Shortest path#Relaxation|proof]]). Therefore in graphs containing no cycles of negative weight, the algorithm always terminates and always computes the correct shortest path lengths.
 ==References==
-Although, [http://en.wikipedia.org/wiki/Shortest_Path_Faster_Algorithm Wikipedia] cites [http://wenku.baidu.com/view/3b8c5d778e9951e79a892705.html Duan Fanding] as the originator of the algorithm under this name, this algorithm is first discovered by Yen as his first improvement to Bellman-Ford.
+Details of the algorithm were obtained from code written by Gelin Zhou (University of Waterloo) who himself attributes the algorithm to a slide presented in a computer science class at MIT. The contributors to this article are unable to find a reference to it in the informatics literature. The algorithm almost certainly either originated among or was popularized by Chinese informatics competitors.
-The actual details used in this article were deduced from code (privately communicated to the authors) written by Gelin Zhou (University of Waterloo) who himself attributes the algorithm to a slide presented in a computer science class at MIT. The contributors to this article are unable to find a reference to it in the informatics literature. The algorithm was almost certainly popularized by Chinese informatics competitors.
-[[Category:Algorithms]]
-[[Category:Graph theory]]