Minimum cuts from a maximum assignment

Let f be a maximum bounded s–t assignment for lower and upper bounds lo and hi, between distinct terminals. Weak duality and the augmenting-path optimality criterion show that the minimum of the cut bound cutBound lo hi over the vertex sets containing s but not t is the value of f. The residual cut gap identity TauCeti.BoundedFlow.cutBound_sub_val then identifies the minimum cuts: they are exactly the vertex sets containing s but not t that no residual arrow of positive capacity leaves.

Consequently every minimum cut contains all vertices that are positively reachable from the source for the residual capacities of f, and no vertex from which the sink is positively reachable. Both bounds are attained: the vertices reachable from the source form the smallest minimum cut, and the vertices from which the sink is not reachable form the largest. So a vertex lies on the source side of every minimum cut exactly when it is reachable from the source, and on the source side of none exactly when the sink is reachable from it; the minimum cut is unique exactly when every vertex is of one of these two kinds. Since the minimum cuts do not mention f, both reachability relations are the same for every maximum assignment.

The bounds may be negative and the value of f may have either sign. The ordinary-flow statements, for zero lower bounds and the cut capacity of the arrows leaving a set, follow by specialization.

Main results

• TauCeti.BoundedFlow.IsMaximum.isMinimum_cutBound_iff: the minimum cuts are the terminal-separating sets that no residual arrow of positive capacity leaves.
• TauCeti.BoundedFlow.IsMaximum.isMinimum_cutBound_iff_forall_positiveReachable: equivalently, the terminal-separating sets closed under residual positive reachability.
• TauCeti.BoundedFlow.IsMaximum.isLeast_filter_positiveReachable and TauCeti.BoundedFlow.IsMaximum.isGreatest_compl_filter_positiveReachable: the smallest and largest minimum cuts, by residual reachability from the source and to the sink.
• TauCeti.BoundedFlow.IsMaximum.mem_smallest_iff and TauCeti.BoundedFlow.IsMaximum.mem_largest_iff: the same, for the extremal cuts TauCeti.TerminalCut.smallest and TauCeti.TerminalCut.largest of the minimum-cut lattice.
• TauCeti.BoundedFlow.IsMaximum.existsUnique_isMinimum_iff: the minimum cut is unique exactly when every vertex is reachable from the source or reaches the sink.
• TauCeti.BoundedFlow.IsMaximum.positiveReachable_source_iff and TauCeti.BoundedFlow.IsMaximum.positiveReachable_sink_iff: residual reachability from the source and to the sink does not depend on the chosen maximum assignment.
• TauCeti.Flow.IsMaximum.isMinimum_iff, TauCeti.Flow.IsMaximum.mem_smallest_iff, TauCeti.Flow.IsMaximum.mem_largest_iff and TauCeti.Flow.IsMaximum.existsUnique_isMinimum_iff: the ordinary-flow specializations.

References

• L. R. Ford, D. R. Fulkerson, Flows in Networks, Princeton University Press, 1962.
• J.-C. Picard, M. Queyranne, On the structure of all minimum cuts in a network and applications, Math. Programming Stud. 13 (1980), 8–16.

theorem TauCeti.BoundedFlow.IsMaximum.isMinimum_cutBound_iff_val_eq {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hf : f.IsMaximum) {S : Finset V} : TerminalCut.IsMinimum (cutBound lo hi) {s} {t} S ↔ s ∈ S ∧ t ∉ S ∧ f.val = cutBound lo hi S

For a maximum bounded s–t assignment f, the minimum cuts for the cut bound are the vertex sets containing s but not t whose cut bound is the value of f.

theorem TauCeti.BoundedFlow.IsMaximum.val_eq_pairMinimumValue {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hf : f.IsMaximum) : f.val = TerminalCut.pairMinimumValue (cutBound lo hi) s t

The value of a maximum bounded terminal assignment is the directed minimum-cut value.

theorem TauCeti.BoundedFlow.IsMaximum.isMinimum_cutBound_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hf : f.IsMaximum) {S : Finset V} : TerminalCut.IsMinimum (cutBound lo hi) {s} {t} S ↔ s ∈ S ∧ t ∉ S ∧ ∀ v ∈ S, ∀ w ∉ S, ∀ (e : ResidualHom Q v w), residualCapacity lo hi f.toFun e = 0

Residual characterization of minimum cuts. For a maximum bounded s–t assignment f, the minimum cuts for the cut bound are exactly the vertex sets containing s but not t that no residual arrow of positive capacity leaves.

theorem TauCeti.BoundedFlow.IsMaximum.mem_of_positiveReachable {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hf : f.IsMaximum) {S : Finset V} (hS : TerminalCut.IsMinimum (cutBound lo hi) {s} {t} S) {v w : V} (h : PositiveReachable (residualCapacity lo hi f.toFun) v w) (hv : v ∈ S) : w ∈ S

