eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-06-21
25:1
25:18
10.4230/LIPIcs.ITP.2021.25
article
A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks
Lochbihler, Andreas
1
https://orcid.org/0000-0002-5851-494X
Digital Asset (Switzerland) GmbH, Zürich, Switzerland
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol193-itp2021/LIPIcs.ITP.2021.25/LIPIcs.ITP.2021.25.pdf
flow network
optimization
infinite graph
Isabelle/HOL