Gomory–Hu trees of set functions

A set function f : Finset V → β on a finite ground set V assigns a value to every cut. A set X is a minimum s–t cut of f (IsMinCutBetween f s t X) when it contains s, misses t, and minimizes f among such sets. The cut function X ↦ w(δ(X)) of an undirected graph with edge weights w is the motivating example; it is symmetric (f Xᶜ = f X) and submodular.

A Gomory–Hu tree (cut-equivalent tree) of f ([GH61]; [Sch03], Section 15.4) is a spanning tree T on V such that for every tree edge uv, the side of T - uv containing u is a minimum u–v cut of f. This module defines Gomory–Hu trees, using the sides of tree edges SimpleGraph.edgeSide (CslibFrontier.Foundations.Combinatorics.SimpleGraph.EdgeSide), and proves that for every two distinct vertices s, t, some edge on the s–t path of a Gomory–Hu tree has a side that is a minimum s–t cut. Existence of Gomory–Hu trees for symmetric submodular functions is in CslibFrontier.Algorithms.Lean.GomoryHu.Existence, and the weighted-graph instance in CslibFrontier.Algorithms.Lean.GomoryHu.WeightedCut.

Main definitions

• Cslib.Algorithms.Lean.GomoryHu.IsMinCutBetween: X is a minimum s–t cut of f.
• Cslib.Algorithms.Lean.GomoryHu.IsGomoryHuTree: a spanning tree whose edge sides are minimum cuts between the edge's endpoints.

Main results

• Cslib.Algorithms.Lean.GomoryHu.exists_isMinCutBetween: minimum cuts exist between distinct elements, for values in a linear order.
• Cslib.Algorithms.Lean.GomoryHu.IsMinCutBetween.inter, Cslib.Algorithms.Lean.GomoryHu.IsMinCutBetween.union, Cslib.Algorithms.Lean.GomoryHu.IsMinCutBetween.sdiff: uncrossing of minimum cuts for a submodular function.
• Cslib.Algorithms.Lean.GomoryHu.IsGomoryHuTree.exists_isMinCutBetween_of_isPath: some edge of the s–t path of a Gomory–Hu tree has a side that is a minimum s–t cut.

References

• [GH61]
• [Sch03]

Minimum cuts between two elements

def Cslib.Algorithms.Lean.GomoryHu.IsMinCutBetween {V : Type u_1} {β : Type u_2} [Preorder β] (f : Finset V → β) (s t : V) (X : Finset V) : Prop

X is a minimum s–t cut of the set function f when it contains s, misses t, and f X ≤ f Y for every Y that contains s and misses t.

theorem Cslib.Algorithms.Lean.GomoryHu.IsMinCutBetween.left_mem {V : Type u_1} {β : Type u_2} [Preorder β] {f : Finset V → β} {s t : V} {X : Finset V} (h : IsMinCutBetween f s t X) : s ∈ X

theorem Cslib.Algorithms.Lean.GomoryHu.IsMinCutBetween.right_notMem {V : Type u_1} {β : Type u_2} [Preorder β] {f : Finset V → β} {s t : V} {X : Finset V} (h : IsMinCutBetween f s t X) : t ∉ X

theorem Cslib.Algorithms.Lean.GomoryHu.IsMinCutBetween.le {V : Type u_1} {β : Type u_2} [Preorder β] {f : Finset V → β} {s t : V} {X : Finset V} (h : IsMinCutBetween f s t X) {Y : Finset V} (hs : s ∈ Y) (ht : t ∉ Y) : f X ≤ f Y

theorem Cslib.Algorithms.Lean.GomoryHu.IsMinCutBetween.ne {V : Type u_1} {β : Type u_2} [Preorder β] {f : Finset V → β} {s t : V} {X : Finset V} (h : IsMinCutBetween f s t X) : s ≠ t

theorem Cslib.Algorithms.Lean.GomoryHu.IsMinCutBetween.compl {V : Type u_1} {β : Type u_2} [Preorder β] {f : Finset V → β} {s t : V} {X : Finset V} [Fintype V] [DecidableEq V] (hsym : ∀ (X : Finset V), f Xᶜ = f X) (h : IsMinCutBetween f s t X) : IsMinCutBetween f t s Xᶜ

For a symmetric set function, the complement of a minimum s–t cut is a minimum t–s cut.

