Gusfield's algorithm for Gomory–Hu trees

Gusfield ([Gus90]) showed that a Gomory–Hu tree can be computed with n - 1 minimum cut computations in the original graph, without the contractions of Gomory and Hu's construction ([GH61]). The tree is kept as a parent function p with root r. Initially every vertex hangs from r. The other vertices s are processed once each: with t = p s and a minimum s–t cut X, every other vertex whose parent is t and which lies in X is re-hung below s, and if the parent of t lies in X, then s takes the place of t (p s := p t, p t := s).

This module states the algorithm for an arbitrary cut oracle and an arbitrary processing order, and proves it correct for every symmetric submodular set function: if the oracle returns minimum cuts, the final parent graph is a Gomory–Hu tree. The oracle may return any minimum cut. The executable version over Fin n with Edmonds–Karp as the oracle, and its running time, are in CslibFrontier.Algorithms.Lean.GomoryHu.Construction.

Proof

After processing a set P ∋ r of vertices, the invariant is: the parent of every vertex is in P; every i ∈ P other than r carries a minimum i–p i cut S i that no other parent pointer crosses (z ∈ S i ↔ p z ∈ S i for z ≠ i); and every vertex is joined to r by parent pointers. To process s ∉ P with parent t, the cut X returned by the oracle is uncrossed with the sides, away from t, of the parent edges at t (IsMinCutBetween.union, IsMinCutBetween.sdiff). This gives a minimum s–t cut U that agrees with X on the vertices the algorithm inspects and that no other parent pointer crosses. A re-hung vertex i keeps its label: a minimum i–t cut missing s is a minimum i–s cut when some minimum s–t cut contains i. In the swap case, s inherits the label of t and t gets Uᶜ; otherwise s gets U. Once every vertex is processed, the parent graph is connected with n - 1 edges, hence a tree, and by edgeSide_eq_of_forall_adj the side of each parent edge (u, p u) containing u is S u.

Main definitions

• Cslib.Algorithms.Lean.GomoryHu.gusfieldStep, Cslib.Algorithms.Lean.GomoryHu.gusfieldLoop, Cslib.Algorithms.Lean.GomoryHu.gusfieldParent: Gusfield's algorithm on parent functions, with a cut oracle C : V → V → Finset V.
• Cslib.Algorithms.Lean.GomoryHu.gusfieldStepWeight, Cslib.Algorithms.Lean.GomoryHu.gusfieldWeightLoop, Cslib.Algorithms.Lean.GomoryHu.gusfieldWithWeights: the same algorithm tracking the cut value w u = f (S u) alongside the parent function, given a value oracle val : V → V → β.

The tree of the output is its parent graph SimpleGraph.parentGraph (CslibFrontier.Foundations.Combinatorics.SimpleGraph.Acyclic).

Main results

• Cslib.Algorithms.Lean.GomoryHu.isGomoryHuTree_gusfieldParent: for a symmetric submodular f and an oracle returning minimum cuts, Gusfield's algorithm computes a Gomory–Hu tree of f.
• Cslib.Algorithms.Lean.GomoryHu.gusfieldWithWeights_spec, Cslib.Algorithms.Lean.GomoryHu.isGomoryHuTree_gusfieldWithWeights, Cslib.Algorithms.Lean.GomoryHu.gusfieldWithWeights_weight_eq, Cslib.Algorithms.Lean.GomoryHu.isMinCutBetween_gusfieldWithWeights_edgeSide: gusfieldWithWeights computes the same Gomory–Hu tree together with w u = f (edgeSide (parentGraph p) u (p u)) for every non-root u.

References

• [GH61]
• [Gus90]

Iterated uncrossing

Gusfield's algorithm

def Cslib.Algorithms.Lean.GomoryHu.gusfieldStep {V : Type u_1} [DecidableEq V] (p : V → V) (s : V) (X : Finset V) : V → V

One step of Gusfield's algorithm ([Gus90]) on the parent function p: given the vertex s with current parent t = p s and an s–t cut X ∋ s, every other vertex with parent t on the s-side of X is re-hung below s; if moreover the parent of t lies on the s-side, s takes the place of t (p s := p t, p t := s).

def Cslib.Algorithms.Lean.GomoryHu.gusfieldLoop {V : Type u_1} [DecidableEq V] (C : V → V → Finset V) (r : V) : List V → (V → V) → V → V

Gusfield's algorithm: process the vertices of l in order (skipping the root r), each with one call C s (p s) of the cut oracle.

def Cslib.Algorithms.Lean.GomoryHu.gusfieldParent {V : Type u_1} [DecidableEq V] (C : V → V → Finset V) (r : V) (l : List V) : V → V

The parent function computed by Gusfield's algorithm with cut oracle C, root r and vertex order l, starting from the star centred at r.

