Kuhn's Algorithm
Lax117284.BipartiteKuhn · concepts/Lax117284/BipartiteKuhn.lean · lax-117284
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
Kuhn's algorithm builds a matching of a bipartite graph one left vertex at a time. To place a left vertex it searches for an augmenting path: among the neighbours of not yet visited on this search, it takes one that is either free, in which case takes it, or held by some left vertex , in which case is displaced and re-placed by the same search, among the neighbours not yet visited; if can be re-placed, takes the neighbour, and otherwise the next neighbour is tried. A left vertex whose search fails stays unmatched, and the algorithm goes on to the next left vertex. The output is the matching after every left vertex has been tried.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Data.Fintype.Card |
| 2 | import Mathlib.Data.Finset.Sort |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Kuhn's Algorithm |
| 7 | type: definition |
| 8 | --- |
| 9 | Kuhn's algorithm builds a matching of a bipartite graph one left vertex at a time. To place a |
| 10 | left vertex it searches for an *augmenting path*: among the neighbours of not yet |
| 11 | visited on this search, it takes one that is either free, in which case takes it, or held by |
| 12 | some left vertex , in which case is displaced and re-placed by the same search, among |
| 13 | the neighbours not yet visited; if can be re-placed, takes the neighbour, and otherwise |
| 14 | the next neighbour is tried. A left vertex whose search fails stays unmatched, and the algorithm |
| 15 | goes on to the next left vertex. The output is the matching after every left vertex has been |
| 16 | tried. |
| 17 | |
| 18 | # Formalization Notes |
| 19 | |
| 20 | The graph is a relation `adj : L → R → Prop` between the left and the right vertices, both finite |
| 21 | types; the bipartite graph split at `n` of this submission gives such a relation between |
| 22 | `Fin n` and `Fin (V - n)`. A matching is kept as `μ : R → Option L`, the left vertex each right |
| 23 | vertex currently holds, which is the form the machine keeps it in. |
| 24 | |
| 25 | `tryAugment` is the search from one left vertex. It is written as a recursion on a fuel, spent |
| 26 | once per displaced left vertex; the number of right vertices plus one is always enough, as each |
| 27 | descent visits a fresh right vertex. `step` tries one candidate neighbour and passes a success |
| 28 | through unchanged, so that the fold over the candidates stops at the first success. `runAll` |
| 29 | tries every left vertex in turn from an empty visited set, keeping the matching it has when a |
| 30 | search fails. The machine implements the recursion with an explicit stack of frames, one per |
| 31 | displaced vertex, and tries left vertices and neighbours in the order of the word; the order is |
| 32 | immaterial to what is proved about the result. |
| 33 | -/ |
| 34 | |
| 35 | namespace Lax117284.BipartiteKuhn |
| 36 | |
| 37 | variable {L R : Type*} [Fintype L] [DecidableEq L] [Fintype R] [DecidableEq R] |
| 38 | |
| 39 | /-- The neighbours of a left vertex. -/ |
| 40 | noncomputable def nbrs (adj : L → R → Prop) [DecidableRel adj] (l : L) : Finset R := |
| 41 | Finset.univ.filter fun r => adj l r |
| 42 | |
| 43 | /-- A matching respects the graph: every right vertex's match is one of its neighbours. -/ |
| 44 | def Respects (adj : L → R → Prop) (μ : R → Option L) : Prop := |
| 45 | ∀ r l, μ r = some l → adj l r |
| 46 | |
| 47 | /-- A matching is injective: no two right vertices hold the same left vertex. -/ |
| 48 | def InjOnSupport (μ : R → Option L) : Prop := |
| 49 | ∀ r r' l, μ r = some l → μ r' = some l → r = r' |
| 50 | |
| 51 | /-- The left vertex `l` holds some right vertex. -/ |
| 52 | def Matched (μ : R → Option L) (l : L) : Prop := ∃ r, μ r = some l |
| 53 | |
| 54 | /-- The number of matched pairs. -/ |
| 55 | noncomputable def size (μ : R → Option L) : ℕ := |
| 56 | (Finset.univ.filter fun r => (μ r).isSome).card |
| 57 | |
| 58 | /-- One candidate `r` of the search for `l`: a success already found passes through; a free `r` |
| 59 | is taken; an `r` held by `l'` is taken if `l'` can be re-placed by `tryFrom`, from the matching |
| 60 | with `r` cleared and `r` marked visited. -/ |
| 61 | noncomputable def step (adj : L → R → Prop) [DecidableRel adj] (μ : R → Option L) (l : L) |
| 62 | (tryFrom : (R → Option L) → Finset R → L → Option (R → Option L)) |
| 63 | (acc : Option (R → Option L) × Finset R) (r : R) : |
| 64 | Option (R → Option L) × Finset R := |
| 65 | match acc.1 with |
| 66 | | some _ => acc |
| 67 | | none => |
| 68 | let visited' := insert r acc.2 |
| 69 | match μ r with |
| 70 | | none => (some (Function.update μ r (some l)), visited') |
| 71 | | some l' => |
| 72 | match tryFrom (Function.update μ r none) visited' l' with |
| 73 | | some μ' => (some (Function.update μ' r (some l)), visited') |
| 74 | | none => (none, visited') |
| 75 | |
| 76 | /-- **The augmenting search from `l`**: try the unvisited neighbours of `l` in turn, with `fuel` |
| 77 | descents allowed. -/ |
| 78 | noncomputable def tryAugment (adj : L → R → Prop) [DecidableRel adj] (fuel : ℕ) |
| 79 | (μ : R → Option L) (visited : Finset R) (l : L) : |
| 80 | Option (R → Option L) := |
| 81 | match fuel with |
| 82 | | 0 => none |
| 83 | | fuel + 1 => |
| 84 | (((nbrs adj l) \ visited).toList.foldl (step adj μ l (tryAugment adj fuel)) |
| 85 | (none, visited)).1 |
| 86 | |
| 87 | /-- **Try every left vertex in turn**, from an empty visited set, keeping the matching when a |
| 88 | search fails. -/ |
| 89 | noncomputable def runAll (adj : L → R → Prop) [DecidableRel adj] (fuel : ℕ) : |
| 90 | List L → (R → Option L) → (R → Option L) |
| 91 | | [], μ => μ |
| 92 | | l :: ls, μ => |
| 93 | match tryAugment adj fuel μ ∅ l with |
| 94 | | some μ' => runAll adj fuel ls μ' |
| 95 | | none => runAll adj fuel ls μ |
| 96 | |
| 97 | /-- **Kuhn's algorithm**: every left vertex, from the empty matching, with fuel enough for any |
| 98 | search. -/ |
| 99 | noncomputable def kuhn (adj : L → R → Prop) [DecidableRel adj] : R → Option L := |
| 100 | runAll adj (Fintype.card R + 1) Finset.univ.toList (fun _ => none) |
| 101 | |
| 102 | end Lax117284.BipartiteKuhn |
| 103 |
Formalization Notes
The graph is a relation between the left and the right vertices, both finite types; the bipartite graph split at of this submission gives such a relation between and . A matching is kept as , the left vertex each right vertex currently holds, which is the form the machine keeps it in.
is the search from one left vertex. It is written as a recursion on a fuel, spent once per displaced left vertex; the number of right vertices plus one is always enough, as each descent visits a fresh right vertex. tries one candidate neighbour and passes a success through unchanged, so that the fold over the candidates stops at the first success. tries every left vertex in turn from an empty visited set, keeping the matching it has when a search fails. The machine implements the recursion with an explicit stack of frames, one per displaced vertex, and tries left vertices and neighbours in the order of the word; the order is immaterial to what is proved about the result.
Builds on
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments