12.22 Correctness Proofs

Problem

Flow algorithms are easy to implement incorrectly because their state changes over time.

Residual capacities change. Reverse edges appear. Flow may be pushed forward, canceled backward, or rerouted through a different path. A program can return a plausible number while violating conservation, exceeding capacity, or stopping too early.

A correctness proof gives you a disciplined way to reason about the algorithm:

What is preserved after every update?
Why does the algorithm terminate?
Why is the final answer optimal?

For network flow, most correctness proofs are built from a small set of reusable invariants.

Solution

Prove flow algorithms in three layers:

Feasibility: every intermediate or final flow satisfies the required constraints.
Progress: each algorithm step improves or advances the computation.
Optimality: when the algorithm stops, no better solution exists.

For augmenting-path algorithms, the final optimality argument usually comes from the max-flow min-cut theorem.

For push-relabel, the proof uses preflow invariants, height labels, and the absence of active vertices.

Feasibility Invariants

A valid flow must satisfy capacity constraints:

0 ≤ f(u, v) ≤ c(u, v)

and conservation constraints:

incoming(v) = outgoing(v)

for every internal vertex.

Augmenting-path algorithms preserve both.

When you augment by δ along a residual path, δ is chosen as the minimum residual capacity on that path. Therefore no edge exceeds capacity. Reverse edges subtract flow only where positive flow already exists, so no original edge becomes negative.

At every internal vertex on the path, one edge gains incoming flow and one edge gains outgoing flow. Conservation remains balanced.

Residual Capacity Invariant

For every original edge:

u -> v

the residual graph represents two possible actions.

Forward residual capacity:

c(u, v) - f(u, v)

Reverse residual capacity:

f(u, v)

The invariant is:

forward residual + current flow = original capacity
reverse residual = current flow

Every update must preserve this relationship.

This invariant is the core implementation check for Ford-Fulkerson, Edmonds-Karp, and Dinic.

Augmentation Lemma

If there is an s-t path in the residual graph, the current flow can be improved.

Let P be such a path.

Let:

δ = minimum residual capacity on P

Since every residual edge on P has positive capacity:

δ > 0

Pushing δ along the path produces a feasible flow with value:

old value + δ

Therefore the old flow was not maximum.

This lemma explains why algorithms keep searching residual graphs.

No-Augmenting-Path Lemma

If there is no path from s to t in the residual graph, the current flow is maximum.

Proof outline:

Let A be the set of vertices reachable from s in the residual graph.
Since t is unreachable, t ∉ A.
Let B = V - A.
Every original edge from A to B is saturated.
Every original edge from B to A carries zero flow.
Therefore flow value equals capacity of cut (A, B).
Since every flow is at most every cut, the current flow is maximum.

This is the standard proof of Ford-Fulkerson correctness.

Ford-Fulkerson Correctness

Ford-Fulkerson starts with zero flow.

Zero flow is feasible.

Each iteration finds an augmenting path and augments along it.

By the augmentation lemma:

feasibility is preserved
flow value increases

When no augmenting path remains, the no-augmenting-path lemma proves optimality.

For integer capacities, termination follows because each augmentation increases the flow by at least one unit and the maximum possible flow is finite.

Edmonds-Karp Correctness

Edmonds-Karp uses the same correctness proof as Ford-Fulkerson.

The only difference is path selection:

choose shortest residual path by BFS

This affects running time, not correctness.

The correctness proof remains:

Each BFS path is an augmenting path.
Each augmentation preserves feasibility.
If BFS cannot reach the sink, no augmenting path exists.
No augmenting path implies maximum flow.

The additional Edmonds-Karp proof concerns complexity: shortest-path distances in the residual graph never decrease, and each edge becomes critical only O(V) times.

Dinic Correctness

Dinic also relies on augmenting paths, but it processes many shortest paths per phase.

A Dinic phase builds a level graph and computes a blocking flow.

Correctness follows from two facts.

First, every DFS augmentation in the level graph is still an augmentation in the residual graph, so feasibility is preserved.

Second, a blocking flow eliminates all shortest augmenting paths of the current length. After the phase, any remaining augmenting path must be longer.

When the BFS phase can no longer reach the sink, no residual augmenting path exists, so the current flow is maximum.

Blocking Flow Lemma

A blocking flow in a level graph saturates at least one edge on every source-to-sink path in that level graph.

Therefore, after applying the blocking flow, no path remains from s to t using only the current level edges.

Since all shortest residual paths are represented in the level graph, all shortest augmenting paths are eliminated.

This is the reason Dinic can make more progress per BFS phase than Edmonds-Karp.

Push-Relabel Correctness

Push-relabel uses a different proof structure because it does not maintain an ordinary feasible flow during execution.

It maintains a preflow.

A preflow satisfies:

0 ≤ f(u, v) ≤ c(u, v)

but allows internal vertices to have excess:

incoming(v) ≥ outgoing(v)

The algorithm terminates when no internal vertex has positive excess.

At that point the preflow becomes a valid flow.

Height Invariant

Push-relabel assigns a height h(v) to each vertex.

The key invariant is:

if residual edge u -> v exists,
then h(u) ≤ h(v) + 1

A push is allowed only on an admissible edge:

h(u) = h(v) + 1

Relabeling restores the possibility of admissible edges when a vertex has excess but cannot push.

The height labels prevent flow from cycling indefinitely without progress.

Push Operation Proof

A push sends:

δ = min(excess(u), residual(u, v))

along an admissible edge.

This preserves capacity because δ does not exceed residual capacity.

It preserves the preflow condition because it reduces excess at u and increases excess at v.

The operation is local, but the global preflow invariant remains valid.

Relabel Operation Proof

A relabel occurs when vertex u has excess but no admissible outgoing residual edge.

Set:

h(u) = 1 + min h(v)

over residual neighbors v.

This creates at least one admissible edge.

Heights only increase.

Since heights are bounded in the standard proof, only finitely many relabels occur.

Optimality for Push-Relabel

At termination, there are no active vertices.

So every internal vertex has zero excess.

The preflow is now a feasible flow.

The height invariant implies there is no residual path from s to t. If such a path existed, heights would have to decrease by at most one per edge from h(s) = V down to h(t) = 0, contradicting the structure of reachable residual paths.

Therefore no augmenting path exists.

By the max-flow min-cut theorem, the resulting flow is maximum.

Matching Correctness

For bipartite matching, the proof usually uses augmenting paths.

A matching is maximum if and only if no augmenting path exists.

Why?

If an augmenting path exists, flipping it increases the matching size by one.

If the matching is not maximum, the symmetric difference between the current matching and a larger matching contains an augmenting path.

This theorem underlies both simple augmenting-path matching algorithms and Hopcroft-Karp.

Hopcroft-Karp Correctness

Hopcroft-Karp repeats phases.

Each BFS phase finds the length of the shortest augmenting paths.

Each DFS phase flips a maximal set of vertex-disjoint shortest augmenting paths.

Every successful DFS increases the matching size by one.

When BFS finds no augmenting path, the matching is maximum.

The performance proof comes from showing that the number of phases is O(√V).

Min-Cost Flow Correctness

Minimum-cost flow has two dimensions:

feasibility of flow
optimality of cost

For successive shortest path algorithms, each augmentation sends flow along the cheapest residual path.

Reverse edges with negative costs allow the algorithm to undo expensive earlier choices.

With potentials, reduced costs preserve shortest-path order while allowing Dijkstra to run on nonnegative edge weights.

A standard optimality condition is:

No negative-cost cycle exists in the residual graph.

If the residual graph has no negative-cost cycle, the current flow has minimum cost for its value.

Lower-Bound Correctness

Lower-bound transformations are proven by a bijection.

Every feasible original flow corresponds to a feasible transformed flow:

f_extra(u, v) = f_original(u, v) - lower(u, v)

Every feasible transformed flow corresponds to an original flow:

f_original(u, v) = lower(u, v) + f_extra(u, v)

The balance constraints ensure conservation is restored.

Therefore the transformed max-flow feasibility test is correct.

Project Selection Correctness

Project selection uses min cut.

Let:

P = sum of all positive values

For any dependency-closed selection:

cut capacity = P - selection value

Dependency edges with infinite capacity forbid invalid selections.

Thus minimizing cut capacity maximizes selected value.

The source side of the minimum cut gives the optimal project set.

Common Proof Mistakes

Proving Only Progress

Showing that the algorithm improves the solution is not enough. You must also prove that stopping means optimality.

Ignoring Reverse Edges

Most flow correctness arguments depend on reverse residual edges.

Mixing Original and Residual Graphs

Cuts are evaluated on original capacities. Reachability is computed in the residual graph.

Forgetting Integrality

For matching and disjoint paths, unit capacities plus integral max-flow algorithms ensure integral solutions.

Treating Modeling Reductions as Obvious

Every reduction needs two directions: any original solution maps to a flow solution, and any flow solution maps back to a valid original solution.

Takeaway

Correctness proofs for flow algorithms rely on a small set of reusable ideas: feasibility invariants, residual capacity invariants, augmenting paths, cuts, and dual certificates.

For algorithms, prove that every update preserves the required invariants and that termination implies no better solution exists. For reductions, prove that solutions map correctly in both directions.