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

TL;DR

This paper formalizes and verifies the correctness and running time of scaling algorithms, including Orlin's, for solving minimum-cost flow problems within a proof assistant, enhancing reliability and understanding.

Contribution

It provides the first formal verification of minimum-cost flow algorithms, especially scaling techniques like Orlin's, with executable implementations and complexity proofs.

Findings

Verified correctness of scaling algorithms in Isabelle/HOL

Formalized the worst-case running time of Orlin's algorithm

Developed a reusable formal library on graph algorithms

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.