Edmonds–Karp algorithm

AbbreviationFlow#✓fully proved

A flow on \(n\) vertices, labelled \(0, \dots, n-1\), is an integer matrix: it assigns an integer \(f(u, v)\) to each ordered pair of vertices \((u, v)\).

No condition is imposed here; skew symmetry, capacity bounds and conservation are required by feasibility.

abbrev Flow (n : Nat) := Fin n → Fin n → Int

Used by 32

Used byArc flow of an integer flow · Augmenting a flow along a path · Augmentation within residual capacities preserves feasibility · Bottleneck augmentation preserves feasibility · Two-sided capacity bounds for a feasible flow · Edmonds–Karp maximum flow · The Edmonds–Karp flow is feasible · Edmonds-Karp computes a maximum flow and a minimum cut · Maximality of the Edmonds–Karp flow · The Edmonds–Karp flow value equals its residual cut capacity · No augmenting path remains after Edmonds–Karp · A skew flow is the difference of its arc flows · Flow value · Augmenting along a path changes the flow value by the amount · Weak max-flow min-cut duality · The augmentation loop never decreases the flow value · The flow value is at most the source capacity · One augmentation step keeps or strictly raises the flow value · Feasible flow · A feasible skew flow gives a feasible flow · Bottleneck of a path · Augmenting paths have positive bottleneck · Real arc flow · Residual capacity · Residual cut · Residual graph · Edges of the residual graph · Augmenting-path iteration with fuel · The iteration stops when there is no augmenting path · One augmenting-path step · Net outflow in the arc representation · Zero flow

DefinitionFlow value#✓fully proved

For a flow \(f\) on \(n\) vertices and a vertex \(s\), the value of \(f\) at \(s\) is the net flow leaving \(s\), namely the integer \(\sum_v f(s, v)\), where \(v\) runs over all vertices.

def flowValue {n : Nat} (source : Fin n) (flow : Flow n) : Int :=
  ∑ target, flow source target

Uses 1 · Used by 15

Statement usesFlow

Used byAugmentation within residual capacities preserves feasibility · Two-sided capacity bounds for a feasible flow · Edmonds-Karp computes a maximum flow and a minimum cut · Maximality of the Edmonds–Karp flow · The Edmonds–Karp flow value equals its residual cut capacity · No augmenting path remains after Edmonds–Karp · Augmenting along a path changes the flow value by the amount · Weak max-flow min-cut duality · The augmentation loop never decreases the flow value · The flow value is at most the source capacity · One augmentation step keeps or strictly raises the flow value · Feasible flow · A feasible skew flow gives a feasible flow · Net outflow in the arc representation · The zero flow is feasible

DefinitionFeasible flow#✓fully proved

Let \(c\) be a capacity function assigning a natural number \(c(u, v)\) to each ordered pair of vertices, and let \(s\) and \(t\) be vertices. A flow \(f\) is feasible for \(c\), \(s\) and \(t\) when it is skew symmetric, \(f(u, v) = -f(v, u)\) for all \(u\) and \(v\); it respects the capacities, \(f(u, v) \le c(u, v)\) for all \(u\) and \(v\); and it is conserved: for every vertex \(v\) other than \(s\) and \(t\), the net flow \(\sum_w f(v, w)\) leaving \(v\) is \(0\).

def IsFeasible {n : Nat} (capacity : Fin n → Fin n → Nat)
    (source sink : Fin n) (flow : Flow n) : Prop :=
  (∀ u v, flow u v = -flow v u) ∧
  (∀ u v, flow u v ≤ (capacity u v : Int)) ∧
  ∀ v, v ≠ source → v ≠ sink → flowValue v flow = 0

Uses 2 · Used by 12

Statement usesFlow · Flow value

Used byAugmentation within residual capacities preserves feasibility · Bottleneck augmentation preserves feasibility · Two-sided capacity bounds for a feasible flow · The Edmonds–Karp flow is feasible · Edmonds-Karp computes a maximum flow and a minimum cut · Maximality of the Edmonds–Karp flow · The Edmonds–Karp flow value equals its residual cut capacity · No augmenting path remains after Edmonds–Karp · Weak max-flow min-cut duality · The flow value is at most the source capacity · A feasible skew flow gives a feasible flow · The zero flow is feasible

DefinitionZero flow#✓fully proved

The zero flow on the vertices \(\{0, \dots, n - 1\}\) is the integer-valued matrix \(f\) with \(f(u, v) = 0\) for all vertices \(u\) and \(v\).

def zeroFlow (n : Nat) : Flow n := fun _ _ => 0

Uses 1 · Used by 4

Statement usesFlow

Used byEdmonds–Karp maximum flow · The Edmonds–Karp flow is feasible · No augmenting path remains after Edmonds–Karp · The zero flow is feasible

TheoremThe zero flow is feasible#✓fully proved

For every capacity matrix \(c\) with natural-number entries on the vertices \(\{0, \dots, n - 1\}\) and all vertices \(s\) and \(t\), the zero flow is feasible for \(c\) with source \(s\) and sink \(t\).

theorem zeroFlow_feasible {n : Nat} (capacity : Fin n → Fin n → Nat)
    (source sink : Fin n) : IsFeasible capacity source sink (zeroFlow n)

Uses 3 · Used by 1

Statement usesFeasible flow · Zero flow

Proof usesFlow value

Used byThe Edmonds–Karp flow is feasible

TheoremTwo-sided capacity bounds for a feasible flow#✓fully proved

Let \(c\) be a capacity matrix with natural-number entries on the vertices \(\{0, \dots, n-1\}\), let \(s\) and \(t\) be vertices, and let \(f\) be a flow that is feasible for \(c\), \(s\), \(t\). Then for all vertices \(u\) and \(v\), we have \(-c(v, u) \le f(u, v) \le c(u, v)\).

The lower bound follows from skew symmetry and the upper bound on the reverse entry.

theorem IsFeasible.capacity_bounds {n : Nat}
    {capacity : Fin n → Fin n → Nat} {source sink : Fin n}
    {flow : Flow n} (feasible : IsFeasible capacity source sink flow)
    (u v : Fin n) :
    -(capacity v u : Int) ≤ flow u v ∧ flow u v ≤ (capacity u v : Int)

Uses 3

Statement usesFlow · Feasible flow

Proof usesFlow value

DefinitionResidual graph#✓fully proved

Let \(c\) be a capacity matrix assigning a natural number \(c(u, v)\) to each ordered pair of vertices among \(0, \dots, n - 1\), and let \(f\) be a flow on these vertices. The residual graph of \(c\) and \(f\) is the directed adjacency graph whose vertices \(0, \dots, n - 1\) are enumerated in increasing order and in which the adjacency list of \(u\) consists of the vertices \(v\) with \(f(u, v) < c(u, v)\), that is, with positive residual capacity \(c(u, v) - f(u, v)\), in increasing order.

def residualGraph {n : Nat} (capacity : Fin n → Fin n → Nat)
    (flow : Flow n) : DirectedAdjacency (Fin n) where
  vertices := List.finRange n
  vertices_nodup := List.nodup_finRange n
  vertices_complete := List.mem_finRange
  adjacency u := (List.finRange n).filter fun v => decide (flow u v < capacity u v)