def Cslib.Algorithms.Lean.GomoryHu.gusfieldStepWeight {V : Type u_1} {β : Type u_2} [DecidableEq V] (p : V → V) (w : V → β) (s : V) (X : Finset V) (v : β) : V → β

One step of Gusfield's algorithm on the edge-weight function w, updating edge weights from the cut value v for (s, p s). On a swap (p (p s) ∈ X), s inherits w (p s) and p s receives v; otherwise s receives v.

def Cslib.Algorithms.Lean.GomoryHu.gusfieldWeightLoop {V : Type u_1} {β : Type u_2} [DecidableEq V] (C : V → V → Finset V) (val : V → V → β) (r : V) : List V → (V → V) → (V → β) → (V → V) × (V → β)

Gusfield's loop tracking both the parent function p and edge-weight function w, using cut oracle C and cut-value oracle val.

def Cslib.Algorithms.Lean.GomoryHu.gusfieldWithWeights {V : Type u_1} {β : Type u_2} [DecidableEq V] (C : V → V → Finset V) (val : V → V → β) (r : V) (w₀ : β) (l : List V) : (V → V) × (V → β)

The parent and weight functions computed by Gusfield's algorithm with cut oracle C, value oracle val, root r, initial weight w₀, and vertex order l.

theorem Cslib.Algorithms.Lean.GomoryHu.fst_gusfieldWeightLoop {V : Type u_1} {β : Type u_2} [DecidableEq V] (C : V → V → Finset V) (val : V → V → β) (r : V) (l : List V) (p : V → V) (w : V → β) : (gusfieldWeightLoop C val r l p w).1 = gusfieldLoop C r l p

Ignoring edge weights, gusfieldWeightLoop computes the same parent function as gusfieldLoop.

theorem Cslib.Algorithms.Lean.GomoryHu.fst_gusfieldWithWeights {V : Type u_1} {β : Type u_2} [DecidableEq V] (C : V → V → Finset V) (val : V → V → β) (r : V) (w₀ : β) (l : List V) : (gusfieldWithWeights C val r w₀ l).1 = gusfieldParent C r l

The first component of gusfieldWithWeights equals gusfieldParent.

The invariant

The step

The processed tree edges at t

Correctness

theorem Cslib.Algorithms.Lean.GomoryHu.isGomoryHuTree_gusfieldParent {V : Type u_1} {β : Type u_2} [Fintype V] [DecidableEq V] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] {f : Finset V → β} (hsym : ∀ (X : Finset V), f Xᶜ = f X) (hsub : Submodular.IsSubmodular f) {C : V → V → Finset V} (hC : ∀ (s t : V), s ≠ t → IsMinCutBetween f s t (C s t)) (r : V) {l : List V} (hnd : l.Nodup) (hl : ∀ (x : V), x ≠ r → x ∈ l) : IsGomoryHuTree f (SimpleGraph.parentGraph (gusfieldParent C r l))

Correctness of Gusfield's algorithm ([Gus90]). For a symmetric submodular f, a cut oracle C returning a minimum s–t cut for all s ≠ t, a root r and a duplicate-free list l containing every vertex other than r, the parent function computed by Gusfield's algorithm is a Gomory–Hu tree of f.

theorem Cslib.Algorithms.Lean.GomoryHu.gusfieldWithWeights_spec {V : Type u_1} {β : Type u_2} [Fintype V] [DecidableEq V] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] {f : Finset V → β} (hsym : ∀ (X : Finset V), f Xᶜ = f X) (hsub : Submodular.IsSubmodular f) {C : V → V → Finset V} {val : V → V → β} (hC : ∀ (s t : V), s ≠ t → IsMinCutBetween f s t (C s t)) (hval : ∀ (s t : V), s ≠ t → val s t = f (C s t)) (r : V) (w₀ : β) {l : List V} (hnd : l.Nodup) (hl : ∀ (x : V), x ≠ r → x ∈ l) : have res := gusfieldWithWeights C val r w₀ l; IsGomoryHuTree f (SimpleGraph.parentGraph res.1) ∧ res.1 r = r ∧ res.2 r = w₀ ∧ ∀ (u : V), u ≠ r → IsMinCutBetween f u (res.1 u) ((SimpleGraph.parentGraph res.1).edgeSide u (res.1 u)) ∧ res.2 u = f ((SimpleGraph.parentGraph res.1).edgeSide u (res.1 u))

Bundled correctness of Gusfield's algorithm with edge weights ([Gus90]): for a symmetric submodular f, cut oracle C, consistent value oracle val s t = f (C s t), root r, initial weight w₀ and duplicate-free list l covering V \ {r}, gusfieldWithWeights produces a Gomory–Hu parent graph with fixed root r, root weight w₀, and non-root weights equal to f on each tree-edge side.

