Karger's algorithm

StructureMultigraph state of Karger's algorithm#✓fully proved

A state over a vertex type \(V\) consists of a list of current (super-)vertices in \(V\) and a list of edges, each an ordered pair of elements of \(V\); repeated pairs are parallel edges.

structure State (V : Type u) where
  /-- The current vertices. -/
  verts : List V
  /-- The edges, with multiplicity. -/
  edges : List (V × V)

Used by 21

Used byMinimum cut size bounds the number of edges · Edge contraction · Cut sizes under contraction · Cuts of a multigraph · Minimum cut size · Contraction preserves the minimum cut size · Success probability of repeated runs · Amplification with high probability · Repeating Karger's algorithm succeeds with probability at least one half · Karger's algorithm succeeds with high probability · Success probability of the contraction process · Karger's bound · The success probability is at most one · The success probability is nonnegative · Handshake lemma · Survival probabilities of distinct cuts sum to at most one · Probability that a run outputs a given cut · Each minimum cut survives with probability at least \(2/(n(n-1))\) · At most \(n(n-1)/2\) minimum cuts · Valid multigraph · Contraction preserves validity and removes one vertex

DefinitionValid multigraph#✓fully proved

A multigraph, given by a list of vertices and a list of edges (pairs of vertices, with multiplicity), is valid when its vertex list has no repeated entries and every edge joins two distinct vertices of the list.

def State.Valid (st : State V) : Prop :=
  st.verts.Nodup ∧ ∀ e ∈ st.edges, e.1 ∈ st.verts ∧ e.2 ∈ st.verts ∧ e.1 ≠ e.2

Uses 1 · Used by 11

Statement usesMultigraph state of Karger's algorithm

Used byMinimum cut size bounds the number of edges · Contraction preserves the minimum cut size · Amplification with high probability · Repeating Karger's algorithm succeeds with probability at least one half · Karger's algorithm succeeds with high probability · Karger's bound · Handshake lemma · Survival probabilities of distinct cuts sum to at most one · Each minimum cut survives with probability at least \(2/(n(n-1))\) · At most \(n(n-1)/2\) minimum cuts · Contraction preserves validity and removes one vertex

DefinitionSize of a cut#✓fully proved

For a list of edges (pairs of vertices, repeated pairs counted with multiplicity) and a map \(X\) from vertices to booleans, the size of the cut \(X\) is the number of edges \((u, v)\) in the list with \(X(u) \ne X(v)\).

def cutSize (edges : List (V × V)) (X : V → Bool) : ℕ :=
  (edges.filter fun e => X e.1 != X e.2).length

Used by 8

Used byMinimum cut size bounds the number of edges · Cut sizes under contraction · Minimum cut size · Contraction preserves the minimum cut size · Karger's bound · Handshake lemma · Each minimum cut survives with probability at least \(2/(n(n-1))\) · At most \(n(n-1)/2\) minimum cuts

DefinitionCuts of a multigraph#✓fully proved

A map \(X\) from vertices to booleans is a cut of a multigraph state \(G\) when some vertex \(v\) of \(G\) has \(X(v) = \mathrm{true}\) and some vertex \(w\) of \(G\) has \(X(w) = \mathrm{false}\).

def IsCut (st : State V) (X : V → Bool) : Prop :=
  (∃ v ∈ st.verts, X v = true) ∧ ∃ v ∈ st.verts, X v = false

Uses 1 · Used by 8

Statement usesMultigraph state of Karger's algorithm

Used byMinimum cut size bounds the number of edges · Minimum cut size · Contraction preserves the minimum cut size · Karger's bound · Survival probabilities of distinct cuts sum to at most one · Probability that a run outputs a given cut · Each minimum cut survives with probability at least \(2/(n(n-1))\) · At most \(n(n-1)/2\) minimum cuts

DefinitionMinimum cut size#✓fully proved

A natural number \(k\) is the minimum cut size of a multigraph state \(G\) when some cut of \(G\) has size \(k\) and every cut of \(G\) has size at least \(k\).

def IsMinCut (st : State V) (k : ℕ) : Prop :=
  (∃ X, IsCut st X ∧ cutSize st.edges X = k) ∧ ∀ X, IsCut st X → k ≤ cutSize st.edges X