Uses 2 · Used by 14

Statement usesDirected adjacency graph · Flow

Used byBottleneck augmentation preserves feasibility · The Edmonds–Karp flow is feasible · Maximality of the Edmonds–Karp flow · The Edmonds–Karp flow value equals its residual cut capacity · No augmenting path remains after Edmonds–Karp · The augmentation loop never decreases the flow value · One augmentation step keeps or strictly raises the flow value · The Edmonds-Karp residual cut separates source and sink · Augmenting paths have positive bottleneck · Residual cut · Edges of the residual graph · Augmenting-path iteration with fuel · The iteration stops when there is no augmenting path · One augmenting-path step

TheoremEdges of the residual graph#✓fully proved

Let \(c\) be a capacity matrix with natural-number entries and \(f\) an integer matrix (the flow) on the vertices \(0, \dots, n - 1\). For all vertices \(u\) and \(v\), the residual graph of \(c\) and \(f\) has an edge from \(u\) to \(v\) if and only if \(f(u, v) < c(u, v)\).

@[simp]
theorem residualGraph_edge_iff {n : Nat}
    (capacity : Fin n → Fin n → Nat) (flow : Flow n) (u v : Fin n) :
    (residualGraph capacity flow).Edge u v ↔ flow u v < (capacity u v : Int)

Uses 3 · Used by 3

Statement usesEdge of a directed adjacency graph · Flow · Residual graph

Used byBottleneck augmentation preserves feasibility · The Edmonds–Karp flow value equals its residual cut capacity · Augmenting paths have positive bottleneck

DefinitionDirected path#✓fully proved

In a directed graph \(G\), a list \(p\) of vertices is a path from \(s\) to \(t\) when it is nonempty, its first entry is \(s\), its last entry is \(t\), every pair of consecutive entries \(u, v\) forms a directed edge of \(G\) from \(u\) to \(v\), and no vertex occurs twice in \(p\).

def IsPath {V : Type*} (graph : DirectedAdjacency V)
    (source sink : V) (path : List V) : Prop :=
  path.IsChainFromTo graph.Edge source sink ∧ path.Nodup

Uses 2 · Used by 8

Statement usesDirected adjacency graph · Edge of a directed adjacency graph

Used byBottleneck augmentation preserves feasibility · The Edmonds–Karp flow is feasible · No augmenting path remains after Edmonds–Karp · The augmentation loop never decreases the flow value · One augmentation step keeps or strictly raises the flow value · Augmenting paths have positive bottleneck · The shortest-path search succeeds exactly when the sink is reachable · Soundness of the shortest-path search

DefinitionDistance-guided path reconstruction#✓fully proved

Let \(G\) be a directed graph with ordered adjacency lists, \(d\) a partial labelling of its vertices by natural numbers, \(t\) a vertex, and \(\equiv\) a given Boolean test on pairs of vertices (not required to be equality). The reconstruction from a vertex \(u\) with \(k\) steps left returns the one-element list \([u]\) when \(k = 0\) and \(u \equiv t\) holds, and fails when \(k = 0\) and \(u \equiv t\) fails. When \(k \ge 1\), it takes the first out-neighbour \(w\) of \(u\) in adjacency order with \(d(w) = k - 1\); it fails if there is none, and otherwise returns \(u\) followed by the reconstruction from \(w\) with \(k - 1\) steps left, failing if that fails.

def pathFromDistances {V : Type*} [BEq V]
    (graph : DirectedAdjacency V) (distance : V → Option Nat) (sink : V) :
    Nat → V → Option (List V)
  | 0, current => if current == sink then some [current] else none
  | remaining + 1, current =>
      match (graph.adjacency current).find? fun next => distance next == some remaining with
      | none => none
      | some next =>
          (pathFromDistances graph distance sink remaining next).map (current :: ·)

Uses 1 · Used by 4

Statement usesDirected adjacency graph

Used bySoundness of distance-guided path reconstruction · Shortest path via breadth-first search · The shortest-path search succeeds exactly when the sink is reachable · Soundness of the shortest-path search

TheoremSoundness of distance-guided path reconstruction#✓fully proved

Let \(G\) be a directed adjacency graph on a type \(V\) whose Boolean test \(\equiv\) on pairs of vertices holds exactly for equal vertices, let \(d\) be a partial labelling of the vertices by natural numbers, let \(t\) and \(u\) be vertices, and let \(k\) be a natural number. If the distance-guided reconstruction for \(G\), \(d\) and \(t\) from \(u\) with \(k\) steps left succeeds and returns a list \(p\), then \(p\) is a walk from \(u\) to \(t\) in \(G\) (it is nonempty, its first entry is \(u\), its last entry is \(t\), and every pair of consecutive entries is an edge of \(G\)) and \(p\) has exactly \(k + 1\) entries.

theorem pathFromDistances_sound {V : Type*} [BEq V] [LawfulBEq V]
    (graph : DirectedAdjacency V) (distance : V → Option Nat) (sink : V)
    {remaining : Nat} {current : V} {path : List V}
    (result : pathFromDistances graph distance sink remaining current = some path) :
    path.IsChainFromTo graph.Edge current sink ∧ path.length = remaining + 1

Uses 3 · Used by 1

Statement usesDirected adjacency graph · Edge of a directed adjacency graph · Distance-guided path reconstruction

Used bySoundness of the shortest-path search

DefinitionShortest path via breadth-first search#✓fully proved

Let \(G\) be a finite directed graph on the vertices \(\{0, \dots, n - 1\}\) with ordered adjacency lists, and let \(s\) be a source and \(t\) a sink. Run breadth-first search from \(t\) in the reverse graph of \(G\); it labels each vertex \(v\) from which \(t\) is reachable with the distance from \(v\) to \(t\) in \(G\). If \(s\) has no label, the search returns no path. Otherwise, starting at \(s\) with label \(d\), take \(d\) steps, each time moving to the first out-neighbour (in adjacency order) whose label is one less than that of the current vertex. The search returns the list of visited vertices, from \(s\) to the last one, if every step succeeds and the last vertex is \(t\), and no path otherwise.

def shortestPath {n : Nat} (graph : DirectedAdjacency (Fin n))
    (source sink : Fin n) : Option (List (Fin n)) :=
  let search := bfs graph.transpose sink
  match search.distance source with
  | none => none
  | some distance => pathFromDistances graph search.distance sink distance source

Uses 5 · Used by 10

Statement usesResult of breadth-first search · Breadth-first search · Directed adjacency graph · Transpose of a directed adjacency graph · Distance-guided path reconstruction

Used byThe Edmonds–Karp flow is feasible · No augmenting path remains after Edmonds–Karp · The augmentation loop never decreases the flow value · One augmentation step keeps or strictly raises the flow value · Augmenting-path iteration with fuel · The iteration stops when there is no augmenting path · The shortest-path search fails exactly when the sink is unreachable · The shortest-path search succeeds exactly when the sink is reachable · Soundness of the shortest-path search · One augmenting-path step

TheoremSoundness of the shortest-path search#✓fully proved