A minimum cut is closed under positive reachability for the residual capacities of a maximum bounded s–t assignment.

theorem TauCeti.BoundedFlow.IsMaximum.isMinimum_cutBound_iff_forall_positiveReachable {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hf : f.IsMaximum) {S : Finset V} : TerminalCut.IsMinimum (cutBound lo hi) {s} {t} S ↔ s ∈ S ∧ t ∉ S ∧ ∀ v ∈ S, ∀ (w : V), PositiveReachable (residualCapacity lo hi f.toFun) v w → w ∈ S

For a maximum bounded s–t assignment f, the minimum cuts for the cut bound are exactly the vertex sets containing s but not t that are closed under positive reachability for the residual capacities of f.

theorem TauCeti.BoundedFlow.IsMaximum.isLeast_filter_positiveReachable {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hst : s ≠ t) (hf : f.IsMaximum) [DecidablePred (PositiveReachable (residualCapacity lo hi f.toFun) s)] : IsLeast {S : Finset V | TerminalCut.IsMinimum (cutBound lo hi) {s} {t} S} (Finset.filter (PositiveReachable (residualCapacity lo hi f.toFun) s) Finset.univ)

The vertices positively reachable from the source for the residual capacities of a maximum bounded s–t assignment form the smallest minimum cut.

theorem TauCeti.BoundedFlow.IsMaximum.isGreatest_compl_filter_positiveReachable {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hst : s ≠ t) (hf : f.IsMaximum) [DecidablePred fun (x : V) => PositiveReachable (residualCapacity lo hi f.toFun) x t] : IsGreatest {S : Finset V | TerminalCut.IsMinimum (cutBound lo hi) {s} {t} S} {x : V | PositiveReachable (residualCapacity lo hi f.toFun) x t}ᶜ

The vertices from which the sink is not positively reachable for the residual capacities of a maximum bounded s–t assignment form the largest minimum cut.

theorem TauCeti.BoundedFlow.IsMaximum.forall_isMinimum_mem_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hst : s ≠ t) (hf : f.IsMaximum) {v : V} : (∀ (S : Finset V), TerminalCut.IsMinimum (cutBound lo hi) {s} {t} S → v ∈ S) ↔ PositiveReachable (residualCapacity lo hi f.toFun) s v

A vertex lies on the source side of every minimum cut exactly when it is positively reachable from the source for the residual capacities of a maximum bounded s–t assignment.

theorem TauCeti.BoundedFlow.IsMaximum.forall_isMinimum_notMem_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hst : s ≠ t) (hf : f.IsMaximum) {v : V} : (∀ (S : Finset V), TerminalCut.IsMinimum (cutBound lo hi) {s} {t} S → v ∉ S) ↔ PositiveReachable (residualCapacity lo hi f.toFun) v t

A vertex lies on the source side of no minimum cut exactly when the sink is positively reachable from it for the residual capacities of a maximum bounded s–t assignment.

theorem TauCeti.BoundedFlow.IsMaximum.mem_smallest_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hst : s ≠ t) (hf : f.IsMaximum) (hsub : IsSubmodular (cutBound lo hi)) {v : V} : v ∈ TerminalCut.smallest hsub ⋯ ↔ PositiveReachable (residualCapacity lo hi f.toFun) s v

A vertex belongs to the smallest minimum cut exactly when it is positively reachable from the source for the residual capacities of a maximum bounded s–t assignment.

theorem TauCeti.BoundedFlow.IsMaximum.mem_largest_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hst : s ≠ t) (hf : f.IsMaximum) (hsub : IsSubmodular (cutBound lo hi)) {v : V} : v ∈ TerminalCut.largest hsub ⋯ ↔ ¬PositiveReachable (residualCapacity lo hi f.toFun) v t

A vertex belongs to the largest minimum cut exactly when the sink is not positively reachable from it for the residual capacities of a maximum bounded s–t assignment.

theorem TauCeti.BoundedFlow.IsMaximum.existsUnique_isMinimum_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hst : s ≠ t) (hf : f.IsMaximum) : (∃! S : Finset V, TerminalCut.IsMinimum (cutBound lo hi) {s} {t} S) ↔ ∀ (v : V), PositiveReachable (residualCapacity lo hi f.toFun) s v ∨ PositiveReachable (residualCapacity lo hi f.toFun) v t

The minimum cut is unique exactly when every vertex is positively reachable from the source or reaches the sink positively, for the residual capacities of a maximum bounded s–t assignment.

theorem TauCeti.BoundedFlow.IsMaximum.positiveReachable_source_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hst : s ≠ t) (hf : f.IsMaximum) {g : BoundedFlow lo hi s t} (hg : g.IsMaximum) {v : V} : PositiveReachable (residualCapacity lo hi f.toFun) s v ↔ PositiveReachable (residualCapacity lo hi g.toFun) s v

Positive reachability from the source for the residual capacities is the same for all maximum bounded s–t assignments.

