3.1. Search and interpret the result🔗

A Cslib.Complexity.Graph stores declared natural-number names in Cslib.Complexity.Graph.vertices and original endpoint pairs in Cslib.Complexity.Graph.edges. Names are binary, even when numerically large. The matching interpretation is undirected: it discards loops and undeclared endpoints, and deduplicates parallel or reversed edges and repeated declarations. Selected pairs retain their original orientation; the input record retains its original lists.

def oneEdge : Graph := ⟨[7, 42, 7], [(7, 7), (42, 7), (7, 42)]⟩

example : oneEdge.maximumMatching = [(42, 7)] := by⊢ oneEdge.maximumMatching = [(42, 7)] decide +kernelAll goals completed! 🐙

example : oneEdge.perfectMatching = some [(42, 7)] := by⊢ oneEdge.perfectMatching = some [(42, 7)] decide +kernelAll goals completed! 🐙

example : oneEdge.decidePerfectMatching = true := by⊢ oneEdge.decidePerfectMatching = true decide +kernelAll goals completed! 🐙

Cslib.Complexity.Graph.maximumMatching always returns a maximum matching, including when the graph has isolates or an odd cycle. Cslib.Complexity.Graph.perfectMatching returns none when some declared vertex cannot be covered. On the empty graph it returns some [].

The output has an associated subgraph in the original mathematical model. Its edges are exactly the returned pairs in either orientation:

example (G : Graph) : G.maximumMatchingSubgraph.IsMaximumMatching :=
  maximumMatchingSubgraph_isMaximumMatching G

example (G : Graph) (M : G.induced.Subgraph) (hM : M.IsMatching) :
    M.edgeSet.ncard ≤ G.maximumMatching.length :=
  maximumMatching_cardinality G M hM

example (G : Graph) {edges : List (ℕ × ℕ)}
    (h : G.perfectMatching = some edges) :
    edges = G.maximumMatching ∧ G.maximumMatchingSubgraph.IsPerfectMatching :=
  perfectMatching_spec h

example (G : Graph) : G.decidePerfectMatching = true ↔
    ∃ M : G.induced.Subgraph, M.IsPerfectMatching :=
  decidePerfectMatching_eq_true G

For clients storing edge positions, Cslib.Complexity.Graph.maximumMatchingPositions returns positions in the normalized edge list, and Cslib.Complexity.Graph.edgesAtPositions converts them to original pairs executably.