Proofs: Almost-linear-time maximum flow algorithm
These are the human proofs of Almost-linear-time maximum flow algorithm, at full length.
The exact version of the almost-linear max flow method returns a maximum flow full
This proof shows: correctness, termination.
This proof is for the version on the algorithm page, with exact min-ratio cycles and the finish of lines L7 to L9. The step bound of the real algorithm is proved by Chen and others and is not repeated here.
Setup. Variables are the original edges with and (lower bound 0, upper bound , cost 0), the return edge with upper bound and cost , and the edges at with upper bound and cost 4. All upper bounds are integers: is a sum of halves of integers, so is an integer. Write for the vector of variable values, and call a circulation if inflow equals outflow at every vertex, including .
Claim 1 (start). After line L2, is a circulation and for every variable. Proof. After line L1 each variable is at half its bound, and is the inflow minus outflow at . The edge with value , or with value for , cancels it. At the inflow minus outflow is , as every variable adds to one head and subtracts from one tail. Every value is half of its bound, which is positive.
Claim 2 (steps). Every step of line L6 keeps a strictly interior circulation. Proof. is a cycle, so adding any multiple keeps the circulation. The room is the least distance to a bound along , and the step is at most , so every value stays strictly inside.
Claim 3 (the loop ends). Line L3 allows a fixed number of steps, and line L5 is a finite procedure: each Dinkelbach round finds a cycle with a strictly lower ratio, and a graph has finitely many simple cycles. Line L6 tries finitely many .
Claim 4 (rounding). Line L7 ends with an integral circulation within the bounds whose cost is at most the cost of . Proof. Call a variable fractional if its value is not an integer. Suppose some variable at vertex is fractional. The net flow at is 0, an integer, and the integral variables contribute an integer, so the fractional ones at sum (with signs) to an integer, which is impossible with only one of them. So in the multigraph of fractional variables every vertex with an edge has degree at least 2, and it contains a cycle . Pushing around in one direction keeps the circulation and changes the cost by times the signed cost of ; line L7 picks the direction where this is at most 0. It takes as the least distance to the next integer in the direction of motion, so each value stays between two consecutive integers it lay between, hence within its integer bounds, and at least one variable becomes integral. Integral variables are not in , so they stay integral, and there are finitely many variables, so line L7 ends.
Claim 5 (removing ). Line L8 ends with value 0 on all edges at , an integral circulation within bounds, and a cost not higher. Proof. If an edge out of has positive value, let be the set of vertices reachable from by edges of positive value. If no edge of positive value entered from , then the set would receive positive flow from and, since all edges of positive value leaving it stay in , send none to ; the total inflow minus outflow over would be positive, which contradicts conservation. So the search finds a cycle through of positive values. Subtracting its least value keeps an integral circulation within bounds and sets one value to 0; the cost changes by minus the cost of the cycle, which uses two edges at (cost 8) and at most one return edge (cost ), so it falls. Each round makes one more value 0 and never raises one, so line L8 ends. If no edge leaves with positive value, conservation at shows that none enters it either.
Claim 6 (output). After line L8, the values on the original edges form an integral s-t flow within capacities. Conservation holds at every vertex other than and , since the only other variables there, edges at , are 0, and the return edge touches only and . Dropped edges (capacity 0 and self-loops) get flow 0, which is feasible. Line L9 runs Ford-Fulkerson with breadth-first paths from ; each augmentation raises the integer value by at least 1 and the value is at most , so it ends, and when no augmenting path is left the set reachable from in the residual graph is a cut whose capacity equals the flow value, so is a maximum flow.
Claim 7 (when the interior phase suffices). Let be the least cost of a circulation of the extended instance. Integral circulations of the original edges plus the return edge with cost are s-t flows of value , so ; and any circulation decomposes into cycles, those through cost at least , so , an integer. If the interior phase ends with , the rounded circulation of Claim 4 is integral, its cost is an integer at least and less than , so it equals . An optimal circulation with positive value at could drop a cycle through and lower the cost, by Claim 5, so its values at are 0 and line L8 does nothing. Its return edge carries , so line L9 finds no augmenting path.
By Claims 1 to 6 the algorithm ends and returns an integral maximum flow.