Gomory–Hu trees with n - 1 maximum flow computations

An executable TimeM construction of a Gomory–Hu tree of a weighted multigraph W : Fin n → Fin n → ℕ, following Gusfield's contraction-free algorithm ([Gus90]): one Edmonds–Karp maximum flow computation ([EK72]) per non-root vertex, so n - 1 in total, all on the original graph, plus O(n) bookkeeping per vertex on a parent array and edge-weight array fl. Correctness is transferred from the abstract algorithm Cslib.Algorithms.Lean.GomoryHu.gusfieldWithWeights of CslibFrontier.Algorithms.Lean.GomoryHu.Gusfield, with the Edmonds–Karp minimum cut and maximum flow value as the oracle.

Main definitions

• Cslib.Algorithms.Lean.GomoryHu.Output: parent array parent and edge-weight array weight returned by Gusfield's algorithm.
• Cslib.Algorithms.Lean.GomoryHu.gomoryHuM: Gusfield's algorithm over Fin n in TimeM ℕ, returning the parent array and edge weights of the tree.
• Cslib.Algorithms.Lean.GomoryHu.ekCut, Cslib.Algorithms.Lean.GomoryHu.ekValue: the minimum cut and maximum flow value returned by edmondsKarpM.

Main results

• Cslib.Algorithms.Lean.GomoryHu.isGomoryHuTree_gomoryHuM: the parent graph of the output is a Gomory–Hu tree of cutWeight W (cut-equivalent: the side of each tree edge uv containing u is a minimum u–v cut of W).
• Cslib.Algorithms.Lean.GomoryHu.vget_gomoryHuM_weight_eq_minCutBetween: for every vertex u : Fin n, the recorded weight vget (gomoryHuM W adj r).ret.weight u equals minCutBetween W u (vget (gomoryHuM W adj r).ret.parent u) (0 at the root r, vget_gomoryHuM_weight_root).
• Cslib.Algorithms.Lean.GomoryHu.vget_gomoryHuM, Cslib.Algorithms.Lean.GomoryHu.vget_gomoryHuM_parent, Cslib.Algorithms.Lean.GomoryHu.vget_gomoryHuM_weight: the output agrees with the abstract gusfieldParent and gusfieldWithWeights run with ekCut and ekValue.
• Cslib.Algorithms.Lean.GomoryHu.gomoryHuM_time_le_of_forall: the charged time is at most 3 n plus n - 1 times (any bound on one Edmonds–Karp computation, plus n + 3).
• Cslib.Algorithms.Lean.GomoryHu.gomoryHuM_time_le: the same with the Edmonds–Karp bound edmondsKarpM_time_le, O(n m²) per computation for m edges, so O(n² m²) in total.
• Cslib.Algorithms.Lean.GomoryHu.gomoryHuM_time_le_dense: O(n ^ 6) with dense adjacency lists.

Cost model

The unit-cost model of Cslib.Algorithms.Lean.MaxFlow.edmondsKarpM, extended with Finset membership on the returned cut and reading out.flow.value (netOut N.s, an O(n) sum over Fin n) as free primitives: Vector reads and writes, those membership tests, that Flow.value sum, equality tests on Fin n, and evaluating W u v count as O(1) primitives inside charged steps. (Computing out.flow.value once per step would add O(n²) in total, subsumed by the re-hanging scan; O(n) Finset membership tests inside each n-vertex scan would add O(n³) in total.) Charged: n ticks to allocate the parent array p, n ticks to allocate the edge-weight array fl, 1 tick per vertex for the loop test s = r, and for each non-root vertex s: 1 tick to read its parent, the full Edmonds–Karp cost, n ticks for the re-hanging scan over all vertices, 1 tick for the final swap test and its parent writes, and 1 tick to record the edge weight in fl.

Limitations

The weights of W are natural numbers, and only Edmonds–Karp is instantiated as the maximum flow oracle (gomoryHuM_time_le_of_forall accepts any per-call bound).

References

• [EK72]
• [GH61]
• [Gus90]

structure Cslib.Algorithms.Lean.GomoryHu.Output (n : ℕ) : Type

Output of Gusfield's Gomory–Hu tree construction on Fin n: the parent array parent rooted at r and the edge-weight array weight storing λ(u, parent[u]) for every non-root u (0 at the root r).

• parent : Vector (Fin n) n

  Parent array of the tree (vget parent r = r).

• weight : Vector ℕ n

  Edge weight λ(u, vget parent u) for every non-root vertex u (0 at r).

@[instance_reducible]

instance Cslib.Algorithms.Lean.GomoryHu.instDecidableEqOutput {n✝ : ℕ} : DecidableEq (Output n✝)

