Proofs: Highway hierarchies

The two-level highway query returns shortest paths full

This proof shows: correctness, termination.

Claim. Let all weights be nonnegative, let $H \ge 1$, and let radii and highway edges be as in lines L1 and L2. For all $s, t$, the query returns $\operatorname{dist}(s, t)$, and when it is finite, a walk of that weight (a simple path when all weights are positive).

If $s = t$ the query returns 0 and $[s]$, which is correct. Assume $s \ne t$.

Step 1: neighborhoods are closed along shortest paths. If $v \in N^\to(s)$ and $x$ is a vertex on a shortest $s$-$v$ path, then $\operatorname{dist}(s, x) \le \operatorname{dist}(s, v) \le r^\to(s)$ (weights are nonnegative), so $x \in N^\to(s)$. Symmetrically, if $u \in N^\gets(t)$ and $x$ is on a shortest $u$-$t$ path, then $x \in N^\gets(t)$.

Step 2: each side is Dijkstra on a fixed graph. Let $F$ be the graph with all edges out of vertices of $N^\to(s)$ plus all highway edges. We claim the forward side runs Dijkstra's algorithm on $F$ from $s$. It is a Dijkstra search, so when it scans $u$, its label $d^\to[u]$ is at least $\operatorname{dist}(s, u)$ (every label is the weight of a real path). If $u \notin N^\to(s)$, then $d^\to[u] \ge \operatorname{dist}(s, u) > r^\to(s)$, so line L4 allows only highway edges at $u$, the edges of $F$. If $u \in N^\to(s)$, a shortest $s$-$u$ path lies in $N^\to(s)$ by Step 1, all of whose out-edges are allowed; by induction over the scan order, as in the correctness of Dijkstra, $d^\to[u] = \operatorname{dist}(s, u) \le r^\to(s)$ when $u$ is scanned, so all its edges are allowed, again the edges of $F$. (The induction: the vertices of $N^\to(s)$ are scanned in order of their distance, and each is relaxed from its predecessor on a shortest path, which is in $N^\to(s)$ and was scanned with its true distance.) So the forward side is Dijkstra on $F$. In the same way, the backward side is Dijkstra from $t$ on the reverse of $B$, the graph of all edges into vertices of $N^\gets(t)$ plus all highway edges.

Step 3: a shortest path splits. Suppose $\operatorname{dist}(s, t) < \infty$ and let $P = (p_0 = s, \ldots, p_k = t)$ be a shortest path. Let $j$ be the least index with $p_j \in N^\gets(t)$; it exists since $t \in N^\gets(t)$. By Step 1, $p_j, \ldots, p_k$ are all in $N^\gets(t)$, so the edges of $P$ after $p_j$ end in $N^\gets(t)$ and lie in $B$. Consider an edge $(p_i, p_{i+1})$ with $i < j$. If $p_i \in N^\to(s)$, the edge is in $F$. Otherwise $p_{i+1} \notin N^\to(s)$ by Step 1 (applied to the prefix of $P$ up to $p_{i+1}$, a shortest path), and $p_i \notin N^\gets(t)$ since $i < j$; as $(p_i, p_{i+1})$ is on the shortest $s$-$t$ path $P$, it is a highway edge by line L2, so it is in $F$. Hence the prefix of $P$ up to $p_j$ is in $F$, and the suffix from $p_j$ is in $B$, so $\operatorname{dist}_F(s, p_j) + \operatorname{dist}_B(p_j, t) \le w(P) = \operatorname{dist}(s, t)$.

Step 4: the query. Every value given to $\mu$ is a label of one side plus a label of the other at the same vertex, the weight of an $s$-$t$ walk in $G$, so $\mu \ge \operatorname{dist}(s, t)$ always. If $\operatorname{dist}(s, t) = \infty$ there is no such walk, no meeting vertex is recorded, and the query returns $\infty$. Otherwise let $z = p_j$ from Step 3. Suppose the query stops with $\mu > \operatorname{dist}(s, t)$. Then both least keys were at least $\mu > \operatorname{dist}_F(s, z)$ and $> \operatorname{dist}_B(z, t)$, so both Dijkstra searches had scanned $z$ with labels $\operatorname{dist}_F(s, z)$ and $\operatorname{dist}_B(z, t)$ (Step 2). At the later of the two scans, line L5 set $\mu \le \operatorname{dist}_F(s, z) + \operatorname{dist}_B(z, t) \le \operatorname{dist}(s, t)$, and $\mu$ never increases, a contradiction. So $\mu = \operatorname{dist}(s, t)$. Following the predecessors of the remembered vertex on both sides gives an $s$-$t$ walk of weight at most the value of $\mu$ when it was set (labels only fall), hence exactly $\operatorname{dist}(s, t)$. (The two chains are each simple, coming from Dijkstra trees; if they share a vertex other than the meeting vertex, the result is a walk of that weight, which with positive weights cannot happen.)

Termination. Each side scans each vertex at most once and pushes one heap entry per relaxation, so the loop ends. $\blacksquare$