theorem TauCeti.BoundedFlow.IsMaximum.positiveReachable_sink_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} {f : BoundedFlow lo hi s t} (hst : s ≠ t) (hf : f.IsMaximum) {g : BoundedFlow lo hi s t} (hg : g.IsMaximum) {v : V} : PositiveReachable (residualCapacity lo hi f.toFun) v t ↔ PositiveReachable (residualCapacity lo hi g.toFun) v t

Positive reachability of the sink for the residual capacities is the same for all maximum bounded s–t assignments.

Ordinary flows

theorem TauCeti.Flow.IsMaximum.isMinimum_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {s t : V} {f : Flow cap s t} (hf : f.IsMaximum) {S : Finset V} : TerminalCut.IsMinimum (fun (S : Finset V) => arrowSum cap S Sᶜ) {s} {t} S ↔ s ∈ S ∧ t ∉ S ∧ ∀ v ∈ S, ∀ w ∉ S, ∀ (e : ResidualHom Q v w), residualCapacity 0 cap f.toFun e = 0

Residual characterization of minimum cuts for ordinary flows. For a maximum ordinary s–t flow f, the minimum cuts for the capacity of the arrows leaving a set are exactly the vertex sets containing s but not t that no residual arrow of positive capacity leaves.

theorem TauCeti.Flow.IsMaximum.forall_isMinimum_mem_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {s t : V} {f : Flow cap s t} (hst : s ≠ t) (hf : f.IsMaximum) {v : V} : (∀ (S : Finset V), TerminalCut.IsMinimum (fun (S : Finset V) => arrowSum cap S Sᶜ) {s} {t} S → v ∈ S) ↔ PositiveReachable (residualCapacity 0 cap f.toFun) s v

A vertex lies on the source side of every minimum cut exactly when it is positively reachable from the source for the residual capacities of a maximum ordinary s–t flow.

theorem TauCeti.Flow.IsMaximum.forall_isMinimum_notMem_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {s t : V} {f : Flow cap s t} (hst : s ≠ t) (hf : f.IsMaximum) {v : V} : (∀ (S : Finset V), TerminalCut.IsMinimum (fun (S : Finset V) => arrowSum cap S Sᶜ) {s} {t} S → v ∉ S) ↔ PositiveReachable (residualCapacity 0 cap f.toFun) v t

A vertex lies on the source side of no minimum cut exactly when the sink is positively reachable from it for the residual capacities of a maximum ordinary s–t flow.

theorem TauCeti.Flow.IsMaximum.mem_smallest_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {s t : V} {f : Flow cap s t} (hst : s ≠ t) (hf : f.IsMaximum) (hsub : IsSubmodular fun (S : Finset V) => arrowSum cap S Sᶜ) {v : V} : v ∈ TerminalCut.smallest hsub ⋯ ↔ PositiveReachable (residualCapacity 0 cap f.toFun) s v

A vertex belongs to the smallest minimum cut exactly when it is positively reachable from the source for the residual capacities of a maximum ordinary s–t flow.

theorem TauCeti.Flow.IsMaximum.mem_largest_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {s t : V} {f : Flow cap s t} (hst : s ≠ t) (hf : f.IsMaximum) (hsub : IsSubmodular fun (S : Finset V) => arrowSum cap S Sᶜ) {v : V} : v ∈ TerminalCut.largest hsub ⋯ ↔ ¬PositiveReachable (residualCapacity 0 cap f.toFun) v t

A vertex belongs to the largest minimum cut exactly when the sink is not positively reachable from it for the residual capacities of a maximum ordinary s–t flow.

theorem TauCeti.Flow.IsMaximum.existsUnique_isMinimum_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {s t : V} {f : Flow cap s t} (hst : s ≠ t) (hf : f.IsMaximum) : (∃! S : Finset V, TerminalCut.IsMinimum (fun (S : Finset V) => arrowSum cap S Sᶜ) {s} {t} S) ↔ ∀ (v : V), PositiveReachable (residualCapacity 0 cap f.toFun) s v ∨ PositiveReachable (residualCapacity 0 cap f.toFun) v t

The minimum cut is unique exactly when every vertex is positively reachable from the source or reaches the sink positively, for the residual capacities of a maximum ordinary s–t flow.

Example

On the vertices s = 0, a = 1, b = 2 and t = 3, take the arrows s → a with bounds [-2, 1], s → b with bounds [0, 3], a → t with bounds [-1, 1], b → t with bounds [0, 1] and t → s with bounds [-1, 0], and one arrow with bounds [0, 0] for every other ordered pair, loops included. The assignment 1, 1, 1, 1, -1 on the five main arrows has value 3, which is the cut bound of {s, b}, so it is maximum. In its residual network b is positively reachable from s, and t is positively reachable only from itself. So the smallest minimum cut is {s, b} and the largest is {s, a, b}; in particular the minimum cut is not unique. The cut {s} is not minimum: its residual gap is the room 2 left on s → b.