Let \(G\) be a finite directed graph on the vertices \(\{0, \dots, n - 1\}\) and let \(s\) and \(t\) be vertices. If the breadth-first shortest-path search in \(G\) from \(s\) to \(t\) returns a list \(P\) of vertices, then \(P\) is a directed path in \(G\) from \(s\) to \(t\) without repeated vertices, and breadth-first search in \(G\) from \(s\) assigns \(t\) a distance \(d\) such that \(P\) has exactly \(d + 1\) vertices.

theorem shortestPath_sound {n : Nat} {graph : DirectedAdjacency (Fin n)}
    {source sink : Fin n} {path : List (Fin n)}
    (result : shortestPath graph source sink = some path) :
    IsPath graph source sink path ∧
      ∃ distance, (bfs graph source).distance sink = some distance ∧
        path.length = distance + 1

Uses 12 · Used by 5

Statement usesResult of breadth-first search · Breadth-first search · Directed adjacency graph · Directed path · Shortest path via breadth-first search

Proof usesBFS reports exactly the shortest walk length · Edge of a directed adjacency graph · Walks of a given length · Transpose of a directed adjacency graph · Walks in the transpose are reversed walks · Distance-guided path reconstruction · Soundness of distance-guided path reconstruction

Used byThe Edmonds–Karp flow is feasible · No augmenting path remains after Edmonds–Karp · The augmentation loop never decreases the flow value · One augmentation step keeps or strictly raises the flow value · The shortest-path search succeeds exactly when the sink is reachable

TheoremThe shortest-path search succeeds exactly when the sink is reachable#✓fully proved

Let \(G\) be a finite directed graph on the vertices \(\{0, \dots, n - 1\}\) and let \(s\) and \(t\) be vertices. The breadth-first shortest-path search in \(G\) from \(s\) to \(t\) returns some path if and only if \(t\) is reachable from \(s\) in \(G\) (every vertex counts as reachable from itself).

theorem shortestPath_present_iff_reachable {n : Nat}
    (graph : DirectedAdjacency (Fin n)) (source sink : Fin n) :
    (∃ path, shortestPath graph source sink = some path) ↔ graph.Reachable source sink

Uses 18 · Used by 1

Statement usesDirected adjacency graph · Reachability in a directed graph · Shortest path via breadth-first search

Proof usesResult of breadth-first search · Breadth-first search · BFS reports exactly the shortest walk length · BFS reports a distance exactly for the reachable vertices · Edge of a directed adjacency graph · Walks of a given length · Reachability by walks · Reachability in the transpose graph · Transpose of a directed adjacency graph · Splitting off the first edge of a walk · Walks in the transpose are reversed walks · Walks of length zero · Directed path · Distance-guided path reconstruction · Soundness of the shortest-path search

Used byThe shortest-path search fails exactly when the sink is unreachable

TheoremThe shortest-path search fails exactly when the sink is unreachable#✓fully proved

Let \(G\) be a finite directed graph on the vertices \(\{0, \dots, n - 1\}\) and let \(s\) and \(t\) be vertices. The breadth-first shortest-path search in \(G\) from \(s\) to \(t\) returns no path if and only if \(t\) is not reachable from \(s\) in \(G\).

theorem shortestPath_eq_none_iff_not_reachable {n : Nat}
    (graph : DirectedAdjacency (Fin n)) (source sink : Fin n) :
    shortestPath graph source sink = none ↔ ¬ graph.Reachable source sink

Uses 4 · Used by 1

Statement usesDirected adjacency graph · Reachability in a directed graph · Shortest path via breadth-first search

Proof usesThe shortest-path search succeeds exactly when the sink is reachable

Used byNo augmenting path remains after Edmonds–Karp

DefinitionEdges of a path#✓fully proved

The edges of a list \(v_0, v_1, \dots, v_k\) are the list of its consecutive ordered pairs \((v_0, v_1), (v_1, v_2), \dots, (v_{k-1}, v_k)\), in this order; the empty list and one-element lists have no edges.

def pathEdges {V : Type*} : List V → List (V × V)
  | [] | [_] => []
  | first :: second :: rest => (first, second) :: pathEdges (second :: rest)

Used by 3

Used byAugmentation within residual capacities preserves feasibility · Bottleneck augmentation preserves feasibility · Augmenting paths have positive bottleneck

DefinitionResidual capacity#✓fully proved

Let \(c\) be a capacity matrix with natural-number entries and \(f\) an integer matrix (the flow) on the vertices \(0, \dots, n - 1\). The residual capacity of an ordered pair of vertices \((u, v)\) is the integer \(c(u, v) - f(u, v)\).

def residualAmount {n : Nat} (capacity : Fin n → Fin n → Nat)
    (flow : Flow n) (source target : Fin n) : Int :=
  (capacity source target : Int) - flow source target

Uses 1 · Used by 4

Statement usesFlow

Used byAugmentation within residual capacities preserves feasibility · Bottleneck augmentation preserves feasibility · Bottleneck of a path · Augmenting paths have positive bottleneck

DefinitionBottleneck of a path#✓fully proved

Let \(c\) be a capacity matrix with natural-number entries and \(f\) an integer matrix (the flow) on the same vertices. The bottleneck of a list of vertices \(v_0, v_1, \dots, v_k\) with \(k \ge 1\) is the integer \(\min_{i < k} \bigl(c(v_i, v_{i+1}) - f(v_i, v_{i+1})\bigr)\), the least residual capacity of a consecutive pair; a list with at most one vertex has bottleneck \(0\).

def pathBottleneck {n : Nat} (capacity : Fin n → Fin n → Nat)
    (flow : Flow n) : List (Fin n) → Int
  | [] | [_] => 0
  | first :: second :: [] => residualAmount capacity flow first second
  | first :: second :: third :: rest =>
      min (residualAmount capacity flow first second)
        (pathBottleneck capacity flow (second :: third :: rest))

Uses 2 · Used by 9

Statement usesFlow · Residual capacity

Used byBottleneck augmentation preserves feasibility · The Edmonds–Karp flow is feasible · No augmenting path remains after Edmonds–Karp · The augmentation loop never decreases the flow value · One augmentation step keeps or strictly raises the flow value · Augmenting paths have positive bottleneck · Augmenting-path iteration with fuel · The iteration stops when there is no augmenting path · One augmenting-path step

DefinitionUnit skew flow along an oriented edge#✓fully proved

For vertices \(a\), \(b\), \(u\), \(v\), the unit skew flow of the oriented edge \((a, b)\) at the ordered pair \((u, v)\) is the integer \([u = a \text{ and } v = b] - [u = b \text{ and } v = a]\), where \([P]\) is \(1\) if \(P\) holds and \(0\) otherwise.

def localDelta {V : Type*} [DecidableEq V]
    (first second source target : V) : Int :=
  (if source = first ∧ target = second then 1 else 0) -
    if source = second ∧ target = first then 1 else 0

Used by 3

Used byAugmentation within residual capacities preserves feasibility · Edge delta of a path · Augmenting along a path changes the flow value by the amount

DefinitionEdge delta of a path#✓fully proved

For a list \(P\) of elements of a set \(V\) and elements \(u, v\) of \(V\), the edge delta of \(P\) at \((u, v)\) is the integer obtained as the number of consecutive pairs of \(P\) equal to \((u, v)\) minus the number of consecutive pairs of \(P\) equal to \((v, u)\), counted with multiplicity. It is \(0\) when \(P\) has fewer than two elements.

