129 Graph Theory — Karger Min Cut
129.1 Overview
This file develops a multigraph model (a Multiset of unordered pairs, since Mathlib’s SimpleGraph has no parallel edges) together with edge contraction, cuts and their sizes, and the structural lemmas behind Karger’s randomized contraction algorithm: contraction of a non-crossing edge preserves a minimum cut, every vertex degree bounds the min-cut size, the handshake lemma \(\sum _v \deg (v) = 2\left\lvert E\right\rvert \), the telescoping survival product \(2/(n(n-1))\), and the standard corollaries on repetition and on the number of (approximate) minimum cuts.
129.2 Declarations
A multigraph on a vertex type \(\alpha \) consists of a finite vertex set together with a multiset of unordered pairs (elements of \(\mathrm{Sym}_2\, \alpha \)) as edges, subject to two conditions: every endpoint of every edge is a live vertex, and no edge is a self-loop (edges are loopless, since loops are deleted after each contraction).
The number of edges of \(G\) counted with multiplicity, i.e. the cardinality of the edge multiset.
The number of vertices of \(G\), i.e. the cardinality of its vertex Finset.
Given an edge \(e \in E(G)\) with endpoints \(u\) and \(v\), the contracted multigraph \(G/e\) is obtained by replacing every occurrence of \(v\) by \(u\) in all edges, deleting the resulting self-loops (in particular all parallel copies of \(e\)), and removing \(v\) from the vertex set. Parallel edges between the merged vertex and the rest of the graph are retained with multiplicity.
Let \(G\) be a multigraph and let \(e\) be an edge of \(G\) that is not a self-loop, so that its two endpoints are distinct. Writing \(G/e\) for the multigraph obtained by contracting \(e\), its vertex count satisfies
where the subtraction is truncated at \(0\).
Let \(G\) be a multigraph and let \(e \in E(G)\) be one of its edges. Then the multigraph \(G/e\) obtained by contracting \(e\) satisfies
where both edge counts are taken with multiplicity; in particular, contracting an edge never increases the number of edges and eliminates at least the contracted edge itself.
A cut of \(G\) is a subset \(S \subseteq V(G)\) that is nonempty and whose complement \(V(G) \setminus S\) inside \(V(G)\) is also nonempty; the two nonemptiness conditions rule out the trivial partitions.
The multiset of edges of \(G\) that cross the cut \(C\), i.e. those edges having exactly one endpoint in \(S\), counted with multiplicity. It is obtained by filtering the edge multiset by the condition that exactly one of the two representative endpoints lies in \(S\).
For a finite set \(S\) and an unordered pair \(e\), the predicate \(\texttt{Crosses}\; S\; e\) holds when some element of \(e\) lies in \(S\) and some element of \(e\) lies outside \(S\). This is a membership-based formulation independent of a choice of representative.
Let \(S\) be a finite subset of a type \(\alpha \), and let \(e\) be an unordered pair of elements of \(\alpha \); write \((x,y)\) for a chosen ordered representative of \(e\). Then \(e\) crosses \(S\) — that is, some element of \(e\) lies in \(S\) and some element of \(e\) lies outside \(S\) — if and only if either \(x \in S\) and \(y \notin S\), or \(x \notin S\) and \(y \in S\).
Let \(G\) be a multigraph and let \(C\) be a cut of \(G\) determined by a vertex subset \(S\). Then the multiset of edges crossing \(C\) equals the sub-multiset of edges \(e\) of \(G\) for which some endpoint of \(e\) lies in \(S\) while some endpoint of \(e\) lies outside \(S\), counted with multiplicity.
The size of a cut \(C\) is the number of crossing edges, counted with multiplicity.
A cut \(C\) of \(G\) is a minimum cut when its size is at most the size of every cut \(C'\) of \(G\).
If \(e \in E(G)\) does not cross the cut \(C\), then \(C\) induces a cut of the contracted multigraph \(G/e\): the vertex side is the image of \(S\) after merging the endpoints of \(e\), and both nonemptiness conditions continue to hold because \(e\) has both endpoints on the same side.
Let \(G\) be a multigraph with vertex set \(V(G)\) and edge multiset \(E(G)\), and let \(C\) be a cut of \(G\), given by a nonempty proper subset \(S \subseteq V(G)\) with nonempty complement. Suppose \(e \in E(G)\) is an edge that does not cross \(C\), i.e. both endpoints of \(e\) lie on the same side of the partition. Then the cut induced on the contracted multigraph \(G/e\) by merging the endpoints of \(e\) has the same size as \(C\): the number of edges crossing the induced cut in \(G/e\), counted with multiplicity, equals the number of edges crossing \(C\) in \(G\).
Let \(G\) be a multigraph, and let \(C\) be a minimum cut of \(G\), given by a vertex subset \(S\) that is nonempty and has nonempty complement in \(V(G)\). Suppose \(e \in E(G)\) is an edge that does not cross \(C\), so that both endpoints of \(e\) lie on the same side of the partition. Then the cut induced by \(C\) on the contracted multigraph \(G/e\) — obtained by merging the endpoints of \(e\) and intersecting \(S\) with the surviving vertices — is again a minimum cut, of \(G/e\).
Given a multigraph \(G\) with at least one edge, a step of the algorithm is modelled as a function from an index \(i \in \mathrm{Fin}\, \left\lvert E(G)\right\rvert \) — thought of as a uniformly random edge choice — to the multigraph obtained by contracting the \(i\)-th edge of \(G\).
A run of the algorithm on \(G_0\) is indexed by a sequence of edge choices, one for each of the \(\left\lvert V(G_0)\right\rvert - 2\) contraction steps, and produces a multigraph. The current Lean definition is a placeholder that returns \(G_0\); the state-threading version is not yet formalized.
The predicate stating that \(G\) is a valid output of the algorithm, namely that it has exactly two vertices; its remaining edges are then exactly the edges of the output cut.
The degree of \(v\) in a loopless multigraph \(G\) is the number of edges incident to \(v\), counted with multiplicity.
Let \(e\) be an unordered pair of elements of a type \(\alpha \) with decidable equality, and let \((a, b)\) be the ordered pair chosen as a representative of \(e\). If an element \(z\) belongs to \(e\), then \(z = a\) or \(z = b\).
Let \(m\) be a multiset of unordered pairs (edges) drawn from a type \(\alpha \), and fix an element \(v \in \alpha \). For each edge \(e\), let \(\{ e\} _\ast \) denote the finite set of its endpoints — a singleton when \(e\) is a loop and a two-element set otherwise — and form the multiset obtained by concatenating \(\{ e\} _\ast \) over all \(e\) in \(m\), counting multiplicities of \(m\). Then the multiplicity of \(v\) in this concatenated multiset equals the number of edges \(e\) of \(m\) for which \(v\) is an endpoint of \(e\).
Let \(G\) be a loopless multigraph with vertex set \(V(G)\), and let \(v \in V(G)\) be a vertex whose deletion leaves at least one other vertex, i.e. \(V(G) \setminus \{ v\} \) is nonempty. Then the singleton \(S = \{ v\} \) is a cut of \(G\), and the size of this cut — the number of edges with exactly one endpoint in \(\{ v\} \), counted with multiplicity — equals the degree \(\deg (v)\) of \(v\).
Let \(G\) be a multigraph that admits a cut. Then for every vertex \(v\), the vertex set of \(G\) with \(v\) removed, \(V(G) \setminus \{ v\} \), is nonempty.
Let \(G\) be a loopless multigraph, let \(C\) be a minimum cut of \(G\), and let \(v\) be any vertex of \(G\). Then the size of \(C\) is at most the degree of \(v\), that is, \(\mathrm{size}(C) \le \deg (v)\).
Let \(G\) be a multigraph on a vertex type \(\alpha \), with vertex set \(V(G)\) and edge multiset \(E(G)\). If a point \(x \in \alpha \) occurs as an endpoint of some edge of \(G\) — that is, \(x\) lies in one of the unordered pairs making up \(E(G)\) — then \(x \in V(G)\).
Let \(m\) be a finite multiset with elements drawn from a type \(\alpha \), and let \(s\) be a finite set of elements of \(\alpha \) that contains every element occurring in \(m\). Writing \(\mathrm{count}_m(a)\) for the multiplicity of \(a\) in \(m\), the multiplicities over \(s\) sum to the total size of the multiset:
Let \(G\) be a loopless multigraph, given by a finite vertex set \(V\) together with a multiset \(E\) of edges, each edge an unordered pair of distinct vertices of \(V\). For a vertex \(v\), let \(\deg (v)\) be the number of edges of \(G\) incident to \(v\), counted with multiplicity. Then
where \(\left\lvert E\right\rvert \) is the number of edges counted with multiplicity.
Let \(G\) be a loopless multigraph with finite vertex set \(V\) and edge multiset \(E\), and let \(k\) be a natural number. If every vertex \(v \in V\) has degree at least \(k\) in \(G\), then
where \(\left\lvert V\right\rvert \) is the number of vertices and \(\left\lvert E\right\rvert \) is the number of edges counted with multiplicity.
For a cut size \(c\) and a current edge count \(m\), the probability that a uniformly chosen edge is not one of the \(c\) cut edges, namely
Let \(G_0\) be a multigraph, and let \(C_0\) be a minimum cut of \(G_0\), so that the number of edges crossing \(C_0\) (counted with multiplicity), its size, is no larger than that of any other cut. Then for every natural number \(i\) with \(i \lt \left\lvert V(G_0)\right\rvert - 1\),
where \(\left\lvert V(G_0)\right\rvert \) is the vertex count and \(\left\lvert E(G_0)\right\rvert \) is the edge count of \(G_0\).
For every integer \(n \ge 2\), the telescoping product
holds, where the factors are evaluated as real numbers.
Let \(C\) be a minimum cut of a multigraph \(G\), and write \(n\) for its number of vertices; suppose \(n \ge 4\). Then
Let \(G\) be a loopless multigraph whose vertex set is finite, and suppose \(G\) has \(n \ge 4\) vertices. Then running Karger’s random-contraction algorithm \(\binom {n}{2} = n(n-1)/2\) times independently and returning the smallest cut found succeeds with probability
Let \(m\) be a natural number and \(p \gt 0\) a real number. If \(m p \le 1\), then \(m \le p^{-1}\).
For every natural number \(n \ge 2\), the binomial coefficient counting the unordered pairs from an \(n\)-element set satisfies
an identity of real numbers.
For all natural numbers \(n\) and \(\alpha \), the binomial coefficient of \(n\) over \(2\alpha \) is bounded by the corresponding power of \(n\):
Let \(G\) be a multigraph whose (finite) vertex set has \(n \ge 2\) elements, and let \(m\) be a natural number. If
then \(m \le \binom {n}{2}\).
Let \(G\) be a multigraph with \(n\) vertices, and let \(\alpha \) and \(m\) be natural numbers with \(\alpha \ge 1\) and \(2\alpha \le n\). If, as an inequality of real numbers, \(m \cdot \binom {n}{2\alpha }^{-1} \le 1\), then \(m \le n^{2\alpha }\).