Uses 3 · Used by 8

Statement usesCuts of a multigraph · Multigraph state of Karger's algorithm · Size of a cut

Used byMinimum cut size bounds the number of edges · Contraction preserves the minimum cut size · Amplification with high probability · Repeating Karger's algorithm succeeds with probability at least one half · Karger's algorithm succeeds with high probability · Karger's bound · Each minimum cut survives with probability at least \(2/(n(n-1))\) · At most \(n(n-1)/2\) minimum cuts

DefinitionRenaming a vertex#✓fully proved

For vertices \(a\) and \(b\), renaming \(b\) to \(a\) is the map on vertices that sends \(b\) to \(a\) and fixes every other vertex.

def rename (b a v : V) : V := if v = b then a else v

Used by 6

Used byEdge contraction · Cut sizes under contraction · Contraction preserves the minimum cut size · Survival probabilities of distinct cuts sum to at most one · Each minimum cut survives with probability at least \(2/(n(n-1))\) · Contraction preserves validity and removes one vertex

DefinitionEdge contraction#✓fully proved

For a multigraph state \(G\) and a pair of vertices \(e = (a, b)\), the contraction of \(G\) along \(e\) deletes the first occurrence of \(b\) from the vertex list, replaces \(b\) by \(a\) in both endpoints of every edge, and then deletes every edge whose two endpoints are equal.

def contract (st : State V) (e : V × V) : State V where
  verts := st.verts.erase e.2
  edges := (st.edges.map fun x => (rename e.2 e.1 x.1, rename e.2 e.1 x.2)).filter
    fun x => x.1 ≠ x.2

Uses 2 · Used by 10

Statement usesMultigraph state of Karger's algorithm · Renaming a vertex

Used byCut sizes under contraction · Contraction preserves the minimum cut size · Success probability of the contraction process · Karger's bound · The success probability is at most one · The success probability is nonnegative · Survival probabilities of distinct cuts sum to at most one · Probability that a run outputs a given cut · Each minimum cut survives with probability at least \(2/(n(n-1))\) · Contraction preserves validity and removes one vertex

DefinitionSuccess probability of the contraction process#✓fully proved

For a natural number \(k\), a number \(f\) of allowed contractions and a multigraph \(G\) with edge list \(E_G\), the probability \(P_k(f, G)\) that the contraction process on \(G\) returns \(k\) is defined by recursion on \(f\). If \(f = 0\), or \(G\) has at most two vertices, or \(G\) has no edges, then \(P_k(f, G)\) is \(1\) when \(G\) has exactly \(k\) edges and \(0\) otherwise. Otherwise \(P_k(f, G) = \frac{1}{|E_G|} \sum_{e \in E_G} P_k(f - 1, G/e)\), where \(G/e\) is the contraction of \(G\) along \(e\) and the sum runs over the edges with multiplicity.

This models contracting a uniformly random edge while more than two vertices remain and counting the edges between the last two vertices.

def successProb (k : ℕ) : ℕ → State V → ℚ
  | 0, st => if st.edges.length = k then 1 else 0
  | fuel + 1, st =>
      if st.verts.length ≤ 2 ∨ st.edges = [] then (if st.edges.length = k then 1 else 0)
      else (st.edges.map fun e => successProb k fuel (contract st e)).sum / st.edges.length

Uses 2 · Used by 6

Statement usesMultigraph state of Karger's algorithm · Edge contraction

Used bySuccess probability of repeated runs · Amplification with high probability · Repeating Karger's algorithm succeeds with probability at least one half · Karger's bound · The success probability is at most one · The success probability is nonnegative

25 fully proved

Contraction and cuts

TheoremCut sizes under contraction#✓fully proved

Let \(G\) be a multigraph state, \(e = (a, b)\) a pair of vertices and \(Y\) a map from vertices to booleans, and let \(\rho\) send \(b\) to \(a\) and fix every other vertex. The size of the cut \(Y\) in the contraction of \(G\) along \(e\) equals the size of the cut \(Y \circ \rho\) in \(G\).

