Max-flow min-cut theorem

DefinitionFeasible flow#✓fully proved

Let \(V\) be a finite set, \(c : V \times V \to \mathbb{R}\) a capacity function and \(s, t \in V\). A function \(f : V \times V \to \mathbb{R}\) is a feasible \(s\)-\(t\) flow for \(c\) if \(0 \le f(u, v) \le c(u, v)\) for all \(u, v \in V\) and \(f\) is conserved at every vertex \(v \ne s, t\), that is, \(\sum_{u \in V} f(u, v) = \sum_{w \in V} f(v, w)\).

def IsFeasibleFlow {V : Type*} [Fintype V] [DecidableEq V]
    (cap : V → V → ℝ) (s t : V) (f : V → V → ℝ) : Prop :=
  (∀ u v, 0 ≤ f u v) ∧
  (∀ u v, f u v ≤ cap u v) ∧
  (∀ v, v ≠ s → v ≠ t → ∑ u : V, f u v = ∑ w : V, f v w)

Used by 6

Used byNo \(s\)-\(t\) cut is smaller than the Edmonds–Karp residual cut · Edmonds-Karp computes a maximum flow and a minimum cut · Integral flow theorem · A feasible skew flow gives a feasible flow · Weak duality for flows and cuts · Max-flow min-cut theorem

DefinitionFlow value#✓fully proved

For a finite set \(V\), a vertex \(s \in V\) and a function \(f : V \times V \to \mathbb{R}\), the value of \(f\) is its net outflow from the source \(s\), \(\sum_{v \in V} f(s, v) - \sum_{u \in V} f(u, s)\).

def flowValue {V : Type*} [Fintype V] [DecidableEq V]
    (s : V) (f : V → V → ℝ) : ℝ :=
  (∑ v : V, f s v) - ∑ u : V, f u s

Used by 6

Used byNo \(s\)-\(t\) cut is smaller than the Edmonds–Karp residual cut · Edmonds-Karp computes a maximum flow and a minimum cut · Integral flow theorem · Flow across a cut · Weak duality for flows and cuts · Max-flow min-cut theorem

DefinitionSource–sink cut#✓fully proved

For a finite set \(V\) and vertices \(s, t \in V\), an \(s\)-\(t\) cut is a subset \(S \subseteq V\) with \(s \in S\) and \(t \notin S\).

def IsSTCut {V : Type*} [Fintype V] [DecidableEq V]
    (s t : V) (S : Finset V) : Prop :=
  s ∈ S ∧ t ∉ S

Used by 6

Used byNo \(s\)-\(t\) cut is smaller than the Edmonds–Karp residual cut · Edmonds-Karp computes a maximum flow and a minimum cut · Integral flow theorem · The Edmonds-Karp residual cut separates source and sink · Weak duality for flows and cuts · Max-flow min-cut theorem

DefinitionCut capacity#✓fully proved

Let \(V\) be a finite set and \(c : V \times V \to \mathbb{R}\) a capacity function. The capacity of a subset \(S \subseteq V\) is the total capacity of the arcs leaving \(S\), \(\sum_{u \in S} \sum_{v \in V \setminus S} c(u, v)\).

def cutCapacity {V : Type*} [Fintype V] [DecidableEq V]
    (cap : V → V → ℝ) (S : Finset V) : ℝ :=
  ∑ u ∈ S, ∑ v ∈ (Finset.univ : Finset V) \ S, cap u v

Used by 5

Used byNo \(s\)-\(t\) cut is smaller than the Edmonds–Karp residual cut · Edmonds-Karp computes a maximum flow and a minimum cut · Integral flow theorem · Weak duality for flows and cuts · Max-flow min-cut theorem

TheoremFlow across a cut#✓fully proved

