A Formal Analysis of Capacity Scaling Algorithms for Minimum-Cost Flows

TL;DR

This work delivers a comprehensive formalisation of minimum-cost flow algorithms in Isabelle/HOL, delivering executable implementations and rigorous proofs for SSP, capacity scaling, and Orlin's algorithm. It introduces a principled ADT/locale framework that supports stepwise refinement and code extraction, incorporating a Bellman-Ford-based path search and a reduction to infinite-capacity instances to handle general flow problems. A key contribution is the first complete combinatorial correctness proof for Orlin's algorithm, along with detailed running-time analyses and a cohesive methodology that harmonises mathematical rigor with executable artefacts. The results advance the reliability of scaling-based flow algorithms for both theory and practice, enabling verified, reusable graph algorithm components and clarifying the boundaries of applicability via the finite/infinite capacity reductions.

Abstract

We present formalisations of the correctness of executable algorithms to solve minimum-cost flow problems in Isabelle/HOL. Two of the algorithms are based on the technique of scaling, most notably Orlin's algorithm, which has the fastest known running time for solving the problem of minimum-cost flow. We also include a formalisation of the worst-case running time argument for Orlin's algorithm. Our verified implementation of this algorithm, which is derived by the technique of stepwise refinement, is fully executable and was integrated into a reusable formal library on graph algorithms. Because the problems for which Orlin's algorithm works are restricted, we also verified an executable reduction from the general minimum-cost flow problem. We believe we are the first to formally consider the problem of minimum-cost flows and, more generally, any scaling algorithms. Our work has also led to a number of mathematical insights and improvements to proofs as well as theorem statements, compared to all existing expositions.

Figures (11)

• Figure 1: Flows, (residual) capacities and (residual) costs are black, green and red, respectively. Forward edges are blue, backward edges purple.
• Figure 2: A Circulation and its Decomposition
• Figure 3: Eliminating FBPs: Members of an $FBP$ belong either to the same (left) or to two different cycles (right). When we drop the $FBP$ on the left, we obtain two new cycles. On the right, $FBP$ deletion results in a single new cycle. Disjointness is preserved.
• Figure 4: Merging Forest Components: remaining balances $b'$, forest edges, flow values and representatives are blue, red, black and purple, respectively. Assume the balances are non-negative. Initially there are three components: $\{x\}$, $\{y\}$, and $\{z\}$. Then we merge $\{y\}$ and $\{z\}$ into one component, where $z$ is the representative, inheriting the balance of both $y$ and $z$. Then we add $x$ to the component, and $z$ is the representative of the final component. To make sure that the new balances are consistent, we move flow along the red edges to/from the representative vertex. The reduction in flow in each edge is bounded.
• Figure 5: We replace an edge $e$ from $x$ to $y$ with finite capacity $u(e) < \infty$ with a new vertex $e$ with $b(e) = u(e)$ and two edges $e_1=(e,x)$ and $e_2=(e,y)$, each with infinite capacity. After first adding $e_2$, the flow along this new edge is exactly $u(e)$ although it should be equal to $f(e) \leq u(e)$. Adding the other edge $e_1$ makes this possible because we can then send $f(e)$ units of flow from $e$ to $y$ and $u(e) - f(e)$ units to $x$. The vertex $x$ has now an abundant flow of $u(e)$ ($f(e)$ units do not leave $x$ anymore and there is an additional ingoing flow of $u(e) - f(e)$). We need to adjust the balance $b(x)$ to again obtain a balance-complying flow.

Theorems & Definitions (54)

• Example 2.1
• Example 2.2
• Example 2.3
• Remark 2.4
• Lemma 2.5: Flow Value Lemma
• Corollary 2.6
• Lemma 2.7
• Lemma 2.8: Decomposition of Circulations ahujaFindingMinimumcostFlows1992
• proof : Proof Sketch
• Example 3.1