25.1. Maximum bipartite matching revisited

This section develops the native fourth-edition matching interface of CLRS §25.1 on top of the flow reduction of §26.3 (CLRS.­Chapter26.­maxMatching_eq_maxFlow_value). The flow development proves that a maximum matching can be computed; this section supplies the combinatorial characterisation of when a matching is maximum: Berge's augmenting-path lemma.

Main results:

• Matching.matchedLeft / Matching.matchedRight: matched endpoint sets

• Matching.IsMaximum: a matching no other matching exceeds in size

• IsAugmentingPath: alternating paths with unmatched endpoints

• Matching.exists_augment: an augmenting path yields a matching that is larger by one

• augmentingPath_of_hasAugmentingPath: a residual augmenting path in the §26.3 flow network induces an augmenting path in the graph

• berge_maximum_iff_no_augmentingPath (Berge's lemma): a matching is maximum iff it admits no augmenting path

• flowMethod_finds_maximum_matching: a maximum matching exists and is certified by the flow method

Current gaps:

• The O(V · E) execution-cost refinement of the flow method is an optional low-level refinement and is not stated here.

Notation conventions used in this section:

• G : bipartite graph (reused from §26.3)

• M : matching (reused from §26.3)

• p : vertex list representing an alternating path

Implementation details

The section is split into the following sub-modules:

• Matching API Extensions

• Alternating Paths

• Simple-Path Extraction

• Matching Flow Residuals

• Residual Reachability Translation

• Berge's Lemma and the Flow Method