← All papers
First page of Exact Shortest Paths and Maximum Flow in Planar Networks in the CONGEST Model

Exact Shortest Paths and Maximum Flow in Planar Networks in the CONGEST Model

Sebastian Senge

cs.DC Nov 1, 2026 · v1
Three key lemmas (virtual-source lemma, dual distance lemma for the face-disjoint graph, discretized boosting step) are machine-checked in Lean 4 with Mathlib, sorry-free.
In the CONGEST model, exact single-source shortest paths (SSSP) with nonnegative weights and exact maximum $st$-flow in directed planar networks have both been solved in $\tilde O(D^2)$ rounds, where $D$ is the hop diameter, while the lower bound is $Ω(D)$. Given the approximate distance labels of a recent preprint (arXiv:2606.31192), which we use as a black box, we solve exact directed SSSP in $\tilde O(D)$ rounds. It rests on a lemma that answers queries from a virtual source with the labels, and on a corrected discretization of the reduction of exact to approximate distances (arXiv:2210.16351). All further bounds of the form $\tilde O(D)$ and $D\cdot n^{o(1)}$ use these labels. Through the reduction of arXiv:2303.00811, SSSP with negative weights, or the detection of a negative cycle, takes $D\cdot n^{o(1)}$ rounds with high probability. We weight the face-disjoint graph of arXiv:2411.11718 so that its distances are dual distances, which turns distance problems in the dual into problems in a planar network of hop diameter $O(D)$. This gives exact maximum $st$-flow in directed planar networks in $\min\{\tilde O(D^2),D\cdot n^{o(1)}\}$ rounds with high probability, and in $\tilde O(D)$ rounds with $s,t$ on a common face. In undirected planar networks, the value of a minimum $st$-cut and a minimum cut take $\tilde O(D)$ rounds. For this we repair the auxiliary graphs of arXiv:2608.09500 at $s$ and $t$, and we show that its recursion, as we read it, can miss the minimum cut, also with exact shortest paths: on a network with $11$ vertices it reports $37$ for a minimum cut of $15$. Two more shortest-path computations per level make it exact. The virtual-source lemma, the weighting of the face-disjoint graph and the corrected discretization are machine-checked in Lean 4 with Mathlib; all other arguments are proved on paper only. Numerical checks are not used in any proof.

Exact directed SSSP and exact maximum st-flow in planar networks in the CONGEST model were known in Õ(D^2) rounds, against an Ω(D) lower bound. The best undirected minimum-cut algorithm in Õ(D) rounds was only approximate.

Approximate distance labels from a recent preprint are used as a black box. They are combined with a virtual-source lemma and a corrected discretization of an exact-from-approximate reduction to get exact SSSP. The face-disjoint graph is weighted so that its distances equal dual distances, which reduces dual problems to planar networks of hop diameter O(D). A prior minimum-cut recursion is repaired with two extra shortest-path computations per level. The virtual-source lemma, the dual distance lemma and the discretized boosting step are formalized in Lean 4 with Mathlib. The proofs use only standard axioms; the CONGEST algorithms and round counts are not formalized.

Exact directed SSSP runs in Õ(D) rounds, and negative-weight SSSP in D·n^{o(1)} rounds. Exact max st-flow runs in min{Õ(D^2), D·n^{o(1)}} rounds, or Õ(D) when s and t share a face. Exact undirected minimum st-cut runs in Õ(D) rounds. A counterexample shows the earlier recursion reports 37 for a minimum cut of 15.

ProblemRoundsPrevious
Exact SSSP, directed, w≥0Õ(D)Õ(D^2)
Exact SSSP, negative weightsD·n^{o(1)}Õ(D^2)
Exact max st-flow, directedmin{Õ(D^2), D·n^{o(1)}}min{Õ(D^2), n^{1/2+o(1)}D}
Min st-cut value, undirectedÕ(D)Õ(D^2)
New round bounds versus previous