theorem cutSize_contract (st : State V) (e : V × V) (Y : V → Bool) :
    cutSize (contract st e).edges Y = cutSize st.edges fun v => Y (rename e.2 e.1 v)

Uses 4 · Used by 2

Statement usesMultigraph state of Karger's algorithm · Edge contraction · Size of a cut · Renaming a vertex

Used byContraction preserves the minimum cut size · Each minimum cut survives with probability at least \(2/(n(n-1))\)

TheoremContraction preserves the minimum cut size#✓fully proved

Let \(G\) be a valid multigraph state with minimum cut size \(k\), and let \(X\) be a cut of \(G\) of size \(k\). If \(e = (a, b)\) is an edge of \(G\) with \(X(a) = X(b)\), then the contraction of \(G\) along \(e\) also has minimum cut size \(k\).

theorem isMinCut_contract {st : State V} (hv : st.Valid) {k : ℕ} (hmin : IsMinCut st k)
    {X : V → Bool} (hX : IsCut st X) (hk : cutSize st.edges X = k) {e : V × V}
    (he : e ∈ st.edges) (hsame : X e.1 = X e.2) : IsMinCut (contract st e) k

Uses 8 · Used by 2

Statement usesCuts of a multigraph · Minimum cut size · Multigraph state of Karger's algorithm · Valid multigraph · Edge contraction · Size of a cut

Proof usesCut sizes under contraction · Renaming a vertex

Used byKarger's bound · Each minimum cut survives with probability at least \(2/(n(n-1))\)

TheoremContraction preserves validity and removes one vertex#✓fully proved

If a multigraph \(G\) is valid and \(e\) is one of its edges, then the contraction of \(G\) along \(e\) is valid and has exactly one vertex fewer than \(G\).

theorem valid_contract {st : State V} (hv : st.Valid) {e : V × V} (he : e ∈ st.edges) :
    (contract st e).Valid ∧ (contract st e).verts.length = st.verts.length - 1

Uses 4 · Used by 3

Statement usesMultigraph state of Karger's algorithm · Valid multigraph · Edge contraction

Proof usesRenaming a vertex

Used byKarger's bound · Survival probabilities of distinct cuts sum to at most one · Each minimum cut survives with probability at least \(2/(n(n-1))\)

Degrees

TheoremHandshake lemma#✓fully proved

For a valid multigraph \(G\), the sum over the vertices \(v\) of \(G\) of the number of edges crossing the singleton cut \(\{v\}\) equals twice the number of edges of \(G\).

theorem sum_degree (st : State V) (hv : st.Valid) :
    (st.verts.map fun v => cutSize st.edges fun x => decide (x = v)).sum =
      2 * st.edges.length

Uses 3 · Used by 1

Statement usesMultigraph state of Karger's algorithm · Valid multigraph · Size of a cut

Used byMinimum cut size bounds the number of edges

TheoremMinimum cut size bounds the number of edges#✓fully proved

Let \(G\) be a valid multigraph state with \(n \ge 2\) vertices, \(m\) edges (counted with multiplicity) and minimum cut size \(k\). Then \(n k \le 2m\): every vertex has degree at least \(k\), since its singleton is a cut.

theorem card_mul_le_two_mul_edges {st : State V} (hv : st.Valid) {k : ℕ} (hmin : IsMinCut st k)
    (hn : 2 ≤ st.verts.length) : st.verts.length * k ≤ 2 * st.edges.length

Uses 6 · Used by 2

Statement usesMinimum cut size · Multigraph state of Karger's algorithm · Valid multigraph

Proof usesCuts of a multigraph · Size of a cut · Handshake lemma

Used byKarger's bound · Each minimum cut survives with probability at least \(2/(n(n-1))\)

The success probability

TheoremThe success probability is nonnegative#✓fully proved

For every natural number \(k\), every number \(f\) of allowed contractions and every multigraph state \(G\), the probability \(P_k(f, G)\) that the contraction process on \(G\) returns \(k\) satisfies \(0 \le P_k(f, G)\).

theorem successProb_nonneg (k : ℕ) : ∀ (fuel : ℕ) (st : State V), 0 ≤ successProb k fuel st

