The Stoer–Wagner minimum cut algorithm

The Stoer–Wagner algorithm [SW97] computes a global minimum cut of a weighted multigraph W : Fin n → Fin n → ℕ (Cslib.WeightedCut.IsMultigraph) deterministically. Each phase computes a maximum adjacency ordering of the current supervertices by maximum adjacency search (Cslib.WeightedCut.maSearch), records the cut of the phase, the cut {t} of its last vertex t, and merges t into the second to last vertex s. After n - 1 phases one supervertex is left, and the lightest cut of the phase is a global minimum cut.

Correctness has two parts. By the MA-ordering lemma (Cslib.WeightedCut.cutWeight_singleton_le_of_isMAOrdering), the cut of the phase weighs at most every cut separating s and t. A cut not separating s and t survives merging them with the same weight (Cslib.WeightedCut.cutWeight_contractCut), so the minimum cut weight is the smaller of the weight of the cut of the phase and the minimum cut weight after the merge (minCut_eq_min_contractMatrix, the phase recursion of [SW97]). Contraction is that of CslibFrontier.Foundations.Combinatorics.WeightedCut.Contraction (contractMatrix, contractPart), which keeps the supervertices as Fin m and moves the last one into the freed slot; it is shared with Karger's algorithm and needs no probability.

Main definitions

• Cslib.Algorithms.Lean.StoerWagner.maOrder: a maximum adjacency ordering of Fin k.
• Cslib.Algorithms.Lean.StoerWagner.run: the phases on the supervertices of a contraction.
• Cslib.Algorithms.Lean.StoerWagner.stoerWagner: the algorithm, answering one side of a minimum cut and its weight.
• Cslib.Algorithms.Lean.StoerWagner.stoerWagnerM: the algorithm in TimeM, with a cost model.

Main results

• Cslib.Algorithms.Lean.StoerWagner.minCut_eq_min_contractMatrix, Cslib.Algorithms.Lean.StoerWagner.minCut_eq_min_minCutBetween: the phase recursion.
• Cslib.Algorithms.Lean.StoerWagner.minCut_eq_min_of_isMAOrdering: one phase.
• Cslib.Algorithms.Lean.StoerWagner.stoerWagner_spec: the algorithm answers a non-trivial cut of minimum weight, and its weight.
• Cslib.Algorithms.Lean.StoerWagner.time_stoerWagnerM_le: at most n ^ 3 + 4 n ^ 2 steps.

Cost model

stoerWagnerM charges unit cost per scanned entry of an array implementation with machine-word arithmetic on weights, as the TimeM annotations of the other algorithms here do; the charges are TimeM.tick annotations in the program, not derived from the Lean evaluation, which uses closures. For a phase on m supervertices of a graph on n vertices:

• initializing the key array costs m;
• a search step on r remaining candidates costs 2 r - 1: a scan for the largest key and an update of the other r - 1 keys, so the search costs m ^ 2;
• recording the cut of the phase costs m + n: its degree, and the vertex set of the original graph mapped to t;
• the merge costs 4 m + n + 1: adding row and column t of the weight matrix into those of s (2 m), moving row and column m - 1 into the freed slot t (2 m), relabelling the original vertices (n) and comparing two weights (1).

The final phase, on two supervertices, needs no search and costs 2 + n. One-time setup is not charged: the weight matrix is taken as given, and the initial map part = id of the n original vertices to supervertices is free. The total is at most n ^ 3 + 4 n ^ 2 (time_stoerWagnerM_le). This bound is loose. Summing the charges by hand, a phase on m ≥ 3 supervertices costs m ^ 2 + 6 m + 2 n + 1, so the charged time is n ^ 3 / 3 + O(n ^ 2); only the weaker bound is proved. On the 8-vertex example of the tests the charged time is 509, against the bound 768. This is the O(n³) array version of the algorithm; the O(n m + n² log n) bound of [SW97] uses Fibonacci heaps and is not formalized here.

Limitations

Weights are natural numbers, as in Cslib.WeightedCut; rational weights can be scaled to natural numbers, real weights are not covered. The algorithm answers one minimum cut, not all of them.

References

• M. Stoer and F. Wagner, A Simple Min-Cut Algorithm
• H. Nagamochi and T. Ibaraki, Computing Edge-Connectivity in Multigraphs and Capacitated Graphs

The algorithm

def Cslib.Algorithms.Lean.StoerWagner.maOrder {k : ℕ} (W : Fin k → Fin k → ℕ) : List (Fin k)

A maximum adjacency ordering of Fin k, by maximum adjacency search starting from vertex 0 (ties broken towards smaller vertices).

theorem Cslib.Algorithms.Lean.StoerWagner.perm_maOrder {k : ℕ} (W : Fin k → Fin k → ℕ) : (maOrder W).Perm (List.finRange k)