def edgeDelta {V : Type*} [DecidableEq V] : List V → V → V → Int
  | [] | [_] => fun _ _ => 0
  | first :: second :: rest => fun source target =>
      localDelta first second source target +
        edgeDelta (second :: rest) source target

Uses 1 · Used by 3

Statement usesUnit skew flow along an oriented edge

Used byAugmenting a flow along a path · Augmentation within residual capacities preserves feasibility · Augmenting along a path changes the flow value by the amount

DefinitionAugmenting a flow along a path#✓fully proved

Given an integer flow matrix \(f\) on the vertices \(\{0, \dots, n-1\}\), a list of vertices \(P\) and an integer \(a\), the augmentation of \(f\) along \(P\) by \(a\) is the matrix whose entry at \((u, v)\) is \(f(u, v) + a \cdot d\), where \(d\) is the number of consecutive pairs of \(P\) equal to \((u, v)\) minus the number of consecutive pairs of \(P\) equal to \((v, u)\), counted with multiplicity.

def augment {n : Nat} (flow : Flow n) (path : List (Fin n))
    (amount : Int) : Flow n :=
  fun source target => flow source target + amount * edgeDelta path source target

Uses 2 · Used by 10

Statement usesFlow · Edge delta of a path

Used byAugmentation within residual capacities preserves feasibility · Bottleneck augmentation preserves feasibility · The Edmonds–Karp flow is feasible · No augmenting path remains after Edmonds–Karp · Augmenting along a path changes the flow value by the amount · The augmentation loop never decreases the flow value · One augmentation step keeps or strictly raises the flow value · Augmenting-path iteration with fuel · The iteration stops when there is no augmenting path · One augmenting-path step

TheoremAugmenting paths have positive bottleneck#✓fully proved

Let \(c\) be a capacity matrix with natural-number entries and \(f\) any integer matrix (the flow) on the vertices \(0, \dots, n - 1\), and let \(s \ne t\) be vertices. If \(p\) is a duplicate-free path from \(s\) to \(t\) in the residual graph of \(c\) and \(f\), then the bottleneck of \(p\), the minimum of \(c(u, v) - f(u, v)\) over consecutive vertices \(u, v\) of \(p\), is positive.

theorem pathBottleneck_pos {n : Nat}
    (capacity : Fin n → Fin n → Nat) (flow : Flow n)
    {source sink : Fin n} (source_ne_sink : source ≠ sink)
    {path : List (Fin n)}
    (pathSpec : IsPath (residualGraph capacity flow) source sink path) :
    0 < pathBottleneck capacity flow path

Uses 9 · Used by 3

Statement usesFlow · Directed path · Bottleneck of a path · Residual graph

Proof usesDirected adjacency graph · Edge of a directed adjacency graph · Edges of a path · Residual capacity · Edges of the residual graph

Used byNo augmenting path remains after Edmonds–Karp · The augmentation loop never decreases the flow value · One augmentation step keeps or strictly raises the flow value

TheoremAugmentation within residual capacities preserves feasibility#✓fully proved

Let \(c\) be a capacity matrix with natural-number entries on the vertices \(\{0, \dots, n-1\}\), let \(s\) and \(t\) be vertices, and let \(f\) be a flow that is feasible for \(c\), \(s\), \(t\). Let \(P = (v_0, \dots, v_k)\) be a nonempty list of pairwise distinct vertices with \(v_0 = s\) and \(v_k = t\), and let \(a\) be an integer with \(0 \le a\) and \(a \le c(v_i, v_{i+1}) - f(v_i, v_{i+1})\) for every \(i < k\). Then the augmentation of \(f\) along \(P\) by \(a\) is feasible for \(c\), \(s\), \(t\).

theorem augment_feasible {n : Nat}
    (capacity : Fin n → Fin n → Nat) (source sink : Fin n)
    (flow : Flow n) (feasible : IsFeasible capacity source sink flow)
    (path : List (Fin n)) (pathSpec : path.Nodup) (amount : Int)
    (amount_nonneg : 0 ≤ amount)
    (amount_le_residual : ∀ u v, (u, v) ∈ pathEdges path →
      amount ≤ residualAmount capacity flow u v)
    (chain : path.IsChainFromTo (fun _ _ => True) source sink) :
    IsFeasible capacity source sink (augment flow path amount)

Uses 8 · Used by 1

Statement usesFlow · Feasible flow · Augmenting a flow along a path · Edges of a path · Residual capacity

Proof usesEdge delta of a path · Flow value · Unit skew flow along an oriented edge

Used byBottleneck augmentation preserves feasibility

TheoremAugmenting along a path changes the flow value by the amount#✓fully proved

Let \(s \ne t\) be vertices, \(f\) a flow, \(a\) an integer, and \(p\) a nonempty list of vertices whose first entry is \(s\) and whose last entry is \(t\). Then the net flow leaving \(s\) under the flow obtained by augmenting \(f\) along \(p\) by \(a\) equals the net flow leaving \(s\) under \(f\), plus \(a\).

No feasibility of \(f\), no edge condition on consecutive entries of \(p\), and no duplicate-freeness of \(p\) is needed.

theorem flowValue_augment {n : Nat} (source sink : Fin n)
    (source_ne_sink : source ≠ sink) (flow : Flow n)
    (path : List (Fin n)) (amount : Int)
    (chain : path.IsChainFromTo (fun _ _ => True) source sink) :
    flowValue source (augment flow path amount) = flowValue source flow + amount

Uses 5 · Used by 3

Statement usesFlow · Augmenting a flow along a path · Flow value

Proof usesEdge delta of a path · Unit skew flow along an oriented edge

Used byNo augmenting path remains after Edmonds–Karp · The augmentation loop never decreases the flow value · One augmentation step keeps or strictly raises the flow value

TheoremBottleneck augmentation preserves feasibility#✓fully proved

Let \(c\) be a capacity matrix with natural-number entries on the vertices \(\{0, \dots, n-1\}\), let \(s\) and \(t\) be vertices, and let \(f\) be a flow that is feasible for \(c\), \(s\), \(t\). If \(P\) is a path from \(s\) to \(t\) in the residual graph of \(f\), that is, a nonempty list of pairwise distinct vertices starting at \(s\) and ending at \(t\) whose consecutive pairs are residual edges, then the augmentation of \(f\) along \(P\) by the bottleneck of \(P\) is again feasible for \(c\), \(s\), \(t\).

theorem augment_pathBottleneck_feasible {n : Nat}
    (capacity : Fin n → Fin n → Nat) (source sink : Fin n)
    (flow : Flow n) (feasible : IsFeasible capacity source sink flow)
    (path : List (Fin n))
    (pathSpec : IsPath (residualGraph capacity flow) source sink path) :
    IsFeasible capacity source sink
      (augment flow path (pathBottleneck capacity flow path))

Uses 12 · Used by 1

Statement usesFlow · Feasible flow · Directed path · Augmenting a flow along a path · Bottleneck of a path · Residual graph