Uses 3 · Used by 3

Statement usesMultigraph state of Karger's algorithm · Success probability of the contraction process

Proof usesEdge contraction

Used byAmplification with high probability · Repeating Karger's algorithm succeeds with probability at least one half · Karger's bound

TheoremThe success probability is at most one#✓fully proved

For every natural number \(k\), every number of allowed contractions and every multigraph \(G\), the probability that the contraction process on \(G\) returns \(k\) is at most \(1\).

theorem successProb_le_one (k : ℕ) : ∀ (fuel : ℕ) (st : State V), successProb k fuel st ≤ 1

Uses 3 · Used by 2

Statement usesMultigraph state of Karger's algorithm · Success probability of the contraction process

Proof usesEdge contraction

Used byAmplification with high probability · Repeating Karger's algorithm succeeds with probability at least one half

TheoremKarger's bound#✓fully proved

Let \(G\) be a valid multigraph with \(n \ge 2\) vertices and minimum cut size \(k\). Then the contraction process on \(G\), with \(n\) contractions allowed, returns \(k\) with probability at least \(2 / (n(n-1))\).

theorem successProb_ge (st : State V) (hv : st.Valid) {k : ℕ} (hmin : IsMinCut st k)
    (hn : 2 ≤ st.verts.length) :
    2 / ((st.verts.length : ℚ) * (st.verts.length - 1)) ≤
      successProb k st.verts.length st

Uses 11 · Used by 2

Statement usesMinimum cut size · Multigraph state of Karger's algorithm · Valid multigraph · Success probability of the contraction process

Proof usesCuts of a multigraph · Minimum cut size bounds the number of edges · Edge contraction · Size of a cut · Contraction preserves the minimum cut size · The success probability is nonnegative · Contraction preserves validity and removes one vertex

Used byAmplification with high probability · Repeating Karger's algorithm succeeds with probability at least one half

Amplification

DefinitionSuccess probability of repeated runs#✓fully proved

For a multigraph \(G\) with \(n\) vertices and natural numbers \(k\) and \(t\), let \(p\) be the probability that one run of the contraction process on \(G\), with \(n\) contractions allowed, returns \(k\). The repeated success probability is \(1 - (1 - p)^t\), the probability that at least one of \(t\) independent runs returns \(k\).

def repeatSuccessProb (k t : ℕ) (st : State V) : ℚ :=
  1 - (1 - successProb k st.verts.length st) ^ t

Uses 2 · Used by 3

Statement usesMultigraph state of Karger's algorithm · Success probability of the contraction process

Used byAmplification with high probability · Repeating Karger's algorithm succeeds with probability at least one half · Karger's algorithm succeeds with high probability

TheoremRepeating Karger's algorithm succeeds with probability at least one half#✓fully proved

Let \(G\) be a valid multigraph state with \(n \ge 2\) vertices and minimum cut size \(k\), and let \(t\) be a natural number with \(n(n-1) \le 2t\). Then the probability that at least one of \(t\) independent runs of the contraction process returns \(k\) is at least \(1/2\).

theorem repeatSuccessProb_ge_half (st : State V) (hv : st.Valid) {k : ℕ} (hmin : IsMinCut st k)
    (hn : 2 ≤ st.verts.length) {t : ℕ} (ht : st.verts.length * (st.verts.length - 1) ≤ 2 * t) :
    1 / 2 ≤ repeatSuccessProb k t st

Uses 8

Statement usesMinimum cut size · Multigraph state of Karger's algorithm · Valid multigraph · Success probability of repeated runs

Proof usesSuccess probability of the contraction process · Karger's bound · The success probability is at most one · The success probability is nonnegative

TheoremAmplification with high probability#✓fully proved

Let \(G\) be a valid multigraph with \(n \ge 2\) vertices and minimum cut size \(k\), and let \(c\) and \(t\) be natural numbers with \(c \cdot n(n-1) \le 2t\). Then the probability that at least one of \(t\) independent runs of the contraction process on \(G\) returns \(k\) is at least \(1 - (1/2)^c\).

