Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | https://arxiv.org/abs/2602.03701 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866912873492512768 |
|---|---|
| author | Abdulaziz, Mohammad Ammer, Thomas |
| author_facet | Abdulaziz, Mohammad Ammer, Thomas |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_03701 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | A Formal Analysis of Capacity Scaling Algorithms for Minimum-Cost Flows Abdulaziz, Mohammad Ammer, Thomas Logic in Computer Science 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. |
| title | A Formal Analysis of Capacity Scaling Algorithms for Minimum-Cost Flows |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2602.03701 |