Proof usesDirected adjacency graph · Edge of a directed adjacency graph · Augmentation within residual capacities preserves feasibility · Edges of a path · Residual capacity · Edges of the residual graph

Used byThe Edmonds–Karp flow is feasible

DefinitionOne augmenting-path step#✓fully proved

Let \(c\) be a capacity matrix with natural-number entries on the vertices \(\{0, \dots, n - 1\}\), let \(s\) be a source and \(t\) a sink, and let \(f\) be a flow (an integer-valued matrix on pairs of vertices). Run the breadth-first shortest-path search from \(s\) to \(t\) in the residual graph of \(f\) with respect to \(c\). If it finds no path, the step returns \(f\). If it returns a path \(P\), let \(b\) be the bottleneck of \(P\), the least residual capacity \(c(u, v) - f(u, v)\) over the edges \((u, v)\) of \(P\) (and \(b = 0\) if \(P\) has no edges); the step returns \(f\) augmented along \(P\) by \(b\), that is, \(b\) is added to \(f(u, v)\) and subtracted from \(f(v, u)\) for each edge \((u, v)\) of \(P\).

def step {n : Nat} (capacity : Fin n → Fin n → Nat)
    (source sink : Fin n) (flow : Flow n) : Flow n :=
  match shortestPath (residualGraph capacity flow) source sink with
  | none => flow
  | some path => augment flow path (pathBottleneck capacity flow path)

Uses 5 · Used by 1

Statement usesFlow · Augmenting a flow along a path · Bottleneck of a path · Residual graph · Shortest path via breadth-first search

Used byOne augmentation step keeps or strictly raises the flow value

TheoremOne augmentation step keeps or strictly raises the flow value#✓fully proved

Let \(c\) be a capacity function and \(s \ne t\) vertices. For every flow \(f\), the flow obtained from \(f\) by one step of bottleneck augmentation either has the same net flow leaving \(s\) as \(f\), or a strictly larger one.

theorem flowValue_step {n : Nat} (capacity : Fin n → Fin n → Nat)
    (source sink : Fin n) (source_ne_sink : source ≠ sink) (flow : Flow n) :
    flowValue source (step capacity source sink flow) = flowValue source flow ∨
      flowValue source flow < flowValue source (step capacity source sink flow)

Uses 14

Statement usesFlow · Flow value · One augmenting-path step

Proof usesResult of breadth-first search · Breadth-first search · Edge of a directed adjacency graph · Directed path · Augmenting a flow along a path · Augmenting along a path changes the flow value by the amount · Bottleneck of a path · Augmenting paths have positive bottleneck · Residual graph · Shortest path via breadth-first search · Soundness of the shortest-path search

DefinitionAugmenting-path iteration with fuel#✓fully proved

Let \(c\) be a capacity matrix with natural-number entries on the vertices \(\{0, \dots, n - 1\}\), let \(s\) be a source and \(t\) a sink, let \(k\) be a fuel bound and let \(f\) be a flow (an integer-valued matrix on pairs of vertices). The iteration returns \(f\) if \(k = 0\) or \(s = t\). Otherwise it runs the breadth-first shortest-path search from \(s\) to \(t\) in the residual graph of \(f\) with respect to \(c\). If the search finds no path, the iteration returns \(f\). If it returns a path \(P\), let \(b\) be the bottleneck of \(P\), the least residual capacity \(c(u, v) - f(u, v)\) over the edges \((u, v)\) of \(P\); the iteration augments \(f\) along \(P\) by \(b\), adding \(b\) to \(f(u, v)\) and subtracting \(b\) from \(f(v, u)\) for each edge \((u, v)\) of \(P\), and continues from the augmented flow with fuel \(k - 1\).

def run {n : Nat} (capacity : Fin n → Fin n → Nat)
    (source sink : Fin n) : Nat → Flow n → Flow n
  | 0, flow => flow
  | fuel + 1, flow =>
      if source = sink then flow
      else
        match shortestPath (residualGraph capacity flow) source sink with
        | none => flow
        | some path => run capacity source sink fuel
            (augment flow path (pathBottleneck capacity flow path))

Uses 5 · Used by 5

Statement usesFlow · Augmenting a flow along a path · Bottleneck of a path · Residual graph · Shortest path via breadth-first search

Used byEdmonds–Karp maximum flow · The Edmonds–Karp flow is feasible · No augmenting path remains after Edmonds–Karp · The augmentation loop never decreases the flow value · The iteration stops when there is no augmenting path

TheoremThe augmentation loop never decreases the flow value#✓fully proved

Let \(c\) be a capacity function and \(s \ne t\) vertices. For every flow \(f\) and every natural number \(k\), the net flow leaving \(s\) after running at most \(k\) rounds of bottleneck augmentation from \(f\) is at least the net flow leaving \(s\) under \(f\).

theorem flowValue_le_run {n : Nat} (capacity : Fin n → Fin n → Nat)
    (source sink : Fin n) (source_ne_sink : source ≠ sink)
    (fuel : Nat) (flow : Flow n) :
    flowValue source flow ≤ flowValue source (run capacity source sink fuel flow)

Uses 14

Statement usesFlow · Flow value · Augmenting-path iteration with fuel

Proof usesResult of breadth-first search · Breadth-first search · Edge of a directed adjacency graph · Directed path · Augmenting a flow along a path · Augmenting along a path changes the flow value by the amount · Bottleneck of a path · Augmenting paths have positive bottleneck · Residual graph · Shortest path via breadth-first search · Soundness of the shortest-path search

DefinitionSource capacity#✓fully proved

For a capacity matrix \(c\) with natural-number entries on the vertices \(\{0, \dots, n - 1\}\) and a source \(s\), the source capacity is the total capacity leaving \(s\), namely \(\sum_{v} c(s, v)\), where \(v\) ranges over all vertices, including \(s\) itself.

def sourceCapacity {n : Nat} (capacity : Fin n → Fin n → Nat)
    (source : Fin n) : Nat :=
  ∑ target, capacity source target

Used by 4

Used byEdmonds–Karp maximum flow · The Edmonds–Karp flow is feasible · No augmenting path remains after Edmonds–Karp · The flow value is at most the source capacity

DefinitionEdmonds–Karp maximum flow#✓fully proved

Let \(c\) be a capacity function assigning a natural number \(c(u, v)\) to each ordered pair of vertices, and let \(s\) and \(t\) be vertices. If \(s = t\), the Edmonds–Karp flow is the zero flow. Otherwise it is the result of running at most \(C + 1\) rounds of bottleneck augmentation from the zero flow, where \(C = \sum_v c(s, v)\) is the total capacity leaving \(s\): each round looks for a shortest path from \(s\) to \(t\) in the residual graph, stops if there is none, and otherwise augments the flow along that path by its bottleneck.

def edmondsKarp {n : Nat} (capacity : Fin n → Fin n → Nat)
    (source sink : Fin n) : Flow n :=
  if source = sink then zeroFlow n
  else run capacity source sink (sourceCapacity capacity source + 1) (zeroFlow n)

Uses 4 · Used by 8

Statement usesFlow · Augmenting-path iteration with fuel · Source capacity · Zero flow