theorem Cslib.Algorithms.Lean.GomoryHu.IsMinCutBetween.le_of_separates {V : Type u_1} {β : Type u_2} [Preorder β] {f : Finset V → β} {s t : V} {X : Finset V} [Fintype V] [DecidableEq V] (hsym : ∀ (X : Finset V), f Xᶜ = f X) (h : IsMinCutBetween f s t X) {Y : Finset V} (hY : s ∈ Y ↔ t ∉ Y) : f X ≤ f Y

For a symmetric set function, a minimum s–t cut is no larger than any set separating s from t, in either direction.

theorem Cslib.Algorithms.Lean.GomoryHu.exists_isMinCutBetween {V : Type u_1} {β : Type u_2} [LinearOrder β] [Finite V] (f : Finset V → β) {s t : V} (hst : s ≠ t) : ∃ (X : Finset V), IsMinCutBetween f s t X

Minimum cuts exist between distinct elements of a finite ground set.

theorem Cslib.Algorithms.Lean.GomoryHu.IsMinCutBetween.inter {V : Type u_1} {β : Type u_2} [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [DecidableEq V] {f : Finset V → β} {s t a b : V} {U X : Finset V} (hX : IsMinCutBetween f a b X) (hsub : Submodular.IsSubmodular f) (hU : IsMinCutBetween f s t U) (haU : a ∈ U) (htX : t ∉ X) : IsMinCutBetween f a b (X ∩ U)

Uncrossing. For a submodular f, if U is a minimum s–t cut, a ∈ U, and X is a minimum a–b cut missing t, then X ∩ U is a minimum a–b cut too.

theorem Cslib.Algorithms.Lean.GomoryHu.IsMinCutBetween.union {V : Type u_1} {β : Type u_2} [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [DecidableEq V] {f : Finset V → β} {s t a : V} {U A : Finset V} (hsub : Submodular.IsSubmodular f) (hU : IsMinCutBetween f s t U) (hA : IsMinCutBetween f a t A) (haU : a ∈ U) : IsMinCutBetween f s t (U ∪ A)

Uncrossing by union. For a submodular f, if U is a minimum s–t cut, A is a minimum a–t cut and a ∈ U, then U ∪ A is a minimum s–t cut too.

theorem Cslib.Algorithms.Lean.GomoryHu.IsMinCutBetween.sdiff {V : Type u_1} {β : Type u_2} [Fintype V] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [DecidableEq V] {f : Finset V → β} (hsym : ∀ (X : Finset V), f Xᶜ = f X) (hsub : Submodular.IsSubmodular f) {s t a : V} {U A : Finset V} (hU : IsMinCutBetween f s t U) (hA : IsMinCutBetween f a t A) (haU : a ∉ U) (hsA : s ∉ A) : IsMinCutBetween f s t (U \ A)

Uncrossing by difference. For a symmetric submodular f, if U is a minimum s–t cut, A is a minimum a–t cut, a ∉ U and s ∉ A, then U \ A is a minimum s–t cut too.

Gomory–Hu trees

structure Cslib.Algorithms.Lean.GomoryHu.IsGomoryHuTree {V : Type u_1} {β : Type u_2} [Fintype V] [Preorder β] (f : Finset V → β) (T : SimpleGraph V) : Prop

A Gomory–Hu tree (cut-equivalent tree) of a set function f on the finite ground set V ([GH61]; [Sch03], Section 15.4): a spanning tree T on V such that for every tree edge uv, the side of T - uv containing u is a minimum u–v cut of f.

• isTree : T.IsTree

  T is a spanning tree on V.

• isMinCutBetween_edgeSide ⦃u v : V⦄ : T.Adj u v → IsMinCutBetween f u v (T.edgeSide u v)

  For each tree edge uv, the side of T - uv containing u is a minimum u–v cut.

theorem Cslib.Algorithms.Lean.GomoryHu.IsGomoryHuTree.exists_isMinCutBetween_of_isPath {V : Type u_1} {β : Type u_2} [Fintype V] [LinearOrder β] {f : Finset V → β} {T : SimpleGraph V} (hT : IsGomoryHuTree f T) {s t : V} (hst : s ≠ t) {p : T.Walk s t} (hp : p.IsPath) : ∃ d ∈ p.darts, IsMinCutBetween f s t (T.edgeSide d.toProd.1 d.toProd.2)

Minimum cuts along a Gomory–Hu tree path. For distinct s and t, some dart of the s–t path in a Gomory–Hu tree has a side that is a minimum s–t cut.