theorem repeatSuccessProb_ge (st : State V) (hv : st.Valid) {k : ℕ} (hmin : IsMinCut st k)
    (hn : 2 ≤ st.verts.length) {c t : ℕ}
    (ht : c * (st.verts.length * (st.verts.length - 1)) ≤ 2 * t) :
    1 - (1 / 2 : ℚ) ^ c ≤ repeatSuccessProb k t st

Uses 8 · Used by 1

Statement usesMinimum cut size · Multigraph state of Karger's algorithm · Valid multigraph · Success probability of repeated runs

Proof usesSuccess probability of the contraction process · Karger's bound · The success probability is at most one · The success probability is nonnegative

Used byKarger's algorithm succeeds with high probability

TheoremKarger's algorithm succeeds with high probability#✓fully proved

Let \(G\) be a valid multigraph with \(n \ge 2\) vertices and minimum cut size \(k\), and let \(t\) be a natural number with \(\lceil \log_2 n \rceil \cdot n(n-1) \le 2t\). Then the probability that at least one of \(t\) independent runs of the contraction process on \(G\) returns \(k\) is at least \(1 - 1/n\).

Thus \(O(n^2 \log n)\) runs find the minimum cut size with high probability.

theorem repeatSuccessProb_ge_one_sub_inv (st : State V) (hv : st.Valid) {k : ℕ}
    (hmin : IsMinCut st k) (hn : 2 ≤ st.verts.length) {t : ℕ}
    (ht : Nat.clog 2 st.verts.length * (st.verts.length * (st.verts.length - 1)) ≤ 2 * t) :
    1 - 1 / (st.verts.length : ℚ) ≤ repeatSuccessProb k t st

Uses 5

Statement usesMinimum cut size · Multigraph state of Karger's algorithm · Valid multigraph · Success probability of repeated runs

Proof usesAmplification with high probability

Counting minimum cuts

DefinitionProbability that a run outputs a given cut#✓fully proved

For a map \(X\) from vertices to booleans, a fuel bound \(f\) and a multigraph \(G\), this is the probability that the contraction process on \(G\) (contract an edge chosen uniformly at random, counted with multiplicity, while more than two vertices and at least one edge remain, making at most \(f\) contractions) never contracts an edge whose endpoints \(X\) separates and ends with exactly two vertices on which \(X\) takes both values.

Explicitly: if \(f = 0\), or \(G\) has at most two vertices, or \(G\) has no edges, the value is \(1\) when \(G\) has exactly two vertices and \(X\) is a cut of \(G\), and \(0\) otherwise. Otherwise it is the average over the edges \(e\) of \(G\), counted with multiplicity, of the value for fuel \(f - 1\) on the contraction of \(G\) along \(e\) when \(X\) agrees on the two endpoints of \(e\), and of \(0\) when it does not.

def surviveProb (X : V → Bool) : ℕ → State V → ℚ
  | 0, st => if st.verts.length = 2 ∧ IsCut st X then 1 else 0
  | fuel + 1, st =>
      if st.verts.length ≤ 2 ∨ st.edges = [] then
        (if st.verts.length = 2 ∧ IsCut st X then 1 else 0)
      else
        (st.edges.map fun e =>
            if X e.1 = X e.2 then surviveProb X fuel (contract st e) else 0).sum /
          st.edges.length

Uses 3 · Used by 3

Statement usesCuts of a multigraph · Multigraph state of Karger's algorithm · Edge contraction

Used bySurvival probabilities of distinct cuts sum to at most one · Each minimum cut survives with probability at least \(2/(n(n-1))\) · At most \(n(n-1)/2\) minimum cuts

DefinitionCuts distinct as partitions#✓fully proved

Two maps \(X, Y\) from vertices to booleans are distinct on a list of vertices \(S\) when some \(v \in S\) has \(X(v) \ne Y(v)\) and some \(w \in S\) has \(X(w) = Y(w)\); so on \(S\) neither cut is the other or its complement.

def DistinctOn (S : List V) (X Y : V → Bool) : Prop :=
  (∃ v ∈ S, X v ≠ Y v) ∧ ∃ v ∈ S, X v = Y v

Used by 2

