Documentation

CslibFrontier.Algorithms.Lean.GomoryHu.Existence

Existence of Gomory–Hu trees #

Every symmetric submodular set function f : Finset V → β on a nonempty finite ground set has a Gomory–Hu tree (cut-equivalent tree): a spanning tree on V such that for every tree edge uv, the side of T - uv containing u is a minimum u–v cut of f. Gomory and Hu ([GH61]; see also [Sch03], Section 15.4) prove this for the cut function of an undirected graph with nonnegative edge weights, which is symmetric and submodular. Their proof uses only these two properties, and the statement for symmetric submodular functions is its standard abstraction.

Proof #

The proof follows the recursive scheme of Gomory and Hu, phrased without contraction. A partial tree on a set R of terminals is a set of labelled edges (u, v, S) with u, v ∈ R, each S a minimum u–v cut, the labels laminar with respect to the edges (an edge's label does not separate the endpoints of any other edge), every two terminals joined by a chain of edges, and every vertex represented by a terminal on the same side of every label. Pick distinct terminals s, t ∈ R and a minimum s–t cut U. By the uncrossing lemma Cslib.Algorithms.Lean.GomoryHu.IsMinCutBetween.inter, the terminals of R ∩ U have minimum cuts that do not split Uᶜ, and those of R \ U have minimum cuts that do not split U. Recursively build partial trees on both sides and join them by the edge r₁ r₂ labelled U, where r₁ is the terminal of R ∩ U representing t and r₂ the terminal of R \ U representing s. The set U is a minimum r₁–r₂ cut: a cheaper r₁–r₂ separator would cross an edge on a tree chain whose label separates s from t, and all such labels weigh at least f U.

Main results #

References #

From a partial tree on all vertices to a Gomory–Hu tree #

theorem Cslib.Algorithms.Lean.GomoryHu.exists_isGomoryHuTree {V : Type u_1} {β : Type u_2} [Fintype V] [DecidableEq V] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [Nonempty V] {f : Finset V → β} (hsym : ∀ (X : Finset V), f Xᶜ = f X) (hsub : Submodular.IsSubmodular f) :
∃ (T : SimpleGraph V), IsGomoryHuTree f T

Gomory–Hu theorem for symmetric submodular set functions: every symmetric submodular f : Finset V → β on a nonempty finite ground set V has a Gomory–Hu tree, a spanning tree T on V in which for every edge uv, the side of T - uv containing u is a minimum u–v cut of f. This is the cut-equivalent form. [GH61] (see also [Sch03], Section 15.4) proves it for cut functions of undirected graphs; the statement for symmetric submodular functions is the standard abstraction of that proof, which uses only symmetry and submodularity. The graph case is Cslib.Algorithms.Lean.GomoryHu.exists_isGomoryHuTree_cutWeight.