Document Open Access Logo

A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks

Author Andreas Lochbihler

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2021.25.pdf
  • Filesize: 0.85 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Network flows
  • Theory of computation → Higher order logic
  • Theory of computation → Logic and verification
Keywords
  • flow network
  • optimization
  • infinite graph
  • Isabelle/HOL

Metrics

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

Abstract

Aharoni et al. [Ron Aharoni et al., 2010] proved the max-flow min-cut theorem for countable networks, namely that in every countable network with finite edge capacities, there exists a flow and a cut such that the flow saturates all outgoing edges of the cut and is zero on all incoming edges. In this paper, we formalize their proof in Isabelle/HOL and thereby identify and fix several problems with their proof. We also provide a simpler proof for networks where the total outgoing capacity of all vertices other than the source is finite. This proof is based on the max-flow min-cut theorem for finite networks.

Cite As Get BibTex

Andreas Lochbihler. A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ITP.2021.25

Author Details

Andreas Lochbihler
  • Digital Asset (Switzerland) GmbH, Zürich, Switzerland

Funding

Swiss National Science Foundation grant 153217 "Formalising Computational Soundness for Protocol Implementations". This work was partially done while the author was at ETH Zurich.

Acknowledgements

We thank Ron Aharoni and Eli Berger for helping to clarify the weaknesses in the original proofs. S. Reza Sefidgar and the anonymous reviewers helped to improve the presentation.

Supplementary Materials

References

  1. Ron Aharoni. Menger’s theorem for graphs containing no infinite paths. European Journal of Combinatorics, 4:201-204, 1983. URL: https://doi.org/10.1016/S0195-6698(83)80012-2.
  2. Ron Aharoni and Eli Berger. Menger’s theorem for infinite graphs. Inventiones mathematicae, 176(1):1-62, 2009. URL: https://doi.org/10.1007/s00222-008-0157-3.
  3. Ron Aharoni, Eli Berger, Agelos Georgakopoulos, Amitai Perlstein, and Philipp Sprüssel. The max-flow min-cut theorem for countable networks. Journal of Combinatorial Theory, Series B, 101:1-17, 2010. URL: https://doi.org/10.1016/j.jctb.2010.08.002.
  4. Clemens Ballarin. Locales and locale expressions in Isabelle/Isar. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, Types for Proofs and Programs (TYPES 2003), volume 3085 of LNCS, pages 34-50. Springer Berlin Heidelberg, 2004. URL: https://doi.org/10.1007/978-3-540-24849-1_3.
  5. Clemens Ballarin. Locales: A module system for mathematical theories. Journal of Automated Reasoning, 52:123-153, 2014. URL: https://doi.org/10.1007/s10817-013-9284-7.
  6. Clemens Ballarin. Exploring the structure of an algebra text with locales. Journal of Automated Reasoning, 64:1093-1121, 2020. URL: https://doi.org/10.1007/s10817-019-09537-9.
  7. Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, and Pierre-Yves Strub. *-liftings for differential privacy. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, International Colloquium on Automata, Languages, and Programming (ICALP 2017), volume 80 of Leibniz International Proceedings in Informatics (LIPIcs), pages 102:1-102:12, Dagstuhl, Germany, 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.102.
  8. N. Bourbaki. Sur le théorème de Zorn. Archiv der Mathematik, 2(6):434-437, 1949. Google Scholar
  9. Jack Edmonds and Richard M. Karp. Theoretical improvements in algorithmic efficiency for network flow problems. Journal of the ACM, 19(2):248-264, 1972. URL: https://doi.org/10.1145/321694.321699.
  10. L. R. Ford and D. R. Fulkerson. Maximal flow through a network. Canadian Journal of Mathematics, 8:399-404, 1956. URL: https://doi.org/10.4153/CJM-1956-045-5.
  11. Fabian Immler. Generic construction of probability spaces for paths of stochastic processes in Isabelle/HOL. Master’s thesis, Fakultät für Informatik, Technische Universität München, 2012. Google Scholar
  12. Hans G. Kellerer. Funktionen auf Produkträumen mit vorgegebenen Marginal-Funktionen. Mathematische Annalen, 144:323-344, 1961. URL: https://doi.org/10.1007/BF01470505.
  13. Peter Lammich and S. Reza Sefidgar. Formalizing the Edmonds-Karp algorithm. In Jasmin Christian Blanchette and Stephan Merz, editors, Interactive Theorem Proving (ITP 2016), volume 9807 of LNCS, pages 219-234. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-43144-4_14.
  14. Peter Lammich and S. Reza Sefidgar. Formalizing network flow algorithms: A refinement approach in Isabelle/HOL. Journal of Automated Reasoning, 62:261-280, 2019. URL: https://doi.org/10.1007/s10817-017-9442-4.
  15. Gilbert Lee. Correctnesss of Ford-Fulkerson’s maximum flow algorithm. Formalized Mathematics, 13(2):305-314, 2005. URL: https://fm.mizar.org/2005-13/pdf13-2/glib_005.pdf.
  16. Andreas Lochbihler. A formal proof of the max-flow min-cut theorem for countable networks. Archive of Formal Proofs, 2016. http://www.isa-afp.org/entries/MFMC_Countable.shtml, Formal proof development.
  17. Andreas Lochbihler. Probabilistic functions and cryptographic oracles in higher-order logic. In Peter Thiemann, editor, Programming Languages and Systems (ESOP 2016), volume 9632 of LNCS, pages 503-531. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49498-1_20.
  18. Andreas Lochbihler. A mechanized proof of the max-flow min-cut theorem for countable networks. http://www.andreas-lochbihler.de/pub/lochbihler2021itpl.pdf, 2021.
  19. Russell Lyons and Yuval Peres. Probability on Trees and Networks. Cambridge University Press, New York, 2017. URL: https://doi.org/10.1017/9781316672815.
  20. Wolfgang Naraschewski and Markus Wenzel. Object-oriented verification based on record subtyping in higher-order logic. In Jim Grundy and Malcolm Newey, editors, Theorem Proving in Higher Order Logics (TPHOLs 1998), volume 1479 of LNCS, pages 349-366. Springer, 1998. URL: https://doi.org/10.1007/BFb0055146.
  21. Christophe Sabot and Laurent Tournier. Random walks in Dirichlet environment: an overview. Annales de la Faculté des sciences de Toulouse: Mathématiques, Ser. 6, 26(2):463-509, 2017. URL: https://doi.org/10.5802/afst.1542.
  22. Joshua Sack and Lijun Zhang. A general framework for probabilistic characterizing formulae. In Viktor Kuncak and Andrey Rybalchenko, editors, Verification, Model Checking, and Abstract Interpretation (VMCAI 2012), volume 7148 of LNCS, pages 396-411. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-27940-9_26.
  23. Gert Smolka, Steven Schäfer, and Christian Doczkal. Transfinite constructions in classical type theory. In Christian Urban and Xingyuan Zhang, editors, Interactive Theorem Proving (ITP 2015), volume 9236 of LNCS, pages 391-404. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-22102-1_26.
  24. Freek Wiedijk. The de Bruijn factor. https://www.cs.ru.nl/~freek/factor/factor.pdf, 2000.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact