Supervertex contractions and Karger's survival bounds

Combinatorial and probabilistic core for Karger's randomized contraction algorithm [Karger1993] and the Karger–Stein recursive algorithm [KargerStein1996] on n-vertex weighted undirected multigraphs represented as symmetric zero-diagonal adjacency matrices W : Fin n → Fin n → ℕ. Multigraphs, cut weights, global minimum cuts and contractions along supervertex maps are the general notions of CslibFrontier.Foundations.Combinatorics.WeightedCut (Cslib.WeightedCut), and the swap-compacted contraction of one pair of supervertices (mergePair, embedCompact, contractMatrix, contractPart) is CslibFrontier.Foundations.Combinatorics.WeightedCut.Contraction; this module adds edge-weight-proportional sampling and the survival bounds. Nothing here refers to a machine: the word-RAM programs (CslibFrontier.Algorithms.WordRAM.Karger.Contract, CslibFrontier.Algorithms.WordRAM.KargerMinCut) store the matrix in row-major order (Cslib.Algorithms.WordRAM.Karger.flattenMatrix) and import these facts.

Source statements and notation mapping

• Cut-survival bounds (paraphrase):
  • [Karger1993], Section 2, Theorem 2.1 and Corollary 2.1 (paraphrase): contracting randomly chosen edges in an n-vertex multigraph down to 2 meta-vertices preserves any fixed global minimum cut with probability at least C(n, 2)⁻¹ = 2 / (n * (n - 1)), and repeating O(n ^ 2 log n) independent trials finds a minimum cut with high probability.
  • [KargerStein1996], Section 2, Lemma 2.1, Theorem 2.2, and Corollary 2.3, and Section 2.1, Corollary 2.4 (paraphrase): a fixed cut survives contraction if and only if no contracted edge crosses it; at k active supervertices every singleton cut has weight at least minCut W, so total doubled weight S is at least k * minCut W, a single edge-weight-proportional step crosses a fixed minimum cut with probability at most 2 / k, and contracting from n down to t supervertices preserves the cut with probability at least C(t, 2) / C(n, 2) = t * (t - 1) / (n * (n - 1)).
  • [MitzenmacherUpfal2017], Section 1.5, Theorem 1.8 (paraphrase): multiplying the conditional single-step survival bounds 1 - 2 / i = (i - 2) / i for i = n, …, 3 telescopes to 2 / (n * (n - 1)).
• Notation mapping and implementation variants:
  • C(t, 2) / C(n, 2) and C(n, 2)⁻¹ ↔ ((t * (t - 1) : ℕ) : ℝ≥0∞) / (n * (n - 1)) and 2 / (n * (n - 1)) (step_survival_prob_ge, telescope_survival_step);
  • [KargerStein1996], Section 3.1, Lemma 3.1 selects (u, v) with probability 2 * W u v / S via two Random-Select draws (u proportional to D(u) then v proportional to W(u, v)); our edgeOffset / IsSampledPair formalizes an equivalent single-draw variant using one uniform draw r ∈ Fin S (S = totalDoubledWeight W = ∑ u, rowDeg W u) resolved by prefix sums over rowDeg then row weights W u v, achieving the same 2 * W u v / S distribution;
  • [KargerStein1996], Section 3.2 (Figure 5) updates the n × n matrix in O(n) time per contraction (hence Corollary 3.2's O(n ^ 2) total); our embedCompact / contractMatrix swap-compacts active slot k - 1 into the removed slot v so each contraction on k active supervertices scans only 0..k - 1 (O(k) time);
  • highProbTrials n = (n * (n - 1) / 2) * (Nat.log 2 n + 2) and the elementary Real.exp-free Bernoulli bound highProb_failure_le (≤ 1 / (2 * n)) are our own concrete parameter choices instantiating the O(n ^ 2 log n) repeated-trial amplification of [Karger1993], Section 2, Corollary 2.1.

Main definitions

• Cslib.Algorithms.Karger.edgeOffset, Cslib.Algorithms.Karger.IsSampledPair: prefix-sum interval characterization of edge-weight-proportional sampling from Fin S.

Main results

• Cslib.Algorithms.Karger.surviving_card_eq, Cslib.Algorithms.Karger.step_survival_prob_ge: a fixed minimum cut survives one edge-proportional contraction on k supervertices with probability at least (k - 2) / k.
• Cslib.Algorithms.Karger.telescope_survival_step: telescoping multiplication identity ((m - 1) / (m + 1)) * (t * (t - 1) / (m * (m - 1))) = t * (t - 1) / ((m + 1) * m) in ℝ≥0∞.
• Cslib.Algorithms.Karger.highProb_failure_le: elementary Bernoulli amplification bound (1 - 2 / (n * (n - 1))) ^ ((n * (n - 1) / 2) * (Nat.log 2 n + 2)) ≤ 1 / (2 * n).

References

• D. R. Karger, Global Min-cuts in RNC, and Other Ramifications of a Simple Min-Cut Algorithm
• D. R. Karger and C. Stein, A New Approach to the Minimum Cut Problem
• M. Mitzenmacher and E. Upfal, Probability and Computing

Prefix-sum edge-proportional sampling on Fin S

def Cslib.Algorithms.Karger.degBefore {k : ℕ} (W : Fin k → Fin k → ℕ) (u : Fin k) : ℕ

Sum of rowDeg W a over all a < u.

def Cslib.Algorithms.Karger.weightBefore {k : ℕ} (W : Fin k → Fin k → ℕ) (u v : Fin k) : ℕ

Sum of W u b over all b < v.

def Cslib.Algorithms.Karger.edgeOffset {k : ℕ} (W : Fin k → Fin k → ℕ) (u v : Fin k) : ℕ

Flattened prefix-sum start offset of directed edge slot (u, v) inside [0, S).

theorem Cslib.Algorithms.Karger.weightBefore_add_le_rowDeg {k : ℕ} (W : Fin k → Fin k → ℕ) (u v : Fin k) : weightBefore W u v + W u v ≤ WeightedCut.rowDeg W u

theorem Cslib.Algorithms.Karger.weightBefore_le_of_lt {k : ℕ} (W : Fin k → Fin k → ℕ) (u : Fin k) {v₁ v₂ : Fin k} (hlt : v₁ < v₂) : weightBefore W u v₁ + W u v₁ ≤ weightBefore W u v₂

theorem Cslib.Algorithms.Karger.degBefore_add_le_totalDoubledWeight {k : ℕ} (W : Fin k → Fin k → ℕ) (u : Fin k) : degBefore W u + WeightedCut.rowDeg W u ≤ WeightedCut.totalDoubledWeight W

theorem Cslib.Algorithms.Karger.degBefore_le_of_lt {k : ℕ} (W : Fin k → Fin k → ℕ) {u₁ u₂ : Fin k} (hlt : u₁ < u₂) : degBefore W u₁ + WeightedCut.rowDeg W u₁ ≤ degBefore W u₂

theorem Cslib.Algorithms.Karger.edgeOffset_add_le_totalDoubledWeight {k : ℕ} (W : Fin k → Fin k → ℕ) (u v : Fin k) : edgeOffset W u v + W u v ≤ WeightedCut.totalDoubledWeight W

def Cslib.Algorithms.Karger.IsSampledPair {k : ℕ} (W : Fin k → Fin k → ℕ) (r : ℕ) (u v : Fin k) : Prop

IsSampledPair W r u v holds when sample r falls inside the half-open interval [edgeOffset W u v, edgeOffset W u v + W u v).

@[instance_reducible]

instance Cslib.Algorithms.Karger.instDecidableIsSampledPair {k : ℕ} (W : Fin k → Fin k → ℕ) (r : ℕ) (u v : Fin k) : Decidable (IsSampledPair W r u v)

theorem Cslib.Algorithms.Karger.isSampledPair_ne {k : ℕ} {W : Fin k → Fin k → ℕ} (hW : WeightedCut.IsMultigraph W) {r : ℕ} {u v : Fin k} (h : IsSampledPair W r u v) : u ≠ v

theorem Cslib.Algorithms.Karger.isSampledPair_unique {k : ℕ} (W : Fin k → Fin k → ℕ) {r : ℕ} {u₁ v₁ u₂ v₂ : Fin k} (h₁ : IsSampledPair W r u₁ v₁) (h₂ : IsSampledPair W r u₂ v₂) : u₁ = u₂ ∧ v₁ = v₂

theorem Cslib.Algorithms.Karger.exists_isSampledPair {k : ℕ} (W : Fin k → Fin k → ℕ) {r : ℕ} (hr : r < WeightedCut.totalDoubledWeight W) : ∃ (u : Fin k) (v : Fin k), IsSampledPair W r u v

theorem Cslib.Algorithms.Karger.card_sampledPair_fiber {k : ℕ} (W : Fin k → Fin k → ℕ) (u v : Fin k) : {r : Fin (WeightedCut.totalDoubledWeight W) | IsSampledPair W (↑r) u v}.card = W u v

def Cslib.Algorithms.Karger.SampleSurvives {k : ℕ} (W : Fin k → Fin k → ℕ) (B : Finset (Fin k)) (r : Fin (WeightedCut.totalDoubledWeight W)) : Prop

Event on Fin (totalDoubledWeight W) where the edge sampled at r keeps both endpoints on the same side of B.

@[instance_reducible]

instance Cslib.Algorithms.Karger.instDecidableSampleSurvives {k : ℕ} (W : Fin k → Fin k → ℕ) (B : Finset (Fin k)) (r : Fin (WeightedCut.totalDoubledWeight W)) : Decidable (SampleSurvives W B r)

theorem Cslib.Algorithms.Karger.not_sampleSurvives_iff_crosses {k : ℕ} (W : Fin k → Fin k → ℕ) (B : Finset (Fin k)) (r : Fin (WeightedCut.totalDoubledWeight W)) : ¬SampleSurvives W B r ↔ ∃ (u : Fin k) (v : Fin k), IsSampledPair W (↑r) u v ∧ ¬(u ∈ B ↔ v ∈ B)

theorem Cslib.Algorithms.Karger.crossing_card_eq {k : ℕ} {W : Fin k → Fin k → ℕ} (hW : WeightedCut.IsMultigraph W) (B : Finset (Fin k)) : {r : Fin (WeightedCut.totalDoubledWeight W) | ¬SampleSurvives W B r}.card = 2 * WeightedCut.cutWeight W B

theorem Cslib.Algorithms.Karger.surviving_card_eq {k : ℕ} {W : Fin k → Fin k → ℕ} (hW : WeightedCut.IsMultigraph W) (B : Finset (Fin k)) : {r : Fin (WeightedCut.totalDoubledWeight W) | SampleSurvives W B r}.card = WeightedCut.totalDoubledWeight W - 2 * WeightedCut.cutWeight W B

theorem Cslib.Algorithms.Karger.step_survival_prob_ge {k : ℕ} (hk : 2 ≤ k) {W : Fin k → Fin k → ℕ} (hW : WeightedCut.IsMultigraph W) {B : Finset (Fin k)} (hS : 0 < WeightedCut.totalDoubledWeight W) (hdeg : k * WeightedCut.cutWeight W B ≤ WeightedCut.totalDoubledWeight W) : ↑(k - 2) / ↑k ≤ (Probability.PMF.uniformOfFintype (Fin (WeightedCut.totalDoubledWeight W))).toOuterMeasure {r : Fin (WeightedCut.totalDoubledWeight W) | SampleSurvives W B r}

One-step survival probability lower bound: if k ≥ 2, 0 < totalDoubledWeight W, and k * cutWeight W B ≤ totalDoubledWeight W, then a uniform sample r : Fin (totalDoubledWeight W) satisfies SampleSurvives W B r with probability at least (k - 2) / k.

Telescoping and Bernoulli amplification

theorem Cslib.Algorithms.Karger.ennreal_div_pow (a b : ENNReal) (m : ℕ) : (a / b) ^ m = a ^ m / b ^ m

Power of a quotient in ℝ≥0∞: (a / b) ^ m = a ^ m / b ^ m.

theorem Cslib.Algorithms.Karger.telescope_survival_step {t m : ℕ} (ht : 2 ≤ t) (htm : t ≤ m) : ↑(m - 1) / ↑(m + 1) * (↑(t * (t - 1)) / ↑(m * (m - 1))) = ↑(t * (t - 1)) / ↑((m + 1) * m)

Telescoping cancellation step for contractDownTo survival probability from m + 1 down to t (2 ≤ t ≤ m): ((m - 1) / (m + 1)) * (t * (t - 1) / (m * (m - 1))) = t * (t - 1) / ((m + 1) * m).

theorem Cslib.Algorithms.Karger.one_sub_two_div_pairs_eq {n : ℕ} (hn : 2 ≤ n) : 1 - 2 / ↑(n * (n - 1)) = ↑(n * (n - 1) / 2 - 1) / ↑(n * (n - 1) / 2)

theorem Cslib.Algorithms.Karger.one_sub_two_div_pow_pairs_le_half {n : ℕ} (hn : 2 ≤ n) : (1 - 2 / ↑(n * (n - 1))) ^ (n * (n - 1) / 2) ≤ 1 / 2

def Cslib.Algorithms.Karger.highProbTrials (n : ℕ) : ℕ

Elementary high-probability trial count (n * (n - 1) / 2) * (Nat.log 2 n + 2) for Basic Karger amplification.

theorem Cslib.Algorithms.Karger.highProbTrials_pos {n : ℕ} (hn : 2 ≤ n) : 1 ≤ highProbTrials n

theorem Cslib.Algorithms.Karger.highProb_failure_le {n : ℕ} (hn : 2 ≤ n) : (1 - 2 / ↑(n * (n - 1))) ^ highProbTrials n ≤ 1 / ↑(2 * n)

Elementary failure probability bound for highProbTrials n independent contractions: (1 - 2 / (n * (n - 1))) ^ ((n * (n - 1) / 2) * (Nat.log 2 n + 2)) ≤ 1 / (2 * n).

theorem Cslib.Algorithms.Karger.highProb_failure_le_inv_n {n : ℕ} (hn : 2 ≤ n) : (1 - 2 / ↑(n * (n - 1))) ^ highProbTrials n ≤ 1 / ↑n