DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2024.3

A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows

Authors: Mohammad Abdulaziz and Thomas Ammer

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract

We present a formalisation of the correctness of 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 running time for the problem of minimum-cost flow. Our work uncovered a number of complications in the proofs of the results we formalised, the resolution of which required significant effort. Our work is also the first to formally consider the problem of minimum-cost flows and, more generally, scaling algorithms.

Cite as

Mohammad Abdulaziz and Thomas Ammer. A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 3:1-3:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{abdulaziz_et_al:LIPIcs.ITP.2024.3,
  author =	{Abdulaziz, Mohammad and Ammer, Thomas},
  title =	{{A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{3:1--3:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.3},
  URN =		{urn:nbn:de:0030-drops-207316},
  doi =		{10.4230/LIPIcs.ITP.2024.3},
  annote =	{Keywords: Network Flows, Formal Verification, Combinatorial Optimisation}
}

Search Results

Documents authored by Ammer, Thomas

A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows

Abstract

Cite as

Thanks for your feedback!

Could not send message