Used byNo \(s\)-\(t\) cut is smaller than the Edmonds–Karp residual cut · The Edmonds–Karp flow is feasible · Edmonds-Karp computes a maximum flow and a minimum cut · Maximality of the Edmonds–Karp flow · The Edmonds–Karp flow value equals its residual cut capacity · No augmenting path remains after Edmonds–Karp · Integral flow theorem · The Edmonds-Karp residual cut separates source and sink

TheoremThe Edmonds–Karp flow is feasible#✓fully proved

For every capacity matrix \(c\) with natural-number entries on the vertices \(\{0, \dots, n-1\}\) and all vertices \(s\) and \(t\), the flow \(f\) returned by the Edmonds–Karp algorithm on \(c\), \(s\), \(t\) is feasible for \(c\), \(s\), \(t\): it is skew-symmetric, satisfies \(f(u, v) \le c(u, v)\) for all vertices \(u, v\), and has zero net outflow at every vertex other than \(s\) and \(t\).

theorem edmondsKarp_feasible {n : Nat}
    (capacity : Fin n → Fin n → Nat) (source sink : Fin n) :
    IsFeasible capacity source sink (edmondsKarp capacity source sink)

Uses 16 · Used by 3

Statement usesFeasible flow · Edmonds–Karp maximum flow

Proof usesResult of breadth-first search · Breadth-first search · Flow · Directed path · Augmenting a flow along a path · Bottleneck augmentation preserves feasibility · Bottleneck of a path · Residual graph · Augmenting-path iteration with fuel · Shortest path via breadth-first search · Soundness of the shortest-path search · Source capacity · Zero flow · The zero flow is feasible

Used byEdmonds-Karp computes a maximum flow and a minimum cut · The Edmonds–Karp flow value equals its residual cut capacity · No augmenting path remains after Edmonds–Karp

TheoremThe iteration stops when there is no augmenting path#✓fully proved

Let \(c\) be a capacity matrix with natural-number entries on the vertices \(\{0, \dots, n - 1\}\), let \(s\) and \(t\) be vertices, and let \(f\) be a flow (an integer-valued matrix on pairs of vertices). If the breadth-first shortest-path search finds no path from \(s\) to \(t\) in the residual graph of \(f\) with respect to \(c\), then for every fuel bound \(k\), the augmenting-path iteration started at \(f\) with fuel \(k\) returns \(f\).

theorem run_eq_of_no_path {n : Nat}
    (capacity : Fin n → Fin n → Nat) (source sink : Fin n)
    (flow : Flow n)
    (noPath : shortestPath (residualGraph capacity flow) source sink = none) :
    ∀ fuel, run capacity source sink fuel flow = flow

Uses 6

Statement usesFlow · Residual graph · Augmenting-path iteration with fuel · Shortest path via breadth-first search

Proof usesAugmenting a flow along a path · Bottleneck of a path

TheoremThe flow value is at most the source capacity#✓fully proved

Let \(c\) be a capacity function, \(s\) and \(t\) vertices, and \(f\) a flow that is feasible for \(c\), \(s\) and \(t\). Then the net flow leaving \(s\) under \(f\) is at most \(\sum_v c(s, v)\), the total capacity leaving \(s\).

theorem flowValue_le_sourceCapacity {n : Nat}
    {capacity : Fin n → Fin n → Nat} {source sink : Fin n}
    {flow : Flow n} (feasible : IsFeasible capacity source sink flow) :
    flowValue source flow ≤ (sourceCapacity capacity source : Int)

Uses 4 · Used by 1

Statement usesFlow · Feasible flow · Flow value · Source capacity

Used byNo augmenting path remains after Edmonds–Karp

TheoremNo augmenting path remains after Edmonds–Karp#✓fully proved

Let \(c\) be a capacity matrix with natural-number entries on the vertices \(\{0, \dots, n-1\}\) and let \(s\) and \(t\) be distinct vertices. Then \(t\) is not reachable from \(s\) in the residual graph of the flow returned by the Edmonds–Karp algorithm on \(c\), \(s\), \(t\).

theorem edmondsKarp_no_augmenting_path {n : Nat}
    (capacity : Fin n → Fin n → Nat) {source sink : Fin n}
    (source_ne_sink : source ≠ sink) :
    ¬ (residualGraph capacity (edmondsKarp capacity source sink)).Reachable source sink

Uses 23 · Used by 3

Statement usesReachability in a directed graph · Edmonds–Karp maximum flow · Residual graph

Proof usesResult of breadth-first search · Breadth-first search · Directed adjacency graph · Edge of a directed adjacency graph · Flow · Feasible flow · Directed path · Augmenting a flow along a path · The Edmonds–Karp flow is feasible · Flow value · Augmenting along a path changes the flow value by the amount · The flow value is at most the source capacity · Bottleneck of a path · Augmenting paths have positive bottleneck · Augmenting-path iteration with fuel · Shortest path via breadth-first search · The shortest-path search fails exactly when the sink is unreachable · Soundness of the shortest-path search · Source capacity · Zero flow

Used byMaximality of the Edmonds–Karp flow · The Edmonds–Karp flow value equals its residual cut capacity · The Edmonds-Karp residual cut separates source and sink

DefinitionCut capacity#✓fully proved

For a capacity matrix \(c\) with natural-number entries on the vertices \(\{0, \dots, n-1\}\) and a set \(S\) of vertices, the capacity of the cut \(S\) is the integer \(\sum_{u \in S} \sum_{v \notin S} c(u, v)\).

def cutCapacity {n : Nat} (capacity : Fin n → Fin n → Nat)
    (cut : Finset (Fin n)) : Int :=
  ∑ u ∈ cut, ∑ v ∈ (Finset.univ : Finset (Fin n)) \ cut, (capacity u v : Int)

Used by 4

Used byEdmonds-Karp computes a maximum flow and a minimum cut · Maximality of the Edmonds–Karp flow · The Edmonds–Karp flow value equals its residual cut capacity · Weak max-flow min-cut duality

TheoremWeak max-flow min-cut duality#✓fully proved

Let \(c\) be a capacity function, \(s\) and \(t\) vertices, and \(f\) a flow that is feasible for \(c\), \(s\) and \(t\). For every set \(S\) of vertices with \(s \in S\) and \(t \notin S\), the net flow leaving \(s\) under \(f\) is at most the capacity of the cut \(S\), namely \(\sum_{u \in S} \sum_{v \notin S} c(u, v)\).

theorem flowValue_le_cutCapacity {n : Nat}
    (capacity : Fin n → Fin n → Nat) (source sink : Fin n)
    (flow : Flow n) (feasible : IsFeasible capacity source sink flow)
    (cut : Finset (Fin n)) (sourceMem : source ∈ cut) (sinkNotMem : sink ∉ cut) :
    flowValue source flow ≤ cutCapacity capacity cut

Uses 4 · Used by 1

Statement usesFlow · Feasible flow · Cut capacity · Flow value

Used byMaximality of the Edmonds–Karp flow

DefinitionResidual cut#✓fully proved

Let \(c\) be a capacity matrix assigning a natural number \(c(u, v)\) to each ordered pair of vertices among \(0, \dots, n - 1\), let \(f\) be a flow on these vertices, and let \(s\) be a vertex. The residual cut of \(c\), \(f\) and \(s\) is the set of vertices visited by breadth-first search from \(s\) in the residual graph of \(c\) and \(f\), that is, the set of vertices reachable from \(s\) in that residual graph.