Used bySurvival probabilities of distinct cuts sum to at most one · At most \(n(n-1)/2\) minimum cuts

TheoremEach minimum cut survives with probability at least \(2/(n(n-1))\)#✓fully proved

Let \(G\) be a valid multigraph with \(n \ge 2\) vertices whose minimum cut size \(k\) is at least \(1\), and let \(X\) be a cut of \(G\) with exactly \(k\) crossing edges. Then the probability that the contraction process on \(G\), allowed up to \(n\) contractions, outputs the cut \(X\) is at least \(2/(n(n-1))\).

theorem surviveProb_ge (st : State V) (hv : st.Valid) {k : ℕ} (hmin : IsMinCut st k)
    (hk1 : 1 ≤ k) {X : V → Bool} (hX : IsCut st X) (hk : cutSize st.edges X = k)
    (hn : 2 ≤ st.verts.length) :
    2 / ((st.verts.length : ℚ) * (st.verts.length - 1)) ≤
      surviveProb X st.verts.length st

Uses 12 · Used by 1

Statement usesCuts of a multigraph · Minimum cut size · Multigraph state of Karger's algorithm · Valid multigraph · Size of a cut · Probability that a run outputs a given cut

Proof usesMinimum cut size bounds the number of edges · Edge contraction · Cut sizes under contraction · Contraction preserves the minimum cut size · Renaming a vertex · Contraction preserves validity and removes one vertex

Used byAt most \(n(n-1)/2\) minimum cuts

TheoremSurvival probabilities of distinct cuts sum to at most one#✓fully proved

Let \(G\) be a valid multigraph with vertex list \(S\), let \(f\) be a number of allowed contractions, and let \(X_1, \dots, X_m\) be Boolean functions on the vertex type that are pairwise distinct as partitions of \(S\). Then the probabilities that the contraction process on \(G\), with \(f\) contractions allowed, outputs \(X_1, \dots, X_m\) add up to at most \(1\).

The survival events are disjoint: a run outputs at most one partition.

theorem sum_surviveProb_le_one : ∀ (fuel : ℕ) (st : State V) (F : List (V → Bool)),
    st.Valid → F.Pairwise (DistinctOn st.verts) →
      (F.map fun X => surviveProb X fuel st).sum ≤ 1

Uses 8 · Used by 1

Statement usesCuts distinct as partitions · Multigraph state of Karger's algorithm · Valid multigraph · Probability that a run outputs a given cut

Proof usesCuts of a multigraph · Edge contraction · Renaming a vertex · Contraction preserves validity and removes one vertex

Used byAt most \(n(n-1)/2\) minimum cuts

TheoremAt most \(n(n-1)/2\) minimum cuts#✓fully proved

At most \(n(n-1)/2\) minimum cuts (Karger; Kleinberg and Tardos, Section 13.2). Let \(G\) be a valid multigraph with \(n \ge 2\) vertices whose minimum cut size \(k\) is at least \(1\). If \(X_1, \dots, X_m\) are cuts of \(G\), each with exactly \(k\) crossing edges, that are pairwise distinct as partitions of the vertices of \(G\), then \(2m \le n(n-1)\), that is, \(m \le n(n-1)/2\).

Each of these cuts is output by a run of the contraction process with probability at least \(2/(n(n-1))\), and the runs that output distinct partitions are disjoint.

theorem two_mul_length_minCuts_le (st : State V) (hv : st.Valid) {k : ℕ} (hmin : IsMinCut st k)
    (hk1 : 1 ≤ k) (hn : 2 ≤ st.verts.length) (F : List (V → Bool))
    (hF : ∀ X ∈ F, IsCut st X ∧ cutSize st.edges X = k) (hd : F.Pairwise (DistinctOn st.verts)) :
    2 * F.length ≤ st.verts.length * (st.verts.length - 1)

Uses 9

Statement usesCuts distinct as partitions · Cuts of a multigraph · Minimum cut size · Multigraph state of Karger's algorithm · Valid multigraph · Size of a cut

Proof usesSurvival probabilities of distinct cuts sum to at most one · Probability that a run outputs a given cut · Each minimum cut survives with probability at least \(2/(n(n-1))\)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.