Flows of weighted multigraphs and undirected max-flow/min-cut

A weighted multigraph is a multigraph G : Graph α β with capacities c : E(G) → K on its actual edges. Its flows are the flows of its bidirected network: the bidirected arrow family Graph.BidirectedHom G, in which a nonloop edge gives one arrow in each direction and a loop gives a single loop arrow, with every arrow carrying the capacity of its edge (Graph.bidirectedCapacity). There is no separate type of undirected flows: an s–t flow of G is a TauCeti.Flow (G.bidirectedCapacity c) s t, so the whole directed flow theory applies.

The bridge to undirected cuts is Graph.arrowSum_bidirectedCapacity: the arrows leaving a set S of actual vertices correspond one-to-one to the edges crossing S, each such edge giving exactly the arrow from its end in S to its end outside S. So the directed capacity of the cut is the multigraph cut capacity Graph.edgeCutCapacity c S, in which parallel edges contribute separately and loops not at all.

Acyclic flows are the natural normal form for undirected flows. A nonnegative acyclic assignment vanishes on every loop arrow (TauCeti.Assignment.IsAcyclic.apply_eq_zero_of_loop) and on one of the two opposite arrows of every nonloop edge (TauCeti.Assignment.IsAcyclic.apply_eq_zero_or_apply_eq_zero), so it never sends flow along an edge in both directions. By TauCeti.Flow.exists_isAcyclic, every flow can be replaced by an acyclic flow of the same value that is arrowwise no larger.

Main definitions

• Graph.bidirectedCapacity: the capacities of the bidirected network of a weighted multigraph.

Main results

• Graph.arrowSum_bidirectedCapacity: the directed capacity of the arrows leaving a set of actual vertices is its multigraph cut capacity.
• TauCeti.Flow.val_le_edgeCutCapacity: weak duality, the value of an s–t flow of a weighted multigraph is at most the capacity of every cut separating s from t.
• Graph.exists_flow_val_eq_edgeCutCapacity_mem: the undirected max-flow/min-cut theorem with integrality. For nonnegative capacities in an additive subgroup H and distinct actual vertices s and t, some acyclic s–t flow with values in H has value equal to the capacity of some cut separating s from t. Graph.exists_flow_val_eq_edgeCutCapacity is the case without H.
• TauCeti.Flow.IsMaximum.isMinimum_edgeCutCapacity_iff_val_eq: for a maximum flow, the minimum cuts are the separating sets whose capacity is its value.
• TauCeti.Flow.IsMaximum.val_eq_pairMinimumValue_edgeCutCapacity: the value of a maximum flow is the minimum cut value TauCeti.TerminalCut.pairMinimumValue (G.edgeCutCapacity c) s t of the undirected cut function.

References

• L. R. Ford, D. R. Fulkerson, Maximal flow through a network, Canad. J. Math. 8 (1956).
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Chapter 10.

def Graph.bidirectedCapacity {α : Type u} {β : Type v} {K : Type w} {G : Graph α β} (c : ↑G.edgeSet → K) : TauCeti.Assignment G.BidirectedHom K

The capacities of the bidirected network of a weighted multigraph: every arrow of the bidirected arrow family carries the capacity of its edge, so both arrows of a nonloop edge carry that capacity.

@[simp]

theorem Graph.bidirectedCapacity_apply {α : Type u} {β : Type v} {K : Type w} {G : Graph α β} (c : ↑G.edgeSet → K) {x y : ↑G.vertexSet} (a : G.BidirectedHom x y) : bidirectedCapacity c a = c ⟨↑a, ⋯⟩

Every arrow of the bidirected network carries the capacity of its edge.

theorem Graph.bidirectedCapacity_nonneg {α : Type u} {β : Type v} {K : Type w} {G : Graph α β} [Zero K] [LE K] {c : ↑G.edgeSet → K} (hc : 0 ≤ c) : 0 ≤ bidirectedCapacity c

Nonnegative edge capacities give nonnegative arrow capacities.

@[simp]

theorem Graph.arrowSum_bidirectedCapacity {α : Type u} {β : Type v} {K : Type w} {G : Graph α β} [Fintype ↑G.vertexSet] [DecidableEq ↑G.vertexSet] [Fintype ↑G.edgeSet] [(x y : ↑G.vertexSet) → Fintype (G.BidirectedHom x y)] [AddCommMonoid K] (c : ↑G.edgeSet → K) (S : Finset ↑G.vertexSet) : TauCeti.arrowSum (bidirectedCapacity c) S Sᶜ = G.edgeCutCapacity c S

The directed capacity of the arrows leaving a set S of actual vertices in the bidirected network is the multigraph cut capacity of S. Each edge crossing S gives exactly one arrow leaving S, from its end in S to its end outside S, and no other arrow leaves S.