def residualCut {n : Nat} (capacity : Fin n → Fin n → Nat)
    (flow : Flow n) (source : Fin n) : Finset (Fin n) :=
  (bfs (residualGraph capacity flow) source).order.toFinset

Uses 4 · Used by 6

Statement usesResult of breadth-first search · Breadth-first search · Flow · Residual graph

Used byNo \(s\)-\(t\) cut is smaller than the Edmonds–Karp residual cut · Edmonds-Karp computes a maximum flow and a minimum cut · Maximality of the Edmonds–Karp flow · The Edmonds–Karp flow value equals its residual cut capacity · Integral flow theorem · The Edmonds-Karp residual cut separates source and sink

TheoremThe Edmonds–Karp flow value equals its residual cut capacity#✓fully proved

Let \(c\) be a capacity matrix with natural-number entries on the vertices \(\{0, \dots, n-1\}\), let \(s\) and \(t\) be distinct vertices, and let \(f\) be the flow returned by the Edmonds–Karp algorithm on \(c\), \(s\), \(t\). Then the net flow of \(f\) out of \(s\) equals the capacity of the cut formed by the vertices reachable from \(s\) in the residual graph of \(f\).

theorem edmondsKarp_minCut {n : Nat}
    (capacity : Fin n → Fin n → Nat) {source sink : Fin n}
    (source_ne_sink : source ≠ sink) :
    flowValue source (edmondsKarp capacity source sink) =
      cutCapacity capacity
        (residualCut capacity (edmondsKarp capacity source sink) source)

Uses 15 · Used by 2

Statement usesCut capacity · Edmonds–Karp maximum flow · Flow value · Residual cut

Proof usesResult of breadth-first search · Breadth-first search · BFS lists exactly the reachable vertices · Edge of a directed adjacency graph · Reachability in a directed graph · Flow · Feasible flow · The Edmonds–Karp flow is feasible · No augmenting path remains after Edmonds–Karp · Residual graph · Edges of the residual graph

Used byEdmonds-Karp computes a maximum flow and a minimum cut · Maximality of the Edmonds–Karp flow

TheoremMaximality of the Edmonds–Karp flow#✓fully proved

Let \(c\) be a capacity matrix with natural-number entries on the vertices \(\{0, \dots, n-1\}\), let \(s\) and \(t\) be distinct vertices, and let \(f\) be the flow returned by the Edmonds–Karp algorithm on \(c\), \(s\), \(t\). Then every integer flow \(g\) that is feasible for \(c\), \(s\), \(t\) has value at \(s\) at most the value of \(f\) at \(s\), where the value of a flow at \(s\) is its net flow out of \(s\).

theorem edmondsKarp_maximal {n : Nat}
    (capacity : Fin n → Fin n → Nat) {source sink : Fin n}
    (source_ne_sink : source ≠ sink) (candidate : Flow n)
    (candidate_feasible : IsFeasible capacity source sink candidate) :
    flowValue source candidate ≤ flowValue source (edmondsKarp capacity source sink)

Uses 15

Statement usesFlow · Feasible flow · Edmonds–Karp maximum flow · Flow value

Proof usesResult of breadth-first search · Breadth-first search · BFS lists exactly the reachable vertices · Edge of a directed adjacency graph · Reachability in a directed graph · Cut capacity · The Edmonds–Karp flow value equals its residual cut capacity · No augmenting path remains after Edmonds–Karp · Weak max-flow min-cut duality · Residual cut · Residual graph

DefinitionReal capacities#✓fully proved

For a capacity function \(c\) on the vertices \(0, \dots, n-1\) with natural-number values, the real capacities are the same values viewed as real numbers, \((u, v) \mapsto c(u, v) \in \mathbb{R}\).

def realCap (capacity : Fin n → Fin n → ℕ) : Fin n → Fin n → ℝ := fun u v => (capacity u v : ℝ)

Used by 4

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

DefinitionArc flow of an integer flow#✓fully proved

For an integer flow matrix \(f\) on the vertices \(0, \dots, n-1\), its arc flow is the natural-number matrix whose entry at \((u, v)\) is the positive part \(\max(f(u, v), 0)\) of \(f(u, v)\).

def arcFlow (flow : Flow n) : Fin n → Fin n → ℕ := fun u v => (flow u v).toNat

Uses 1 · Used by 5

Statement usesFlow

Used byIntegral flow theorem · A skew flow is the difference of its arc flows · A feasible skew flow gives a feasible flow · Real arc flow · Net outflow in the arc representation

DefinitionReal arc flow#✓fully proved

For an integer flow matrix \(f\) on the vertices \(0, \dots, n-1\), its real arc flow is the function \((u, v) \mapsto \max(f(u, v), 0)\), the arc flow of \(f\), viewed as real numbers.

def realFlow (flow : Flow n) : Fin n → Fin n → ℝ := fun u v => (arcFlow flow u v : ℝ)

Uses 2 · Used by 5

Statement usesFlow · Arc flow of an integer flow

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 · Net outflow in the arc representation

TheoremA skew flow is the difference of its arc flows#✓fully proved

Let \(f\) be an integer flow matrix on the vertices \(0, \dots, n-1\) that is skew-symmetric, \(f(u, v) = -f(v, u)\) for all \(u, v\), and let \(a(u, v) = \max(f(u, v), 0)\) be its arc flow. Then \(f(u, v) = a(u, v) - a(v, u)\) for all vertices \(u\) and \(v\).

theorem flow_eq_arcFlow_sub {flow : Flow n} (skew : ∀ u v, flow u v = -flow v u) (u v : Fin n) :
    flow u v = (arcFlow flow u v : ℤ) - (arcFlow flow v u : ℤ)

Uses 2 · Used by 1

Statement usesFlow · Arc flow of an integer flow

Used byNet outflow in the arc representation

TheoremNet outflow in the arc representation#✓fully proved

Let \(f\) be a skew-symmetric integer flow matrix on the vertices \(0, \dots, n-1\), so \(f(u, v) = -f(v, u)\) for all \(u, v\), and let \(a(u, v) = \max(f(u, v), 0)\) be its arc flow, viewed as real numbers. Then for every vertex \(v\), \(\sum_w a(v, w) - \sum_u a(u, v) = \sum_w f(v, w)\), the net flow leaving \(v\).

theorem sum_realFlow_sub {flow : Flow n} (skew : ∀ u v, flow u v = -flow v u) (v : Fin n) :
    (∑ w, realFlow flow v w) - ∑ u, realFlow flow u v = (EdmondsKarp.flowValue v flow : ℝ)

Uses 5 · Used by 2

Statement usesFlow · Flow value · Real arc flow

Proof usesArc flow of an integer flow · A skew flow is the difference of its arc flows

Used byEdmonds-Karp computes a maximum flow and a minimum cut · A feasible skew flow gives a feasible flow

TheoremA feasible skew flow gives a feasible flow#✓fully proved