Let \(V\) be a finite set, \(s, t \in V\), and \(f : V \times V \to \mathbb{R}\) a function conserved at every vertex \(v \ne s, t\), that is, \(\sum_{u \in V} f(u, v) = \sum_{w \in V} f(v, w)\); no sign or capacity condition is imposed. Then for every subset \(S \subseteq V\) with \(s \in S\) and \(t \notin S\), the flow value \(\sum_{v \in V} f(s, v) - \sum_{u \in V} f(u, s)\) of \(f\) equals \(\sum_{u \in S} \sum_{v \in V \setminus S} f(u, v) - \sum_{u \in S} \sum_{v \in V \setminus S} f(v, u)\), the flow leaving \(S\) minus the flow entering \(S\).

theorem cutFlow_eq {V : Type*} [Fintype V] [DecidableEq V]
    (s t : V) (f : V → V → ℝ)
    (hcons : ∀ v, v ≠ s → v ≠ t → ∑ u : V, f u v = ∑ w : V, f v w)
    (S : Finset V) (hs : s ∈ S) (ht : t ∉ S) :
    flowValue s f = (∑ u ∈ S, ∑ v ∈ Finset.univ \ S, f u v) -
      (∑ u ∈ S, ∑ v ∈ Finset.univ \ S, f v u)

Uses 1 · Used by 2

Statement usesFlow value

Used byWeak duality for flows and cuts · Max-flow min-cut theorem

TheoremWeak duality for flows and cuts#✓fully proved

Let \(V\) be a finite set, \(c : V \times V \to \mathbb{R}\) a capacity function and \(s, t \in V\). If \(f\) is a feasible \(s\)-\(t\) flow for \(c\) and \(S\) is an \(s\)-\(t\) cut, then the flow value of \(f\) is at most the capacity of \(S\) for \(c\).

theorem flowValue_le_cutCapacity {V : Type*} [Fintype V] [DecidableEq V]
    (cap : V → V → ℝ) (s t : V) (f : V → V → ℝ)
    (hf : IsFeasibleFlow cap s t f) (S : Finset V) (hS : IsSTCut s t S) :
    flowValue s f ≤ cutCapacity cap S

Uses 5 · Used by 2

Statement usesFeasible flow · Source–sink cut · Cut capacity · Flow value

Proof usesFlow across a cut

Used byEdmonds-Karp computes a maximum flow and a minimum cut · Max-flow min-cut theorem

TheoremMax-flow min-cut theorem#✓fully proved

Let \(V\) be a finite set, \(c : V \times V \to \mathbb{R}\) a capacity function with \(c(u, v) \ge 0\) for all \(u, v \in V\), and \(s, t \in V\) with \(s \ne t\). Then there is a feasible \(s\)-\(t\) flow \(f\) for \(c\) whose value is at least the value of every feasible \(s\)-\(t\) flow for \(c\) and at most the capacity of every \(s\)-\(t\) cut, and there is an \(s\)-\(t\) cut whose capacity equals the value of \(f\). In other words, the maximum value of a feasible \(s\)-\(t\) flow equals the minimum capacity of an \(s\)-\(t\) cut.

theorem max_flow_min_cut
    {V : Type*} [Fintype V] [DecidableEq V]
    (cap : V → V → ℝ) (hcap : ∀ u v, 0 ≤ cap u v)
    (s t : V) (hst : s ≠ t) :
    ∃ f : V → V → ℝ, IsFeasibleFlow cap s t f ∧
      (∀ f' : V → V → ℝ, IsFeasibleFlow cap s t f' → flowValue s f' ≤ flowValue s f) ∧
      (∀ S : Finset V, IsSTCut s t S → flowValue s f ≤ cutCapacity cap S) ∧
      ∃ S : Finset V, IsSTCut s t S ∧ flowValue s f = cutCapacity cap S

Sources

• L. R. Ford and D. R. Fulkerson, Canad. J. Math. 8 (1956), 399-404, DOI 10.4153/CJM-1956-045-5.

Uses 6

Statement usesFeasible flow · Source–sink cut · Cut capacity · Flow value

Proof usesFlow across a cut · Weak duality for flows and cuts

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.