Gomory–Hu trees of weighted undirected graphs

For a weighted multigraph W : V → V → ℕ (Cslib.WeightedCut.IsMultigraph: symmetric weights, zero diagonal), the cut function X ↦ cutWeight W X is symmetric and submodular, so it has a Gomory–Hu tree (Cslib.Algorithms.Lean.GomoryHu.exists_isGomoryHuTree). This module specializes the abstract theory to graphs ([GH61]; [Sch03], Section 15.4):

• the Gomory–Hu tree is cut-equivalent: for each tree edge uv, the side of T - uv containing u is a minimum u–v cut of the graph;
• it is flow-equivalent: weighting each tree edge uv by λ(u, v), the minimum s–t cut weight λ(s, t) (Cslib.WeightedCut.minCutBetween) is the least weight of an edge on the s–t path of the tree;
• consequently, the values λ(s, t) over all pairs s ≠ t take at most |V| - 1 distinct values.

By max-flow min-cut (Cslib.Algorithms.Lean.MaxFlow.Network.exists_maxFlow_eq_minCut), λ(s, t) is the value of a maximum s–t flow in the network with capacities W (Cslib.Algorithms.Lean.MaxFlow.Network.Flow.IsMaxFlow.value_eq_minCutBetween), so the Gomory–Hu tree also encodes all pairwise maximum flow values.

The results are existence statements for natural-number weights. Gusfield's construction of the tree with |V| - 1 maximum flow computations, without the contractions of Gomory and Hu ([Gus90]), is in CslibFrontier.Algorithms.Lean.GomoryHu.Gusfield (abstract cut oracle) and CslibFrontier.Algorithms.Lean.GomoryHu.Construction (Edmonds–Karp, with running time).

Main results

• Cslib.WeightedCut.isSubmodular_cutWeight: the cut function is submodular.
• Cslib.WeightedCut.isMinCutBetween_cutWeight_iff: minimum s–t cuts of the cut function are the sets containing s, missing t, of weight λ(s, t).
• Cslib.Algorithms.Lean.GomoryHu.exists_isGomoryHuTree_cutWeight: the Gomory–Hu theorem: every weighted multigraph on a nonempty finite vertex set has a cut-equivalent tree.
• Cslib.Algorithms.Lean.GomoryHu.IsGomoryHuTree.isLeast_minCutBetween: flow-equivalence of a Gomory–Hu tree.
• Cslib.Algorithms.Lean.GomoryHu.card_image_minCutBetween_le: at most |V| - 1 distinct minimum cut values.
• Cslib.Algorithms.Lean.MaxFlow.Network.Flow.IsMaxFlow.value_eq_minCutBetween: a maximum s–t flow has value λ(s, t).

References

• [GH61]
• [Gus90]
• [Sch03]

theorem Cslib.WeightedCut.isSubmodular_cutWeight_of_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] (W : V → V → M) (hW : ∀ (u v : V), 0 ≤ W u v) : Algorithms.Lean.Submodular.IsSubmodular (cutWeight W)

The cut function of a non-negative weight matrix over an ordered additive monoid is submodular.

theorem Cslib.WeightedCut.isSubmodular_cutWeight {V : Type u_1} [Fintype V] [DecidableEq V] (W : V → V → ℕ) : Algorithms.Lean.Submodular.IsSubmodular (cutWeight W)

The cut function of a weight matrix is submodular.

theorem Cslib.WeightedCut.isMinCutBetween_cutWeight_iff {V : Type u_1} [Fintype V] [DecidableEq V] (W : V → V → ℕ) {s t : V} {X : Finset V} : Algorithms.Lean.GomoryHu.IsMinCutBetween (cutWeight W) s t X ↔ s ∈ X ∧ t ∉ X ∧ cutWeight W X = minCutBetween W s t

The minimum s–t cuts of the cut function are the sets containing s and missing t whose weight is λ(s, t).

theorem Cslib.Algorithms.Lean.GomoryHu.exists_isGomoryHuTree_cutWeight {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] {W : V → V → ℕ} (hW : WeightedCut.IsMultigraph W) : ∃ (T : SimpleGraph V), IsGomoryHuTree (WeightedCut.cutWeight W) T

Gomory–Hu theorem ([GH61]; [Sch03], Section 15.4): every weighted multigraph W on a nonempty finite vertex set has a cut-equivalent tree, a spanning tree T on the vertices in which for every edge uv, the side of T - uv containing u is a minimum u–v cut of W. The edges of T need not be edges of W.

theorem Cslib.Algorithms.Lean.GomoryHu.IsGomoryHuTree.isLeast_minCutBetween {V : Type u_1} [Fintype V] [DecidableEq V] {W : V → V → ℕ} {T : SimpleGraph V} (hT : IsGomoryHuTree (WeightedCut.cutWeight W) T) {s t : V} (hst : s ≠ t) {p : T.Walk s t} (hp : p.IsPath) : IsLeast ((fun (d : T.Dart) => WeightedCut.minCutBetween W d.toProd.1 d.toProd.2) '' {d : T.Dart | d ∈ p.darts}) (WeightedCut.minCutBetween W s t)

Flow-equivalence of a Gomory–Hu tree ([GH61]): with each tree edge uv weighted by λ(u, v), the minimum s–t cut weight λ(s, t) is the least weight of an edge on the s–t path of the tree.

theorem Cslib.Algorithms.Lean.GomoryHu.card_image_minCutBetween_le {V : Type u_1} [Fintype V] [DecidableEq V] {W : V → V → ℕ} (hW : WeightedCut.IsMultigraph W) : (Finset.image (fun (p : V × V) => WeightedCut.minCutBetween W p.1 p.2) Finset.univ.offDiag).card ≤ Fintype.card V - 1

An undirected weighted graph on n vertices has at most n - 1 distinct minimum cut values λ(s, t) over pairs of distinct vertices ([GH61]).

theorem Cslib.Algorithms.Lean.MaxFlow.Network.IsMinCut.isMinCutBetween {V : Type u_1} [Fintype V] [DecidableEq V] {W : V → V → ℕ} {s t : V} {S : Finset V} (hS : { cap := W, s := s, t := t }.IsMinCut S) : GomoryHu.IsMinCutBetween (WeightedCut.cutWeight W) s t S

A minimum cut of the network with capacities W, source s and sink t is a minimum s–t cut of the cut function of W.

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.IsMaxFlow.value_eq_minCutBetween {V : Type u_1} [Fintype V] [DecidableEq V] {W : V → V → ℕ} {s t : V} (hst : s ≠ t) {f : { cap := W, s := s, t := t }.Flow} (hf : f.IsMaxFlow) : f.value = ↑(WeightedCut.minCutBetween W s t)

Max-flow min-cut for λ. In the network with capacities W, source s and sink t ≠ s, a maximum flow has value λ(s, t), the minimum s–t cut weight of W.