maOrder W lists every vertex once.

theorem Cslib.Algorithms.Lean.StoerWagner.isMAOrdering_maOrder {k : ℕ} (W : Fin k → Fin k → ℕ) : WeightedCut.IsMAOrdering W (maOrder W)

maOrder W is a maximum adjacency ordering.

structure Cslib.Algorithms.Lean.StoerWagner.CutResult (n : ℕ) : Type

The answer of the algorithm: one side of a cut, and the weight of the cut.

• side : Finset (Fin n)

  One side of the cut.

• weight : ℕ

  The weight of the cut.

def Cslib.Algorithms.Lean.StoerWagner.instDecidableEqCutResult.decEq {n✝ : ℕ} (x✝ x✝¹ : CutResult n✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Algorithms.Lean.StoerWagner.instDecidableEqCutResult {n✝ : ℕ} : DecidableEq (CutResult n✝)

def Cslib.Algorithms.Lean.StoerWagner.run {n : ℕ} (k : ℕ) : (Fin (k + 2) → Fin (k + 2) → ℕ) → (Fin n → Fin (k + 2)) → CutResult n

The phases of the algorithm on the supervertices Fin (k + 2) of the contraction part : Fin n → Fin (k + 2) of the input. A phase computes a maximum adjacency ordering, ending with s, t, and merges t into s; the answer is the cut of the phase, the original vertices mapped to t, unless the phases after the merge find a cut at most as heavy. With two supervertices left the cut of the single phase is that of supervertex 1.

def Cslib.Algorithms.Lean.StoerWagner.stoerWagner {n : ℕ} : (Fin n → Fin n → ℕ) → CutResult n

The Stoer–Wagner algorithm [SW97]: one side of a minimum cut of the multigraph W on Fin n, and its weight. With fewer than two vertices there is no non-trivial cut, and the answer is (∅, 0).

Correctness

theorem Cslib.Algorithms.Lean.StoerWagner.minCut_eq_min_contractMatrix {k : ℕ} {W : Fin (k + 3) → Fin (k + 3) → ℕ} (hW : WeightedCut.IsMultigraph W) {s t : Fin (k + 3)} (hst : s ≠ t) {X : Finset (Fin (k + 3))} (hX : s ∈ X ↔ t ∉ X) (hmin : ∀ (Y : Finset (Fin (k + 3))), (s ∈ Y ↔ t ∉ Y) → WeightedCut.cutWeight W X ≤ WeightedCut.cutWeight W Y) : WeightedCut.minCut W = min (WeightedCut.cutWeight W X) (WeightedCut.minCut (WeightedCut.contractMatrix W s t))

The phase recursion of [SW97]: if X is a minimum cut separating s and t, the global minimum cut weight is the smaller of the weight of X and the global minimum cut weight after merging t into s.

theorem Cslib.Algorithms.Lean.StoerWagner.minCut_eq_min_minCutBetween {k : ℕ} {W : Fin (k + 3) → Fin (k + 3) → ℕ} (hW : WeightedCut.IsMultigraph W) {s t : Fin (k + 3)} (hst : s ≠ t) : WeightedCut.minCut W = min (WeightedCut.minCutBetween W s t) (WeightedCut.minCut (WeightedCut.contractMatrix W s t))

The phase recursion in terms of the minimum s–t cut weight λ(s, t) (Cslib.WeightedCut.minCutBetween): for distinct s and t, the global minimum cut weight is min (λ(s, t)) (minCut (contractMatrix W s t)).

theorem Cslib.Algorithms.Lean.StoerWagner.minCut_eq_min_of_isMAOrdering {k : ℕ} {W : Fin (k + 3) → Fin (k + 3) → ℕ} (hW : WeightedCut.IsMultigraph W) {p : List (Fin (k + 3))} {s t : Fin (k + 3)} (hl : WeightedCut.IsMAOrdering W (p ++ [s, t])) : WeightedCut.minCut W = min (WeightedCut.cutWeight W {t}) (WeightedCut.minCut (WeightedCut.contractMatrix W s t))

One phase: for the last two vertices s, t of a maximum adjacency ordering, the global minimum cut weight is the smaller of the weight of the cut of the phase {t} and the global minimum cut weight after merging t into s.

theorem Cslib.Algorithms.Lean.StoerWagner.run_spec {n : ℕ} {W₀ : Fin n → Fin n → ℕ} (k : ℕ) {W : Fin (k + 2) → Fin (k + 2) → ℕ} {part : Fin n → Fin (k + 2)} : WeightedCut.IsContractionOf W₀ part W → WeightedCut.IsNonTrivialCut (run k W part).side ∧ WeightedCut.cutWeight W₀ (run k W part).side = (run k W part).weight ∧ (run k W part).weight = WeightedCut.minCut W

The phases on a contraction of W₀ answer a non-trivial cut of W₀ with its weight, and that weight is the global minimum cut weight of the contraction.

theorem Cslib.Algorithms.Lean.StoerWagner.stoerWagner_spec {n : ℕ} (hn : 2 ≤ n) {W : Fin n → Fin n → ℕ} (hW : WeightedCut.IsMultigraph W) : WeightedCut.IsNonTrivialCut (stoerWagner W).side ∧ WeightedCut.cutWeight W (stoerWagner W).side = WeightedCut.minCut W ∧ (stoerWagner W).weight = WeightedCut.minCut W

Correctness of the Stoer–Wagner algorithm [SW97]: on a multigraph with at least two vertices it answers a non-trivial cut of minimum weight, and the weight of that cut.

Cost

def Cslib.Algorithms.Lean.StoerWagner.maSearchM {V : Type u_1} [DecidableEq V] (W : V → V → ℕ) : ℕ → (V → ℕ) → List V → TimeM ℕ (List V)

Maximum adjacency search (Cslib.WeightedCut.maSearch) in TimeM: a step on r remaining candidates costs 2 r - 1, a scan for the largest key and an update of the other keys.

theorem Cslib.Algorithms.Lean.StoerWagner.ret_maSearchM {V : Type u_1} [DecidableEq V] (W : V → V → ℕ) (fuel : ℕ) (key : V → ℕ) (R : List V) : (maSearchM W fuel key R).ret = WeightedCut.maSearch W fuel key R

maSearchM computes maSearch.

theorem Cslib.Algorithms.Lean.StoerWagner.time_maSearchM_le {V : Type u_1} [DecidableEq V] (W : V → V → ℕ) (fuel : ℕ) (key : V → ℕ) (R : List V) : (maSearchM W fuel key R).time ≤ R.length ^ 2

Maximum adjacency search over r candidates costs at most r ^ 2.

def Cslib.Algorithms.Lean.StoerWagner.maOrderM {k : ℕ} (W : Fin k → Fin k → ℕ) : TimeM ℕ (List (Fin k))

maOrder in TimeM: initializing the k keys, then the search.

theorem Cslib.Algorithms.Lean.StoerWagner.ret_maOrderM {k : ℕ} (W : Fin k → Fin k → ℕ) : (maOrderM W).ret = maOrder W

maOrderM computes maOrder.

theorem Cslib.Algorithms.Lean.StoerWagner.time_maOrderM_le {k : ℕ} (W : Fin k → Fin k → ℕ) : (maOrderM W).time ≤ k ^ 2 + k

A maximum adjacency ordering of k supervertices costs at most k ^ 2 + k.

def Cslib.Algorithms.Lean.StoerWagner.runM {n : ℕ} (k : ℕ) : (Fin (k + 2) → Fin (k + 2) → ℕ) → (Fin n → Fin (k + 2)) → TimeM ℕ (CutResult n)

run in TimeM, with the charges of the cost model.

theorem Cslib.Algorithms.Lean.StoerWagner.ret_runM {n : ℕ} (k : ℕ) (W : Fin (k + 2) → Fin (k + 2) → ℕ) (part : Fin n → Fin (k + 2)) : (runM k W part).ret = run k W part

runM computes run.

theorem Cslib.Algorithms.Lean.StoerWagner.time_runM_le {n : ℕ} (k : ℕ) (W : Fin (k + 2) → Fin (k + 2) → ℕ) (part : Fin n → Fin (k + 2)) : (runM k W part).time ≤ (k + 2) ^ 3 + 2 * (k + 2) ^ 2 + 2 * n * (k + 2)

The phases on k + 2 supervertices of a contraction of a graph on n vertices cost at most (k + 2) ^ 3 + 2 (k + 2) ^ 2 + 2 n (k + 2).

def Cslib.Algorithms.Lean.StoerWagner.stoerWagnerM {n : ℕ} : (Fin n → Fin n → ℕ) → TimeM ℕ (CutResult n)

stoerWagner in TimeM, with the charges of the cost model.

theorem Cslib.Algorithms.Lean.StoerWagner.ret_stoerWagnerM {n : ℕ} (W : Fin n → Fin n → ℕ) : (stoerWagnerM W).ret = stoerWagner W

stoerWagnerM computes stoerWagner.

theorem Cslib.Algorithms.Lean.StoerWagner.time_stoerWagnerM_le {n : ℕ} (W : Fin n → Fin n → ℕ) : (stoerWagnerM W).time ≤ n ^ 3 + 4 * n ^ 2

The cost of the Stoer–Wagner algorithm: at most n ^ 3 + 4 n ^ 2 steps on n vertices in the cost model of the module docstring, which does not charge one-time setup. The bound is not tight: the leading term of the charged time is n ^ 3 / 3.