Non-crossing minimum cuts

Minimum cuts of a submodular set function can be uncrossed by intersection and union without changing their values. For a symmetric submodular set function, complementing one of the cuts also lets them be uncrossed by the two set differences.

The main result is the non-crossing lemma. If two vertices lie on the same side of a minimum s–t cut, they have a minimum cut with one side contained in that s–t side. This is a basic ingredient in constructions of Gomory–Hu cut trees.

Those constructions maintain a whole family of pairwise non-crossing minimum cuts. Two cuts cross when each side of one meets each side of the other; representing every cut by its side avoiding a fixed root vertex turns a non-crossing family into a laminar one, whose members are pairwise nested or disjoint. Uncrossing by union preserves non-crossing, which gives the multi-cut non-crossing lemma: if no member of such a family separates s from t, some minimum s–t cut crosses none of its members.

References

• B. Korte and J. Vygen, Combinatorial Optimization: Theory and Algorithms, Section 8.6.
• D. Gusfield, Very Simple Methods for All Pairs Network Flow Analysis, SIAM J. Comput. 19 (1990), 143–155.

theorem TauCeti.TerminalCut.IsMinimum.uncross_union_inter {V : Type u_1} {K : Type u_2} [DecidableEq V] [AddCommMonoid K] [Preorder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSubmodular f) {A B C D S T : Finset V} (hS : IsMinimum f A B S) (hT : IsMinimum f C D T) (hunion : IsAdmissible C D (S ∪ T)) (hinter : IsAdmissible A B (S ∩ T)) : IsMinimum f C D (S ∪ T) ∧ IsMinimum f A B (S ∩ T)

Uncross two minimum cuts by union and intersection when the resulting sides have the required terminal orientations.

theorem TauCeti.TerminalCut.IsMinimum.uncross_sdiff {V : Type u_1} {K : Type u_2} [DecidableEq V] [AddCommMonoid K] [Preorder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} [Fintype V] (hf : IsSymmSubmodular f) {A B C D S T : Finset V} (hS : IsMinimum f A B S) (hT : IsMinimum f C D T) (hST : IsAdmissible A B (S \ T)) (hTS : IsAdmissible C D (T \ S)) : IsMinimum f A B (S \ T) ∧ IsMinimum f C D (T \ S)

Uncross two minimum cuts by set difference when the resulting sides have the required terminal orientations.

theorem TauCeti.TerminalCut.IsMinimum.exists_isMinimum_subset {V : Type u_1} {K : Type u_2} [Fintype V] [DecidableEq V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSymmSubmodular f) {s t u v : V} {S : Finset V} (hS : IsMinimum f {s} {t} S) (hu : u ∈ S) (hv : v ∈ S) (huv : u ≠ v) : ∃ T ⊆ S, IsMinimum f {u} {v} T ∨ IsMinimum f {v} {u} T

Non-crossing lemma. If u and v lie on the same side S of a minimum s–t cut, then some minimum cut between u and v has a side contained in S. The contained side may be oriented from either of its two terminals.

theorem TauCeti.TerminalCut.exists_isMinimum_forall_not_crosses {V : Type u_1} {K : Type u_2} [Fintype V] [DecidableEq V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K} (hf : IsSymmSubmodular f) {𝒞 : Set (Finset V)} (h𝒞 : 𝒞.Pairwise fun (Y Z : Finset V) => ¬Y.Crosses Z) (hmin : ∀ Y ∈ 𝒞, ∃ (a : V) (b : V), IsMinimum f {a} {b} Y) {s t : V} (hst : s ≠ t) (hsep : ∀ Y ∈ 𝒞, s ∈ Y ↔ t ∈ Y) : ∃ (X : Finset V), IsMinimum f {s} {t} X ∧ ∀ Y ∈ 𝒞, ¬X.Crosses Y

Multi-cut non-crossing lemma. Let 𝒞 be a pairwise non-crossing family of cuts, each a minimum cut of a symmetric submodular f between some pair of vertices. If none of them separates the distinct vertices s and t, then some minimum s–t cut crosses none of them.