Let \(c\) be a capacity function on the vertices \(0, \dots, n-1\) with natural-number values and let \(s, t\) be vertices. If an integer flow matrix \(f\) is a feasible skew-symmetric \(s\)-\(t\) flow for \(c\), then its arc flow \((u, v) \mapsto \max(f(u, v), 0)\), viewed as a real function, is a feasible \(s\)-\(t\) flow for \(c\) viewed as real capacities.

theorem isFeasibleFlow_realFlow {capacity : Fin n → Fin n → ℕ} {source sink : Fin n}
    {flow : Flow n} (h : IsFeasible capacity source sink flow) :
    MFC.IsFeasibleFlow (realCap capacity) source sink (realFlow flow)

Uses 8 · Used by 1

Statement usesFlow · Feasible flow · Real capacities · Real arc flow · Feasible flow

Proof usesFlow value · Arc flow of an integer flow · Net outflow in the arc representation

Used byEdmonds-Karp computes a maximum flow and a minimum cut

TheoremThe Edmonds-Karp residual cut separates source and sink#✓fully proved

Let \(c\) be a capacity function on the vertices \(0, \dots, n-1\) with natural-number values and let \(s \ne t\) be vertices. The set of vertices reachable from \(s\) in the residual graph of the flow computed by the Edmonds-Karp algorithm on \(c\), \(s\), \(t\) is an \(s\)-\(t\) cut: it contains \(s\) and not \(t\).

theorem isSTCut_residualCut (capacity : Fin n → Fin n → ℕ) {source sink : Fin n}
    (hst : source ≠ sink) :
    MFC.IsSTCut source sink (residualCut capacity (edmondsKarp capacity source sink) source)

Uses 10 · Used by 1

Statement usesEdmonds–Karp maximum flow · Residual cut · Source–sink cut

Proof usesResult of breadth-first search · Breadth-first search · BFS lists exactly the reachable vertices · Edge of a directed adjacency graph · Reachability in a directed graph · No augmenting path remains after Edmonds–Karp · Residual graph

Used byEdmonds-Karp computes a maximum flow and a minimum cut

TheoremEdmonds-Karp computes a maximum flow and a minimum cut#✓fully proved

Let \(c\) be a capacity function on the vertices \(0, \dots, n-1\) with natural-number values, viewed as real capacities, and let \(s \ne t\) be vertices. Let \(f\) be the real arc flow of the flow computed by the Edmonds-Karp algorithm on \(c\), \(s\), \(t\) (its positive part, viewed as real numbers), and let \(S_0\) be the set of vertices reachable from \(s\) in the residual graph of that flow. Then \(f\) is a feasible \(s\)-\(t\) flow for \(c\); every feasible real-valued \(s\)-\(t\) flow for \(c\) has value at most the value of \(f\); the value of \(f\) is at most the capacity of every \(s\)-\(t\) cut; \(S_0\) is an \(s\)-\(t\) cut; and the value of \(f\) equals the capacity of \(S_0\).

theorem edmondsKarp_max_flow_min_cut (capacity : Fin n → Fin n → ℕ) {source sink : Fin n}
    (hst : source ≠ sink) :
    MFC.IsFeasibleFlow (realCap capacity) source sink
        (realFlow (edmondsKarp capacity source sink)) ∧
      (∀ f : Fin n → Fin n → ℝ, MFC.IsFeasibleFlow (realCap capacity) source sink f →
        MFC.flowValue source f ≤
          MFC.flowValue source (realFlow (edmondsKarp capacity source sink))) ∧
      (∀ S : Finset (Fin n), MFC.IsSTCut source sink S →
        MFC.flowValue source (realFlow (edmondsKarp capacity source sink)) ≤
          MFC.cutCapacity (realCap capacity) S) ∧
      MFC.IsSTCut source sink (residualCut capacity (edmondsKarp capacity source sink) source) ∧
      MFC.flowValue source (realFlow (edmondsKarp capacity source sink)) =
        MFC.cutCapacity (realCap capacity)
          (residualCut capacity (edmondsKarp capacity source sink) source)

Uses 18 · Used by 2

Statement usesEdmonds–Karp maximum flow · Residual cut · Real capacities · Real arc flow · Feasible flow · Source–sink cut · Cut capacity · Flow value

Proof usesFlow · Feasible flow · Cut capacity · The Edmonds–Karp flow is feasible · The Edmonds–Karp flow value equals its residual cut capacity · Flow value · A feasible skew flow gives a feasible flow · The Edmonds-Karp residual cut separates source and sink · Net outflow in the arc representation · Weak duality for flows and cuts

Used byNo \(s\)-\(t\) cut is smaller than the Edmonds–Karp residual cut · Integral flow theorem

TheoremNo \(s\)-\(t\) cut is smaller than the Edmonds–Karp residual cut#✓fully proved

Let \(c\) be a capacity function on the vertices \(0, \dots, n-1\) with natural-number values, viewed as real capacities, and let \(s \ne t\) be vertices. Let \(S_0\) be the set of vertices reachable from \(s\) in the residual graph of the flow computed by the Edmonds–Karp algorithm on \(c\), \(s\), \(t\). Then for every \(s\)-\(t\) cut \(S\), the capacity of \(S_0\) is at most the capacity of \(S\).

theorem cutCapacity_residualCut_le (capacity : Fin n → Fin n → ℕ) {source sink : Fin n}
    (hst : source ≠ sink) {S : Finset (Fin n)} (hS : MFC.IsSTCut source sink S) :
    MFC.cutCapacity (realCap capacity)
        (residualCut capacity (edmondsKarp capacity source sink) source) ≤
      MFC.cutCapacity (realCap capacity) S

Uses 9

Statement usesEdmonds–Karp maximum flow · Residual cut · Real capacities · Source–sink cut · Cut capacity

Proof usesEdmonds-Karp computes a maximum flow and a minimum cut · Real arc flow · Feasible flow · Flow value

TheoremIntegral flow theorem#✓fully proved

Let \(c\) be a capacity function on the vertices \(0, \dots, n-1\) with natural-number values, viewed as real capacities, and let \(s \ne t\) be vertices. Then there is a natural-number valued function \(f\) on pairs of vertices which, viewed as a real function, is a feasible \(s\)-\(t\) flow for \(c\) whose value is at least the value of every feasible real-valued \(s\)-\(t\) flow for \(c\).

The proof takes \(f\) to be the arc flow of the flow computed by the Edmonds-Karp algorithm.

theorem exists_nat_max_flow (capacity : Fin n → Fin n → ℕ) {source sink : Fin n}
    (hst : source ≠ sink) :
    ∃ f : Fin n → Fin n → ℕ,
      MFC.IsFeasibleFlow (realCap capacity) source sink (fun u v => (f u v : ℝ)) ∧
      ∀ g : Fin n → Fin n → ℝ, MFC.IsFeasibleFlow (realCap capacity) source sink g →
        MFC.flowValue source g ≤ MFC.flowValue source (fun u v => (f u v : ℝ))

Uses 10

Statement usesReal capacities · Feasible flow · Flow value

Proof usesEdmonds–Karp maximum flow · Residual cut · Arc flow of an integer flow · Edmonds-Karp computes a maximum flow and a minimum cut · Real arc flow · Source–sink cut · Cut capacity

50 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.