Exact Shortest Paths and Maximum Flow in Planar Networks in the CONGEST Model
Sebastian Senge
cs.DC
Nov 1, 2026 · v1
TL;DR
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.
Abstract
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.
Problem
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.
Approach
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.
Results
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.
| Problem | Rounds | Previous |
|---|
| Exact SSSP, directed, w≥0 | Õ(D) | Õ(D^2) |
| Exact SSSP, negative weights | D·n^{o(1)} | Õ(D^2) |
| Exact max st-flow, directed | min{Õ(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