def Cslib.Algorithms.Lean.GomoryHu.instDecidableEqOutput.decEq {n✝ : ℕ} (x✝ x✝¹ : Output n✝) : Decidable (x✝ = x✝¹)

def Cslib.Algorithms.Lean.GomoryHu.rehangM {n : ℕ} (p : Vector (Fin n) n) (s t : Fin n) (X : Finset (Fin n)) : List (Fin n) → Vector (Fin n) n → TimeM ℕ (Vector (Fin n) n)

Re-hang below s every vertex z ∈ zs whose parent in p is t and which lies in X, writing into acc and charging 1 tick per scanned vertex.

@[simp]

theorem Cslib.Algorithms.Lean.GomoryHu.rehangM_time {n : ℕ} (p : Vector (Fin n) n) (s t : Fin n) (X : Finset (Fin n)) (zs : List (Fin n)) (acc : Vector (Fin n) n) : (rehangM p s t X zs acc).time = zs.length

theorem Cslib.Algorithms.Lean.GomoryHu.vget_rehangM {n : ℕ} (p : Vector (Fin n) n) (s t : Fin n) (X : Finset (Fin n)) (zs : List (Fin n)) (acc : Vector (Fin n) n) (z : Fin n) : MaxFlow.vget (rehangM p s t X zs acc).ret z = if z ∈ zs ∧ MaxFlow.vget p z = t ∧ z ∈ X then s else MaxFlow.vget acc z

def Cslib.Algorithms.Lean.GomoryHu.ekCut {n : ℕ} (W : Fin n → Fin n → ℕ) (adj : Fin n → List (Fin n)) (s t : Fin n) : Finset (Fin n)

The minimum cut returned by the Edmonds–Karp solver on the network with capacities W, source s and sink t.

def Cslib.Algorithms.Lean.GomoryHu.ekValue {n : ℕ} (W : Fin n → Fin n → ℕ) (adj : Fin n → List (Fin n)) (s t : Fin n) : ℕ

The maximum flow value returned by the Edmonds–Karp solver on the network with capacities W, source s and sink t.

theorem Cslib.Algorithms.Lean.GomoryHu.isMinCutBetween_ekCut {n : ℕ} {W : Fin n → Fin n → ℕ} {adj : Fin n → List (Fin n)} (hadj : ∀ (u v : Fin n), u ≠ v → 0 < W u v + W v u → v ∈ adj u) {s t : Fin n} (hst : s ≠ t) : IsMinCutBetween (WeightedCut.cutWeight W) s t (ekCut W adj s t)

The Edmonds–Karp cut is a minimum s–t cut of the cut function of W, for adjacency lists covering the edges of W.

theorem Cslib.Algorithms.Lean.GomoryHu.ekValue_eq_cutWeight {n : ℕ} {W : Fin n → Fin n → ℕ} {adj : Fin n → List (Fin n)} (hadj : ∀ (u v : Fin n), u ≠ v → 0 < W u v + W v u → v ∈ adj u) {s t : Fin n} (hst : s ≠ t) : ekValue W adj s t = WeightedCut.cutWeight W (ekCut W adj s t)

The Edmonds–Karp maximum flow value equals the weight of ekCut W adj s t, for adjacency lists covering the edges of W.

def Cslib.Algorithms.Lean.GomoryHu.gusfieldStepM {n : ℕ} (W : Fin n → Fin n → ℕ) (adj : Fin n → List (Fin n)) (p : Vector (Fin n) n) (fl : Vector ℕ n) (s : Fin n) : TimeM ℕ (Output n)

One step of Gusfield's algorithm on the parent array p and weight array fl for vertex s: one Edmonds–Karp computation between s and its parent t, a scan re-hanging the vertices on the s-side below s, the swap of s and t when the parent of t is on the s-side, and the weight update from the maximum flow value (fl[s] := val, or on a swap fl[s] := fl[t] and fl[t] := val).

theorem Cslib.Algorithms.Lean.GomoryHu.gusfieldStepM_time {n : ℕ} (W : Fin n → Fin n → ℕ) (adj : Fin n → List (Fin n)) (p : Vector (Fin n) n) (fl : Vector ℕ n) (s : Fin n) : (gusfieldStepM W adj p fl s).time = (MaxFlow.edmondsKarpM { cap := W, s := s, t := MaxFlow.vget p s } adj).time + n + 3

theorem Cslib.Algorithms.Lean.GomoryHu.vget_gusfieldStepM_parent {n : ℕ} (W : Fin n → Fin n → ℕ) (adj : Fin n → List (Fin n)) (p : Vector (Fin n) n) (fl : Vector ℕ n) (s z : Fin n) : MaxFlow.vget (gusfieldStepM W adj p fl s).ret.parent z = gusfieldStep (MaxFlow.vget p) s (ekCut W adj s (MaxFlow.vget p s)) z

