Document Open Access Logo

A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows

Authors Mohammad Abdulaziz , Thomas Ammer

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.3.pdf
  • Filesize: 0.92 MB
  • 19 pages

Document Identifiers

Author Details

Mohammad Abdulaziz
  • Department of Informatics, King’s College London, UK
Thomas Ammer
  • Department of Informatics, King’s College London, UK

Funding

The authors received funding from the Hausdorff Research Institute for Mathematics as part of the Trimester Programme "Prospects for Formal Mathematics". The second author received funding from the German foundation Cusanuswerk and is currently supported by a studentship from the Department of Informatics at King's College London.

Acknowledgements

Parts of the work presented in this paper were done at the Technical University of Munich.

Cite AsGet BibTex

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)
https://doi.org/10.4230/LIPIcs.ITP.2024.3

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Network flows
  • Theory of computation → Invariants
  • Theory of computation → Program verification
Keywords
  • Network Flows
  • Formal Verification
  • Combinatorial Optimisation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Mohammad Abdulaziz and Christoph Madlener. A Formal Analysis of RANKING. In The 14th Conference on Interactive Theorem Proving (ITP), 2023. URL: https://doi.org/10.48550/arXiv.2302.13747.
  2. Mohammad Abdulaziz, Kurt Mehlhorn, and Tobias Nipkow. Trustworthy graph algorithms (invited paper). In The 44th International Symposium on Mathematical Foundations of Computer Science (MFCS), 2019. URL: https://doi.org/10.4230/LIPIcs.MFCS.2019.1.
  3. Mohammad Abdulaziz and Lawrence C. Paulson. An Isabelle/HOL Formalisation of Green’s Theorem. In The 7th International Conference on Interactive Theorem Proving (ITP), 2016. URL: https://doi.org/10.1007/978-3-319-43144-4_1.
  4. Ravindra K. Ahuja, Thomas L. Magnanti, and James B. Orlin. Network Flows: Theory, Algorithms, and Applications. Prentice Hall, 1993. URL: https://api.semanticscholar.org/CorpusID:12577796.
  5. Stefan Berghofer and Tobias Nipkow. Executing Higher Order Logic. In Types for Proofs and Programs, 2002. URL: https://doi.org/10.1007/3-540-45842-5_2.
  6. Ran Duan, Seth Pettie, and Hsin-Hao Su. Scaling Algorithms for Weighted Matching in General Graphs. In Proceedings of the Twenty-Eighth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2017, Barcelona, Spain, Hotel Porta Fira, January 16-19, 2017. URL: https://doi.org/10.1137/1.9781611974782.50.
  7. Jack Edmonds and Richard M. Karp. Theoretical improvements in algorithmic efficiency for network flow problems. J. ACM, 19(2):248-264, April 1972. URL: https://doi.org/10.1145/321694.321699.
  8. L. R. FORD and D. R. FULKERSON. Flows in Networks. Princeton University Press, 1962. URL: http://www.jstor.org/stable/j.ctt183q0b4.
  9. Harold N. Gabow. The Weighted Matching Approach to Maximum Cardinality Matching. Fundam. Informaticae, 2017. URL: https://doi.org/10.3233/FI-2017-1555.
  10. Harold N. Gabow and Robert Endre Tarjan. Faster Scaling Algorithms for Network Problems. SIAM J. Comput., 1989. URL: https://doi.org/10.1137/0218069.
  11. Harold N. Gabow and Robert Endre Tarjan. Faster Scaling Algorithms for General Graph-Matching Problems. J. ACM, 1991. URL: https://doi.org/10.1145/115234.115366.
  12. Yon T. Gallai and Vorgelegt van G. HnjOs. Maximum-minimum sätze über graphen. Acta Mathematica Academiae Scientiarum Hungarica, 9:395-434, 1958. URL: https://api.semanticscholar.org/CorpusID:123953062.
  13. Fabian Immler and Yong Kiam Tan. The Poincaré-Bendixson theorem in Isabelle/HOL. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, 2020. URL: https://doi.org/10.1145/3372885.3373833.
  14. Bernhard Korte and Jens Vygen. Minimum Cost Flows, pages 215-244. Springer Berlin Heidelberg, Berlin, Heidelberg, 2018. URL: https://doi.org/10.1007/978-3-662-56039-6_9.
  15. Alexander Krauss. Automating Recursive Definitions and Termination Proofs in Higher-Order Logic. PhD thesis, Technische Universität München, 2009. Google Scholar
  16. Peter Lammich. Refinement to Imperative HOL. Journal of Automated Reasoning, 2019. URL: https://doi.org/10.1007/s10817-017-9437-1.
  17. Peter Lammich and S. Reza Sefidgar. Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL. J. Autom. Reason., 2019. URL: https://doi.org/10.1007/s10817-017-9442-4.
  18. Peter Lammich and Thomas Tuerk. Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm. In Interactive Theorem Proving, 2012. URL: https://doi.org/10.1007/978-3-642-32347-8_12.
  19. Gilbert Lee. Correctnesss of ford-fulkerson’s maximum flow algorithm1. Formalized Mathematics, 2005. Google Scholar
  20. Filip Marić. Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation. In Automated Reasoning, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_16.
  21. Tobias Nipkow. Amortized Complexity Verified. In Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings, 2015. URL: https://doi.org/10.1007/978-3-319-22102-1_21.
  22. James Orlin. A faster strongly polynomial minimum cost flow algorithm. In Proceedings of the Twentieth Annual ACM Symposium on Theory of Computing, STOC '88, pages 377-387, New York, NY, USA, 1988. Association for Computing Machinery. URL: https://doi.org/10.1145/62212.62249.
  23. James B. Orlin and Ravindra K. Ahuja. New scaling algorithms for the assignment and minimum mean cycle problems. Math. Program., 1992. URL: https://doi.org/10.1007/BF01586040.
  24. Floris van Doorn, Patrick Massot, and Oliver Nash. Formalising the h-Principle and Sphere Eversion. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, January 2023. URL: https://doi.org/10.1145/3573105.3575688.
  25. Niklaus Wirth. Program Development by Stepwise Refinement. Commun. ACM, 1971. URL: https://doi.org/10.1145/362575.362577.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact