Hopcroft-Karp
Abstract view
Algorithmic problem: Cardinality-maximal matching in bipartite graphs.
Type of algorithm: loop.
Auxiliary data structures: a set [math]\displaystyle{ S }[/math] of BFS runs as iterators (cf. the corresponding remark). The modification to find augmenting paths is applied.
Invariant:
- [math]\displaystyle{ M }[/math] is a matching in [math]\displaystyle{ G }[/math].
Variant: The shortest length of an augmenting path in terms of the number of edges is increased.
Break condition: [math]\displaystyle{ S=\emptyset }[/math].
Induction basis
Abstract view:
- Start with an arbitrary matching, for example, the empty matching.
- Create and initialize one BFS run for each exposed node.
Induction step
Abstract view: In the [math]\displaystyle{ i }[/math]-th iteration:
- Process all nodes of distance [math]\displaystyle{ i-1 }[/math] in the queues of all BFS runs.
- For each BFS run: If it had no nodes to process in step 1, remove it from [math]\displaystyle{ S }[/math].
- While there are two BFS runs in [math]\displaystyle{ S }[/math] that have seen the same edge:
- Choose two such BFS runs and such an edge [math]\displaystyle{ \{v,w\} }[/math], say.
- Augment [math]\displaystyle{ M }[/math] along the concatenation of the paths in the arborescences of these two BFS runs from the start nodes to [math]\displaystyle{ v }[/math] and [math]\displaystyle{ w }[/math], respectively, and of [math]\displaystyle{ \{v,w\} }[/math].
- Remove these two BFS runs from the set of all BFS runs.
Proof: The variant is obviously maintained. To prove the variant, first note