Finding and Certifying Weighted Minimum Cuts with Cut Queries
Troy Lee
cs.DS
Nov 2, 2026 · v2
TL;DR
Develops a Lean 4 library for cut-query algorithms that formalizes the paper's certificate and deterministic minimum-cut results, with an appendix mapping theorems to Lean statements.
Abstract
We study the deterministic and nondeterministic cut query complexity of minimum cut in undirected graphs with arbitrary nonnegative edge weights. For the nondeterministic case, we show that every $n$-vertex graph has an $O(n\log^2(2n))$-query certificate of its exact global minimum-cut value, such that any other nonnegatively weighted graph on the same vertex set that agrees on these queries has the same minimum cut value. A key ingredient is a way to certify a maximum $s$–$t$ flow value with only $O(n)$ cut queries. For the deterministic case we give an algorithm that finds an exact global minimum cut using $O(n^{3/2}\log^3(2n)(\log\log(2n))^2)$ cut queries. Previously no $O(n^{2-\varepsilon})$ deterministic bound was known for arbitrary nonnegatively weighted graphs. The algorithm follows Karger's two-respecting tree approach. The key new ingredient is a deterministic construction of a weak skeleton of the input graph $G$: an explicit weighted graph $H$ in which every minimum cut of $G$ is a $5/4$-approximate minimum cut.
Problem
The paper studies the deterministic and nondeterministic cut-query complexity of finding the global minimum cut in undirected graphs with arbitrary nonnegative edge weights. Before this work, no deterministic O(n^{2-ε}) bound was known for such graphs.
Approach
For certificates, a maximum s–t flow is certified with O(n) cut queries by encoding an optimal dual solution of an auxiliary min-cost flow as potentials on a tree. This is combined with isolating cuts and terminal halving. For the deterministic algorithm, a weak skeleton is built by learning a tree cut sparsifier and then converting it, after which Karger's two-respecting tree approach is applied. The results are formalized in a Lean 4 library, with Claude and GPT models assisting the formalization.
Results
Every n-vertex graph has an O(n log^2 n)-query certificate of its minimum-cut value. A deterministic algorithm finds an exact minimum cut with O(n^{3/2} polylog n) cut queries. The Lean library formalizes the named results except a few remarks, as recorded in Appendix A.