theorem Cslib.Algorithms.Lean.GomoryHu.vget_gusfieldStepM_weight {n : ℕ} (W : Fin n → Fin n → ℕ) (adj : Fin n → List (Fin n)) (p : Vector (Fin n) n) (fl : Vector ℕ n) (s z : Fin n) : MaxFlow.vget (gusfieldStepM W adj p fl s).ret.weight z = gusfieldStepWeight (MaxFlow.vget p) (MaxFlow.vget fl) s (ekCut W adj s (MaxFlow.vget p s)) (ekValue W adj s (MaxFlow.vget p s)) z

The weight array computed by gusfieldStepM agrees pointwise with gusfieldStepWeight.

def Cslib.Algorithms.Lean.GomoryHu.gomoryHuLoopM {n : ℕ} (W : Fin n → Fin n → ℕ) (adj : Fin n → List (Fin n)) (r : Fin n) : List (Fin n) → Vector (Fin n) n → Vector ℕ n → TimeM ℕ (Output n)

Gusfield's loop over the vertices l, skipping the root r and tracking both parent and edge-weight arrays.

theorem Cslib.Algorithms.Lean.GomoryHu.vget_gomoryHuLoopM {n : ℕ} (W : Fin n → Fin n → ℕ) (adj : Fin n → List (Fin n)) (r : Fin n) (l : List (Fin n)) (p : Vector (Fin n) n) (fl : Vector ℕ n) : MaxFlow.vget (gomoryHuLoopM W adj r l p fl).ret.parent = (gusfieldWeightLoop (ekCut W adj) (ekValue W adj) r l (MaxFlow.vget p) (MaxFlow.vget fl)).1 ∧ MaxFlow.vget (gomoryHuLoopM W adj r l p fl).ret.weight = (gusfieldWeightLoop (ekCut W adj) (ekValue W adj) r l (MaxFlow.vget p) (MaxFlow.vget fl)).2

def Cslib.Algorithms.Lean.GomoryHu.gomoryHuM {n : ℕ} (W : Fin n → Fin n → ℕ) (adj : Fin n → List (Fin n)) (r : Fin n) : TimeM ℕ (Output n)

Gusfield's Gomory–Hu tree algorithm ([Gus90]) over Fin n in TimeM ℕ: start from the star centred at the root r with 0 initial weights, and process the other vertices in order with one Edmonds–Karp computation each. Returns both the parent array parent and the tree edge weights weight.

theorem Cslib.Algorithms.Lean.GomoryHu.vget_gomoryHuM_parent {n : ℕ} (W : Fin n → Fin n → ℕ) (adj : Fin n → List (Fin n)) (r : Fin n) : MaxFlow.vget (gomoryHuM W adj r).ret.parent = (gusfieldWithWeights (ekCut W adj) (ekValue W adj) r 0 (List.finRange n)).1

The parent array returned by gomoryHuM agrees pointwise with the first component of gusfieldWithWeights.

theorem Cslib.Algorithms.Lean.GomoryHu.vget_gomoryHuM {n : ℕ} (W : Fin n → Fin n → ℕ) (adj : Fin n → List (Fin n)) (r : Fin n) : MaxFlow.vget (gomoryHuM W adj r).ret.parent = gusfieldParent (ekCut W adj) r (List.finRange n)

The parent array returned by gomoryHuM agrees pointwise with gusfieldParent.

theorem Cslib.Algorithms.Lean.GomoryHu.vget_gomoryHuM_weight {n : ℕ} (W : Fin n → Fin n → ℕ) (adj : Fin n → List (Fin n)) (r : Fin n) : MaxFlow.vget (gomoryHuM W adj r).ret.weight = (gusfieldWithWeights (ekCut W adj) (ekValue W adj) r 0 (List.finRange n)).2

The weight array returned by gomoryHuM agrees pointwise with the second component of gusfieldWithWeights.

theorem Cslib.Algorithms.Lean.GomoryHu.isGomoryHuTree_gomoryHuM {n : ℕ} {W : Fin n → Fin n → ℕ} (hW : WeightedCut.IsMultigraph W) {adj : Fin n → List (Fin n)} (hadj : ∀ (u v : Fin n), u ≠ v → 0 < W u v + W v u → v ∈ adj u) (r : Fin n) : IsGomoryHuTree (WeightedCut.cutWeight W) (SimpleGraph.parentGraph (MaxFlow.vget (gomoryHuM W adj r).ret.parent))

