Shortest augmenting paths and the existence of maximum flows

A step of shortest-path augmentation takes a bounded s–t assignment f to the residual update of f along an augmenting walk of least length, by the bottleneck of that walk. This file proves that the relation is well-founded in the direction of successive steps, from any feasible assignment, over every linearly ordered additive commutative group of coefficients. Combined with the augmenting-path optimality criterion, this gives the existence of maximum assignments whenever a feasible one exists, and in particular of maximum ordinary flows for nonnegative capacities, so the max-flow/min-cut theorem. Since each step preserves values in an additive subgroup containing the bounds, it also gives integrality: for nonnegative capacities in an additive subgroup, some maximum flow takes its values in that subgroup.

The argument is that of Edmonds and Karp, and of Dinitz. Write d for the positive distance from s in the residual network of f, and d' for that of the augmented assignment. A residual arrow that becomes positive is the reverse of an arrow of the augmenting walk, so along it d decreases by one. Hence d rises by at most one along every positive residual arrow of the new assignment, and d ≤ d' (TauCeti.BoundedFlow.ShortestAugmentationStep.positiveEDist_le). When d' = d, the positive residual arrows u → v with d v = d u + 1 after the step are among those before it, and the arrow of the walk attaining the bottleneck is no longer positive. Since distances are bounded by the number of vertices, the distances and then the number of these arrows give a lexicographic measure that decreases at every step. The coefficients need not be discrete or Archimedean; augmentation along arbitrary augmenting paths need not terminate in that generality.

Main definitions

• TauCeti.BoundedFlow.ShortestAugmentationStep f g: g arises from f by one step of shortest-path augmentation.

Main results

• TauCeti.BoundedFlow.exists_shortestAugmentationStep_iff: for distinct terminals, a step exists exactly when there is an augmenting walk, and TauCeti.BoundedFlow.isMaximum_iff_forall_not_shortestAugmentationStep: an assignment is maximum exactly when no step starts from it.
• TauCeti.BoundedFlow.ShortestAugmentationStep.val_lt: each step strictly increases the value.
• TauCeti.BoundedFlow.ShortestAugmentationStep.positiveEDist_le: residual distances from the source do not decrease.
• TauCeti.BoundedFlow.wellFounded_shortestAugmentationStep: shortest-path augmentation terminates.
• TauCeti.BoundedFlow.exists_reflTransGen_shortestAugmentationStep_isMaximum: finitely many steps lead from any bounded s–t assignment to a maximum one.
• TauCeti.BoundedFlow.exists_val_eq_cutBound: the max-flow/min-cut theorem for bounded assignments.
• TauCeti.Flow.exists_isMaximum_mem and TauCeti.Flow.exists_val_eq_arrowSum: integrality and the max-flow/min-cut theorem for ordinary flows with nonnegative capacities.

References

• J. Edmonds, R. M. Karp, Theoretical improvements in algorithmic efficiency for network flow problems, J. ACM 19 (1972).
• E. A. Dinic, Algorithm for solution of a problem of maximum flow in a network with power estimation, Soviet Math. Dokl. 11 (1970).
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Chapter 10.

def TauCeti.BoundedFlow.ShortestAugmentationStep {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] {lo hi : Assignment Q K} {s t : V} (f g : BoundedFlow lo hi s t) : Prop

One step of shortest-path augmentation: g is the residual update of f along an augmenting walk p from s to t of least length, by the bottleneck of p. The walk traverses only residual arrows of positive capacity, its length is the positive distance from s to t in the residual network of f, and it traverses at least one arrow.

theorem TauCeti.BoundedFlow.shortestAugmentationStep_def {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] {lo hi : Assignment Q K} {s t : V} {f g : BoundedFlow lo hi s t} : f.ShortestAugmentationStep g ↔ ∃ (p : ArrowWalk (ResidualHom Q) s t) (hne : p.arrows ≠ []), (∀ a ∈ p.arrows, 0 < residualCapacity lo hi f.toFun a.snd.snd) ∧ ↑p.length = positiveEDist (residualCapacity lo hi f.toFun) s t ∧ g.toFun = residualUpdate f.toFun (walkAssignment p (ArrowWalk.bottleneck (residualCapacity lo hi f.toFun) p hne))

theorem TauCeti.BoundedFlow.exists_shortestAugmentationStep_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} (hst : s ≠ t) (f : BoundedFlow lo hi s t) : (∃ (g : BoundedFlow lo hi s t), f.ShortestAugmentationStep g) ↔ PositiveReachable (residualCapacity lo hi f.toFun) s t

For distinct terminals, a step of shortest-path augmentation starts from f exactly when f has an augmenting walk.

theorem TauCeti.BoundedFlow.isMaximum_iff_forall_not_shortestAugmentationStep {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) : f.IsMaximum ↔ ∀ (g : BoundedFlow lo hi s t), ¬f.ShortestAugmentationStep g

A bounded s–t assignment is maximum exactly when no step of shortest-path augmentation starts from it.

theorem TauCeti.BoundedFlow.ShortestAugmentationStep.val_lt {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 g : BoundedFlow lo hi s t} (h : f.ShortestAugmentationStep g) : f.val < g.val

A step of shortest-path augmentation strictly increases the value.