theorem Cslib.Algorithms.Lean.GomoryHu.isGomoryHuTree_gusfieldWithWeights {V : Type u_1} {β : Type u_2} [Fintype V] [DecidableEq V] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] {f : Finset V → β} (hsym : ∀ (X : Finset V), f Xᶜ = f X) (hsub : Submodular.IsSubmodular f) {C : V → V → Finset V} {val : V → V → β} (hC : ∀ (s t : V), s ≠ t → IsMinCutBetween f s t (C s t)) (r : V) (w₀ : β) {l : List V} (hnd : l.Nodup) (hl : ∀ (x : V), x ≠ r → x ∈ l) : IsGomoryHuTree f (SimpleGraph.parentGraph (gusfieldWithWeights C val r w₀ l).1)

Correctness of Gusfield's algorithm with edge weights ([Gus90]): for a symmetric submodular f, a cut oracle C returning minimum cuts, a root r and a duplicate-free list l covering V \ {r}, the parent component of gusfieldWithWeights is a Gomory–Hu tree of f.

theorem Cslib.Algorithms.Lean.GomoryHu.isMinCutBetween_gusfieldWithWeights_edgeSide {V : Type u_1} {β : Type u_2} [Fintype V] [DecidableEq V] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] {f : Finset V → β} (hsym : ∀ (X : Finset V), f Xᶜ = f X) (hsub : Submodular.IsSubmodular f) {C : V → V → Finset V} {val : V → V → β} (hC : ∀ (s t : V), s ≠ t → IsMinCutBetween f s t (C s t)) (hval : ∀ (s t : V), s ≠ t → val s t = f (C s t)) (r : V) (w₀ : β) {l : List V} (hnd : l.Nodup) (hl : ∀ (x : V), x ≠ r → x ∈ l) {u : V} (hur : u ≠ r) : have res := gusfieldWithWeights C val r w₀ l; IsMinCutBetween f u (res.1 u) ((SimpleGraph.parentGraph res.1).edgeSide u (res.1 u))

For every non-root vertex u, the tree-edge side containing u in gusfieldWithWeights is a minimum u–p u cut of f.

theorem Cslib.Algorithms.Lean.GomoryHu.gusfieldWithWeights_weight_eq {V : Type u_1} {β : Type u_2} [Fintype V] [DecidableEq V] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] {f : Finset V → β} (hsym : ∀ (X : Finset V), f Xᶜ = f X) (hsub : Submodular.IsSubmodular f) {C : V → V → Finset V} {val : V → V → β} (hC : ∀ (s t : V), s ≠ t → IsMinCutBetween f s t (C s t)) (hval : ∀ (s t : V), s ≠ t → val s t = f (C s t)) (r : V) (w₀ : β) {l : List V} (hnd : l.Nodup) (hl : ∀ (x : V), x ≠ r → x ∈ l) {u : V} (hur : u ≠ r) : have res := gusfieldWithWeights C val r w₀ l; res.2 u = f ((SimpleGraph.parentGraph res.1).edgeSide u (res.1 u))

Edge-weight correctness of Gusfield's algorithm ([Gus90]): for every non-root vertex u, the weight recorded by gusfieldWithWeights equals f on the tree-edge side containing u.

theorem Cslib.Algorithms.Lean.GomoryHu.gusfieldWithWeights_parent_root {V : Type u_1} {β : Type u_2} [Fintype V] [DecidableEq V] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] {f : Finset V → β} (hsym : ∀ (X : Finset V), f Xᶜ = f X) (hsub : Submodular.IsSubmodular f) {C : V → V → Finset V} {val : V → V → β} (hC : ∀ (s t : V), s ≠ t → IsMinCutBetween f s t (C s t)) (r : V) (w₀ : β) {l : List V} (hnd : l.Nodup) (hl : ∀ (x : V), x ≠ r → x ∈ l) : (gusfieldWithWeights C val r w₀ l).1 r = r

The root r remains its own parent in gusfieldWithWeights.

theorem Cslib.Algorithms.Lean.GomoryHu.gusfieldWithWeights_weight_root {V : Type u_1} {β : Type u_2} [Fintype V] [DecidableEq V] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] {f : Finset V → β} (hsym : ∀ (X : Finset V), f Xᶜ = f X) (hsub : Submodular.IsSubmodular f) {C : V → V → Finset V} {val : V → V → β} (hC : ∀ (s t : V), s ≠ t → IsMinCutBetween f s t (C s t)) (hval : ∀ (s t : V), s ≠ t → val s t = f (C s t)) (r : V) (w₀ : β) {l : List V} (hnd : l.Nodup) (hl : ∀ (x : V), x ≠ r → x ∈ l) : (gusfieldWithWeights C val r w₀ l).2 r = w₀

The weight recorded at the root r in gusfieldWithWeights equals the initial weight w₀.