Karger's contraction algorithm as a randomized client #
Karger's contraction algorithm [Kar93] [KS96] keeps a weighted multigraph on its
current supervertices. It repeatedly picks an edge with probability proportional to its weight
and contracts it. Here the multigraph is an abstract data type, the contraction structure spec,
whose state is the weight matrix of the current supervertices (Graph) and whose operations are
deterministic:
sizeandtotalanswer the number of supervertices and the total doubled weightS;pairAt ranswers the pair(u, v)whose interval of the prefix sums of the weights contains the offsetr < S(sampledPair, the single-draw sampling ofKarger.Graph);contract u vmergesvintouand moves the last supervertex into slotv(contractMatrix).
The algorithm is a client with private coins, a ProbOracleComp Op.Result program, run against
spec.toRandomized.withCoins. Each step draws a uniform offset below S, asks for the pair there
and contracts it (contractStep), so it contracts each edge {u, v} with probability
2 W u v / S. contractTimes s makes s steps, and karger contracts down to two supervertices
and answers half their total weight, the weight of the cut between them.
All probability is proved here, on the specification. Run laws are derived over trackedSpec n, the
same structure that also keeps the block of original vertices merged into each supervertex
(TrackedGraph, Karger and Stein, Section 2). The blocks are bookkeeping:
forgetting them maps every run over trackedSpec n to the run of the same client over spec
(map_run_trackedSpec), so each statement about spec is the corresponding statement over the
blocks with the blocks forgotten. Contracting from t + s down to t supervertices preserves a
fixed minimum cut with probability at least t (t - 1) / ((t + s) (t + s - 1))
(trackedSurvives_contractTimes, hence survives_contractTimes). One run of karger over
trackedSpec n also outputs a cut, the block of the second of the two supervertices it leaves
(TrackedGraph.side, with law cutLaw W₀), and answers its weight (answer_eq_cutWeight_side,
answerLaw_eq_map_cutLaw). A minimum cut that survives down to two supervertices is the output
cut, up to complement, so karger outputs a fixed minimum cut with probability at least
2 / (n (n - 1)) (two_div_le_cutLaw). Hence it answers the minimum cut weight with at least that
probability (two_div_le_toOuterMeasure_karger), and every answer is the weight of a non-trivial
cut (exists_cut_of_mem_support_answerLaw), never less than the minimum
(minCut_le_of_mem_support_karger). Every call it makes is admissible (demonicValid_karger).
The combinatorics and the one-step bound are Karger.Graph's (isContractionOf_contract,
pullbackCut_contractCut, step_survival_prob_ge, telescope_survival_step), used unchanged,
and the composition of the stages is Probability.PMF.toOuterMeasure_bind_ge_mul_ennreal. The
bound on the number of minimum cuts is in CslibFrontier.Algorithms.Lean.Karger.MinCutCount.
Source map for the output cut ([KS96], author copy dated 6 August 1996):
- Section 2, the blocks
s(a)and the output cut(s(a), s(b)):TrackedGraph,TrackedGraph.side. - Lemma 2.1 (a cut is output if and only if no edge crossing it is contracted): the direction
used, a cut that survives is output, is
two_div_le_cutLaw's final step, withTrackedSurvivesfor the event that no crossing edge was contracted. - Theorem 2.2, a particular minimum cut is output with probability at least
C(n, 2)⁻¹:two_div_le_cutLaw.
Amplification is a client of a trial oracle whose one call answers one run of karger:
minRuns R makes R calls and keeps the least answer, one minStep per call after the first.
Answered by independent runs, OracleComp.evalWith (fun _ => answerLaw G), it misses the minimum
cut weight with probability at most (1 - 2 / (n (n - 1))) ^ R (minRuns_ne_minCut_le), since
the least answer misses it only when every run does (minRuns_ne_le, for any trial).
No register, address or instruction count appears here. The word-RAM loop
Cslib.Algorithms.WordRAM.Karger.contractDownTo simulates contractTimes: the graph it holds has
the law of the client's final state (Cslib.Algorithms.WordRAM.Karger.contractDownTo_law), so its
survival bound is survives_contractTimes. The programs of Cslib.Algorithms.WordRAM.KargerMinCut
simulate karger and minRuns in the same way. An implementation of spec over the memory
oracle is a separate, deterministic hop, and Refinement.toRandomized with
RandomizedRefinement.withCoins carries the law of the client through it.
Main definitions #
Graph,Op,step,valid,spec: the contraction structure.sampledPair,contractGraph: the pair sampled at an offset, and contraction.TrackedGraph,contractTracked,trackedStep,trackedSpec: the contraction structure with blocks.contractStep,contractTimes,karger: the algorithm as a client with coins.answerLaw: the law of the answer of one run ofkarger.TrackedGraph.side,cutLaw: the cut that one run ofkargeroutputs, and its law.minStep,minRuns: amplification, as a client of a trial oracle.TrackedSurvives,Survives: a cut of the input survives in a contraction, with and without blocks.
Main results #
map_run_trackedSpec: forgetting the blocks maps runs overtrackedSpec nto runs overspec.run_contractStep_bind,run_contractStep_bind_of_eq_zero: the run of one contraction, the step that an implementation simulates.trackedSurvives_contractTimes,survives_contractTimes: the survival bound.cutLaw_eq: the output cut is the block of supervertex1aftern - 2contractions.answer_eq_cutWeight_side,answerLaw_eq_map_cutLaw,isNonTrivialCut_of_mem_support_cutLaw: the answer is the weight of the output cut, which is non-trivial.two_div_le_cutLaw: each minimum cut is output with probability at least2 / (n (n - 1)).two_div_le_toOuterMeasure_karger: Karger's success probability.exists_of_mem_support_tracked_contractTimes,isContractionOf_of_mem_support_contractTimes,minCut_eq_zero_of_mem_support_contractTimes,exists_cut_of_mem_support_answerLaw,eq_zero_of_mem_support_answerLaw,minCut_le_of_mem_support_karger: every outcome is a contraction (preservingminCut = 0), so the answer is the weight of a non-trivial cut, never below the minimum (and always0whenminCut = 0).answerLaw_eq: the answer is half the total weight of the graph left byn - 2contractions.minRuns_ne_minCut_le: amplified Karger,Rindependent runs miss with probability at most(1 - 2 / (n (n - 1))) ^ R.mem_support_iterate_minStep,mem_support_minRuns: every amplified answer is the answer of one of the runs.minRuns_ne_le: amplification of any trial whose answers are at leastm.isCostBounded_contractStep,isCostBounded_contractTimes: each contraction makes one coin call and at most four calls of the structure.demonicValid_contractTimes,demonicValid_karger: every call is admissible.
References #
The contraction structure #
The answer type of each operation.
Instances For
Admissibility: an offset below the total weight, and two distinct supervertices.
Instances For
The contraction structure.
Instances For
The pair sampled at an offset is the unique pair whose interval contains it.
The contraction structure with blocks #
The graph of a tracked contraction, forgetting the blocks.
Instances For
The singleton blocks of the uncontracted graph W.
Instances For
Contraction with blocks: contractGraph on the weights, and contractBlocks on the blocks.
Arguments out of range leave the graph unchanged.
Instances For
Contraction with blocks at a pair of supervertices in range.
Forgetting the blocks commutes with contraction.
The transition function of the contraction structure with blocks: step on the weights.
Instances For
The contraction structure with blocks: the operations of spec, with the same answers.
Instances For
The steps of the two structures agree on the graph.
The algorithm #
A call of the contraction structure, in a program with coins.
Instances For
One contraction: draw a uniform offset below the total weight, and contract the pair sampled there. A weightless graph contracts its first and last supervertices.
Instances For
Contract s times.
Instances For
Karger's algorithm: contract down to two supervertices, and answer the weight between them, half their total weight.
Instances For
Runs #
The blocks are bookkeeping. Every client with coins draws the same answers and the same
graphs over the structure with blocks as over spec: TrackedGraph.toGraph represents the state
(Cslib.ProbOracleComp.run_interpret_map_state).
One contraction of a graph with positive total weight, over the structure with blocks: a uniform offset below the total doubled weight, then contraction of the pair sampled there.
One contraction of a weightless graph contracts its first and last supervertices.
One contraction of a graph of positive weight draws a uniform offset below the weight and contracts the pair sampled there.
One contraction of a weightless graph contracts its first and last supervertices.
Survival of a minimum cut #
The cut C of W₀ survives in G: G is a contraction of W₀ to t supervertices along
a map whose fibres are the blocks of G, under which C is the preimage of a cut.
Instances For
Survival of a minimum cut, over the blocks [KS96]. Contracting a contraction
of a connected multigraph W₀ from t + s down to t ≥ 2 supervertices, with the fibres of its
map as blocks, preserves a fixed minimum cut with probability at least
t (t - 1) / ((t + s) (t + s - 1)).
A cut that survives over the blocks survives in the graph.
Survival of a minimum cut [KS96]. Contracting a contraction of a connected
multigraph W₀ from t + s down to t ≥ 2 supervertices preserves a fixed minimum cut with
probability at least t (t - 1) / ((t + s) (t + s - 1)). This is trackedSurvives_contractTimes
with the blocks forgotten.
Every outcome is a contraction #
Every outcome of s contractions of a contraction of W₀ from t + s ≥ 2 supervertices,
with the fibres of its map as blocks, is a contraction of W₀ to t supervertices with the fibres
of its map as blocks.
Every outcome of s contractions of a contraction of W₀ from t + s ≥ 2 supervertices is a
contraction of W₀ to t supervertices. This is exists_of_mem_support_tracked_contractTimes
with the blocks forgotten.
Every outcome of s contractions of a disconnected (minCut W = 0) multigraph down to
t ≥ 2 supervertices is a multigraph with minCut = 0.
The output cut #
The cut that a tracked contraction to two supervertices outputs: the block of supervertex
1.
Instances For
The output cut is the block of supervertex 1 after n - 2 contractions.
The answer is the weight of the output cut. Every outcome of karger on a multigraph with
n ≥ 2 vertices, over the structure with blocks, outputs a non-trivial cut side and answers its
weight.
The answer of karger on a multigraph with n ≥ 2 vertices is the weight of the cut it
outputs: its law is the image of cutLaw under cutWeight.
Karger's theorem for a fixed cut [KS96]. On a connected multigraph on Fin n,
karger outputs a fixed minimum cut {C, Cᶜ} with probability at least
2 / (n (n - 1)) = 1 / C(n, 2). (C non-trivial forces n ≥ 2.)
Karger's theorem #
Karger's theorem [Kar93]. On a connected multigraph with n ≥ 2 vertices, karger
answers the minimum cut weight with probability at least 2 / (n (n - 1)).
Every answer of karger on a multigraph with n ≥ 2 vertices is the weight of a non-trivial
cut.
On a disconnected (minCut W₀ = 0) multigraph with n ≥ 2 vertices, every answer of karger
is 0.
One-sided error. Every answer of karger on a multigraph with n ≥ 2 vertices is the
weight of a non-trivial cut, so it is never below the minimum cut weight.
Amplification #
One more run of a trial, keeping the least answer b so far. The trial is an oracle whose one
call () answers one run of karger.
Instances For
After the least answer b of earlier runs, R more runs answer at most b: either b or the
answer of one of them.
Amplification. If every answer of a run is at least m and a run misses m with
probability at most q, then R independent runs all miss it, so minRuns R misses it, with
probability at most q ^ R.
Amplification of Karger's algorithm [Kar93]. On a connected multigraph with n ≥ 2
vertices, R independent runs of karger all miss the minimum cut weight, so minRuns R misses
it, with probability at most (1 - 2 / (n (n - 1))) ^ R.
Calls #
One contraction makes at most one coin call and four calls of the structure.
s contractions make at most s coin calls and 4 s calls of the structure.
Admissibility #
Every call of s contractions of a multigraph on t + s ≥ 2 supervertices is admissible.
Every call of karger on a multigraph with n ≥ 2 vertices is admissible.