Papers With

← All papers
First page of When is greedy exact for weighted minimum 3-cut?

When is greedy exact for weighted minimum 3-cut?

Armando Rodado Amaris

cs.DS Oct 26, 2026 · v1
formalization combinatorics
Read PDF arXiv abstract Code
TL;DR
Formalizes the greedy-exactness theorem, the 4/3 bound, the merge lemmas, and a 7-vertex counterexample (checked by kernel evaluation) in Lean 4.
Abstract
The greedy algorithm for minimum 3-cut splits a global minimum-weight cut and then the cheaper of its two sides; it is a tight $4/3$-approximation. We show that it is exact, from every global minimum-weight cut, whenever some optimal 3-partition has two parts joined by total weight at least the weighted edge connectivity $λ$. This extends both theorems of Hochbaum and Shmoys from unweighted planar graphs to all weighted graphs, recovers the $4/3$ bound, and generalizes to minimum $k$-cut with a one-paragraph proof. The remaining hard instances have all pair weights below $λ$; for them we prove a merge lemma for Gomory-Hu sides. Finally, we give a 7-vertex graph with a unique Gomory-Hu tree whose unique optimal 3-partition contains no side of that tree, so the first stage of Kapoor's algorithm does not suffice on its own. The main theorem, the 4/3 bound, the merge lemmas and the counterexample are verified in the Lean 4 proof assistant.
Problem

The greedy algorithm for weighted minimum 3-cut first takes a global minimum-weight cut and then splits the cheaper side. It is a tight 4/3-approximation. The question is when it is exact in general weighted graphs.

Approach

A case analysis based on posimodularity shows that greedy(S) ≤ max(λ + d(A), W(A,B,C)) for every 3-partition and every global minimum-weight cut. The remaining hard instances, where all pair weights are below λ, are handled with merge lemmas for Gomory–Hu sides. A 7-vertex counterexample shows that Gomory–Hu sides alone do not suffice for Kapoor's algorithm, and the argument extends to minimum k-cut. The general theorems are formalized in Lean 4 for all n, and the counterexample is verified by kernel evaluation.

Results

Greedy is exact whenever some optimum has two parts joined by weight at least λ. This extends the Hochbaum–Shmoys theorems to all weighted graphs and recovers the 4/3 bound. The 7-vertex graph has a unique Gomory–Hu tree and a unique optimum with no part equal to a tree side. Lean proofs and Python reproduction scripts are provided, and random and adversarial computational tests found no violations of the proved statements.