theorem TauCeti.BoundedFlow.ShortestAugmentationStep.toFun_mem {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] {lo hi : Assignment Q K} {s t : V} {f g : BoundedFlow lo hi s t} (H : AddSubgroup K) (hlo : ∀ ⦃v w : V⦄ (e : Q v w), lo e ∈ H) (hhi : ∀ ⦃v w : V⦄ (e : Q v w), hi e ∈ H) (h : f.ShortestAugmentationStep g) (hf : ∀ ⦃v w : V⦄ (e : Q v w), f.toFun e ∈ H) {v w : V} (e : Q v w) : g.toFun e ∈ H

Integrality of shortest-path augmentation. If the bounds and f take values in an additive subgroup H, then so does the result of a step of shortest-path augmentation.

theorem TauCeti.BoundedFlow.ShortestAugmentationStep.positiveEDist_le {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 g : BoundedFlow lo hi s t} (h : f.ShortestAugmentationStep g) (v : V) : positiveEDist (residualCapacity lo hi f.toFun) s v ≤ positiveEDist (residualCapacity lo hi g.toFun) s v

Monotonicity of residual distances. A step of shortest-path augmentation does not decrease the positive distance from the source in the residual network.

Termination

theorem TauCeti.BoundedFlow.wellFounded_shortestAugmentationStep {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} : WellFounded fun (g f : BoundedFlow lo hi s t) => f.ShortestAugmentationStep g

Termination of shortest-path augmentation. There is no infinite sequence of steps of shortest-path augmentation: the relation is well-founded in the direction of successive steps, from any bounded s–t assignment, whatever the coefficients.

theorem TauCeti.BoundedFlow.exists_reflTransGen_shortestAugmentationStep_isMaximum {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) : ∃ (g : BoundedFlow lo hi s t), Relation.ReflTransGen ShortestAugmentationStep f g ∧ g.IsMaximum

From any bounded s–t assignment, finitely many steps of shortest-path augmentation lead to a maximum one.

theorem TauCeti.BoundedFlow.exists_isMaximum {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) : ∃ (g : BoundedFlow lo hi s t), g.IsMaximum

Existence of maximum assignments. If some bounded s–t assignment exists, then a maximum one exists.

theorem TauCeti.BoundedFlow.exists_isMinimum {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) : ∃ (g : BoundedFlow lo hi s t), g.IsMinimum

A feasible bounded terminal problem has a minimum assignment, including when its values are all negative.

theorem TauCeti.BoundedFlow.exists_val_eq_cutBound {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} [DecidableEq V] (hst : s ≠ t) (f : BoundedFlow lo hi s t) : ∃ (g : BoundedFlow lo hi s t) (S : Finset V), s ∈ S ∧ t ∉ S ∧ g.val = cutBound lo hi S

Max-flow/min-cut theorem for bounded assignments. If some bounded s–t assignment between distinct terminals exists, then some bounded s–t assignment has value equal to the cut bound of some vertex set containing s but not t. By weak duality (TauCeti.BoundedFlow.val_le_cutBound) this assignment is maximum and this cut bound is minimum.

theorem TauCeti.BoundedFlow.exists_isMaximum_mem {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} (H : AddSubgroup K) (hlo : ∀ ⦃v w : V⦄ (e : Q v w), lo e ∈ H) (hhi : ∀ ⦃v w : V⦄ (e : Q v w), hi e ∈ H) (f : BoundedFlow lo hi s t) (hf : ∀ ⦃v w : V⦄ (e : Q v w), f.toFun e ∈ H) : ∃ (g : BoundedFlow lo hi s t), g.IsMaximum ∧ ∀ ⦃v w : V⦄ (e : Q v w), g.toFun e ∈ H

Integrality. If the bounds lie in an additive subgroup H and some bounded s–t assignment takes values in H, then some maximum bounded s–t assignment takes values in H.

Ordinary flows

theorem TauCeti.Flow.exists_isMaximum_mem {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] {cap : Assignment Q K} {s t : V} (hcap : 0 ≤ cap) (H : AddSubgroup K) (hcapH : ∀ ⦃v w : V⦄ (e : Q v w), cap e ∈ H) : ∃ (f : Flow cap s t), f.IsMaximum ∧ ∀ ⦃v w : V⦄ (e : Q v w), f.toFun e ∈ H

Integrality of maximum flows. For nonnegative capacities in an additive subgroup H, some maximum ordinary flow takes values in H. For distinct terminals, its value is the capacity of some cut by TauCeti.Flow.IsMaximum.exists_val_eq_arrowSum.

theorem TauCeti.Flow.exists_isMaximum {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] {cap : Assignment Q K} {s t : V} (hcap : 0 ≤ cap) : ∃ (f : Flow cap s t), f.IsMaximum

For nonnegative capacities, a maximum ordinary flow exists.

theorem TauCeti.Flow.exists_val_eq_arrowSum {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] {cap : Assignment Q K} {s t : V} [DecidableEq V] (hst : s ≠ t) (hcap : 0 ≤ cap) : ∃ (f : Flow cap s t) (S : Finset V), s ∈ S ∧ t ∉ S ∧ f.val = arrowSum cap S Sᶜ

Max-flow/min-cut theorem. For nonnegative capacities and distinct terminals, some ordinary flow has value equal to the capacity of the arrows leaving some vertex set containing s but not t. By weak duality (TauCeti.Flow.val_le_arrowSum) this flow is maximum and this cut is minimum.