theorem TauCeti.Flow.val_le_edgeCutCapacity {α : Type u} {β : Type v} {K : Type w} {G : Graph α β} [Fintype ↑G.vertexSet] [Fintype ↑G.edgeSet] [(x y : ↑G.vertexSet) → Fintype (G.BidirectedHom x y)] [AddCommGroup K] {c : ↑G.edgeSet → K} {s t : ↑G.vertexSet} [Preorder K] [AddLeftMono K] (f : Flow (Graph.bidirectedCapacity c) s t) {S : Finset ↑G.vertexSet} (hs : s ∈ S) (ht : t ∉ S) : f.val ≤ G.edgeCutCapacity c S

Weak duality for weighted multigraphs. The value of an s–t flow of a weighted multigraph is at most the capacity of every set of actual vertices containing s but not t.

theorem TauCeti.Flow.IsMaximum.isMinimum_edgeCutCapacity_iff_val_eq {α : Type u} {β : Type v} {K : Type w} {G : Graph α β} [Fintype ↑G.vertexSet] [Fintype ↑G.edgeSet] [(x y : ↑G.vertexSet) → Fintype (G.BidirectedHom x y)] [AddCommGroup K] {c : ↑G.edgeSet → K} {s t : ↑G.vertexSet} [LinearOrder K] [IsOrderedAddMonoid K] {f : Flow (Graph.bidirectedCapacity c) s t} (hf : f.IsMaximum) {S : Finset ↑G.vertexSet} : TerminalCut.IsMinimum (G.edgeCutCapacity c) {s} {t} S ↔ s ∈ S ∧ t ∉ S ∧ f.val = G.edgeCutCapacity c S

For a maximum s–t flow f of a weighted multigraph, the minimum cuts of the multigraph cut function are the sets of actual vertices containing s but not t whose capacity is the value of f.

theorem TauCeti.Flow.IsMaximum.val_eq_pairMinimumValue_edgeCutCapacity {α : Type u} {β : Type v} {K : Type w} {G : Graph α β} [Fintype ↑G.vertexSet] [Fintype ↑G.edgeSet] [(x y : ↑G.vertexSet) → Fintype (G.BidirectedHom x y)] [AddCommGroup K] {c : ↑G.edgeSet → K} {s t : ↑G.vertexSet} [LinearOrder K] [IsOrderedAddMonoid K] {f : Flow (Graph.bidirectedCapacity c) s t} (hf : f.IsMaximum) : f.val = TerminalCut.pairMinimumValue (G.edgeCutCapacity c) s t

The value of a maximum s–t flow of a weighted multigraph is the minimum cut value between s and t of the multigraph cut function.

theorem Graph.exists_flow_val_eq_edgeCutCapacity_mem {α : Type u} {β : Type v} {K : Type w} {G : Graph α β} [Fintype ↑G.vertexSet] [Fintype ↑G.edgeSet] [(x y : ↑G.vertexSet) → Fintype (G.BidirectedHom x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {c : ↑G.edgeSet → K} {s t : ↑G.vertexSet} (hst : s ≠ t) (hc : 0 ≤ c) (H : AddSubgroup K) (hcH : ∀ (e : ↑G.edgeSet), c e ∈ H) : ∃ (f : TauCeti.Flow (bidirectedCapacity c) s t), f.toFun.IsAcyclic ∧ (∀ ⦃x y : ↑G.vertexSet⦄ (a : G.BidirectedHom x y), f.toFun a ∈ H) ∧ ∃ (S : Finset ↑G.vertexSet), s ∈ S ∧ t ∉ S ∧ f.val = G.edgeCutCapacity c S

Undirected max-flow/min-cut theorem with integrality. For nonnegative capacities on the edges of a multigraph, all lying in an additive subgroup H, and distinct actual vertices s and t, some acyclic s–t flow with all values in H has value equal to the capacity of some set of actual vertices containing s but not t. By TauCeti.Flow.val_le_edgeCutCapacity this flow is maximum and this cut is minimum. Being acyclic, the flow vanishes on every loop arrow and on one of the two arrows of every nonloop edge.

theorem Graph.exists_flow_val_eq_edgeCutCapacity {α : Type u} {β : Type v} {K : Type w} {G : Graph α β} [Fintype ↑G.vertexSet] [Fintype ↑G.edgeSet] [(x y : ↑G.vertexSet) → Fintype (G.BidirectedHom x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {c : ↑G.edgeSet → K} {s t : ↑G.vertexSet} (hst : s ≠ t) (hc : 0 ≤ c) : ∃ (f : TauCeti.Flow (bidirectedCapacity c) s t), f.toFun.IsAcyclic ∧ ∃ (S : Finset ↑G.vertexSet), s ∈ S ∧ t ∉ S ∧ f.val = G.edgeCutCapacity c S

Undirected max-flow/min-cut theorem. For nonnegative capacities on the edges of a multigraph and distinct actual vertices s and t, some acyclic s–t flow has value equal to the capacity of some set of actual vertices containing s but not t. By TauCeti.Flow.val_le_edgeCutCapacity this flow is maximum and this cut is minimum.