Correctness of Gusfield's algorithm with Edmonds–Karp ([Gus90]): for a weighted multigraph W on Fin n and adjacency lists adj covering its edges, the parent array computed by gomoryHuM is a Gomory–Hu tree of W: for every tree edge uv, the side of T - uv containing u is a minimum u–v cut of W.

theorem Cslib.Algorithms.Lean.GomoryHu.vget_gomoryHuM_weight_root {n : ℕ} {W : Fin n → Fin n → ℕ} (hW : WeightedCut.IsMultigraph W) {adj : Fin n → List (Fin n)} (hadj : ∀ (u v : Fin n), u ≠ v → 0 < W u v + W v u → v ∈ adj u) (r : Fin n) : MaxFlow.vget (gomoryHuM W adj r).ret.weight r = 0

The recorded root weight is 0.

theorem Cslib.Algorithms.Lean.GomoryHu.vget_gomoryHuM_weight_eq_minCutBetween {n : ℕ} {W : Fin n → Fin n → ℕ} (hW : WeightedCut.IsMultigraph W) {adj : Fin n → List (Fin n)} (hadj : ∀ (u v : Fin n), u ≠ v → 0 < W u v + W v u → v ∈ adj u) (r u : Fin n) : MaxFlow.vget (gomoryHuM W adj r).ret.weight u = WeightedCut.minCutBetween W u (MaxFlow.vget (gomoryHuM W adj r).ret.parent u)

Correctness of the edge weights returned by gomoryHuM ([Gus90]): for every vertex u : Fin n, the weight vget (gomoryHuM W adj r).ret.weight u equals the minimum cut weight minCutBetween W u (vget (gomoryHuM W adj r).ret.parent u) between u and its parent (0 at the root r).

theorem Cslib.Algorithms.Lean.GomoryHu.gomoryHuLoopM_time_le {n : ℕ} (W : Fin n → Fin n → ℕ) (adj : Fin n → List (Fin n)) (r : Fin n) {B : ℕ} (hB : ∀ (s t : Fin n), (MaxFlow.edmondsKarpM { cap := W, s := s, t := t } adj).time ≤ B) (l : List (Fin n)) (p : Vector (Fin n) n) (fl : Vector ℕ n) : (gomoryHuLoopM W adj r l p fl).time ≤ l.length + (List.filter (fun (x : Fin n) => decide (x ≠ r)) l).length * (B + n + 3)

theorem Cslib.Algorithms.Lean.GomoryHu.gomoryHuM_time_le_of_forall {n : ℕ} (W : Fin n → Fin n → ℕ) (adj : Fin n → List (Fin n)) (r : Fin n) {B : ℕ} (hB : ∀ (s t : Fin n), (MaxFlow.edmondsKarpM { cap := W, s := s, t := t } adj).time ≤ B) : (gomoryHuM W adj r).time ≤ 3 * n + (n - 1) * (B + n + 3)

Running time of Gusfield's algorithm. If every Edmonds–Karp computation on the capacities W takes at most B charged steps, gomoryHuM W adj r takes at most 3 n + (n - 1) (B + n + 3): 2 n to allocate the parent and weight arrays, 1 per vertex for the loop, and for each of the n - 1 non-root vertices one maximum flow computation, the n-step re-hanging scan and 3 steps of pointer and weight updates.

theorem Cslib.Algorithms.Lean.GomoryHu.gomoryHuM_time_le {n : ℕ} {W : Fin n → Fin n → ℕ} {adj : Fin n → List (Fin n)} (hadj : ∀ (u v : Fin n), u ≠ v → 0 < W u v + W v u → v ∈ adj u) (r : Fin n) : (gomoryHuM W adj r).time ≤ 3 * n + (n - 1) * ((MaxFlow.adjSteps adj * (n / 2) + 2) * (MaxFlow.adjSteps adj + 5 * n) + n + 3)

Running time with sparse adjacency lists. With adjacency lists adj covering the edges of W, Gusfield's algorithm makes n - 1 Edmonds–Karp computations, each within (adjSteps adj * (n / 2) + 2) * (adjSteps adj + 5 n) steps (O(n m²) for m edges), plus O(n) bookkeeping per computation.

theorem Cslib.Algorithms.Lean.GomoryHu.gomoryHuM_time_le_dense {n : ℕ} {W : Fin n → Fin n → ℕ} (r : Fin n) : (gomoryHuM W (MaxFlow.defaultAdj n) r).time ≤ 3 * n + (n - 1) * ((n * n * (n / 2) + 2) * (n * n + 5 * n) + n + 3)

Running time with dense adjacency lists: O(n ^ 6).