Executable unweighted matching algorithms

The native even-delta-matroid optimizer is applied to Graph.matchingInstance. Original edges whose two endpoint bits are true are returned in normalized edge-list order, retaining their original binary endpoint labels and orientation. Loops, undeclared endpoints and duplicates in either orientation follow Graph.induced; duplicate declarations have no effect.

All enumeration is funded by actual vertex, edge, scope, row and occurrence lists. No interval below a raw binary name is constructed. Explicit exactly-one tables have one stored one-hot row per port, so their row widths enter the native polynomial certificate. This is a specialization of [KKR18], not a tight classical Edmonds operation-bound claim.

@[reducible, inline]

abbrev Cslib.Complexity.Graph.encMatching : List (ℕ × ℕ) ↪ List Bool

Matching output in list order: each edge pair is framed, and inside each pair the first binary endpoint is framed before the second binary endpoint.

@[reducible, inline]

abbrev Cslib.Complexity.Graph.encMatchingBuffer : Graph × List Bool ↪ List Bool

A framed complete graph followed by buffer-order framed one-bit Boolean encodings.

def Cslib.Complexity.Graph.selectedBit (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (bits : List Bool) (x : ℕ) : Bool

Read whether every actual occurrence of a named edge is true.

def Cslib.Complexity.Graph.matchingPositions (G : Graph) (bits : List Bool) : List ℕ

Original edge positions mutually selected by the optimizer's occurrence buffer.

def Cslib.Complexity.Graph.edgesAtPositions (G : Graph) (positions : List ℕ) : List (ℕ × ℕ)

Executable conversion from normalized positions to original graph edge pairs.

def Cslib.Complexity.Graph.maximumMatchingPositions (G : Graph) : List ℕ

Total maximum-cardinality search, returning canonical positions of original graph edges.

def Cslib.Complexity.Graph.maximumMatching (G : Graph) : List (ℕ × ℕ)

Total maximum-cardinality search on complete raw graphs. The internal failure branch is unreachable: the generated instance passes the full model guard on every graph.

def Cslib.Complexity.Graph.maximumMatchingSubgraph (G : Graph) : G.induced.Subgraph

The Mathlib subgraph represented by the returned canonical original positions.

def Cslib.Complexity.Graph.coversVertices (G : Graph) (edges : List (ℕ × ℕ)) : Bool

Check coverage of every distinct declared vertex by selected original edges.

def Cslib.Complexity.Graph.perfectMatching (G : Graph) : Option (List (ℕ × ℕ))

Total perfect-matching search, including the empty perfect matching on an empty graph.

def Cslib.Complexity.Graph.decidePerfectMatching (G : Graph) : Bool

Perfect-matching decision on every complete raw framed graph.

theorem Cslib.Complexity.Graph.checkModel_matchingInstance (G : Graph) : CSP.EdgeSolver.checkModel G.matchingInstance = true

Every generated instance passes all actual finite model tests.

theorem Cslib.Complexity.Graph.matching_optimizer_spec (G : Graph) : ∃ (bits : List Bool), CSP.EdgeSolver.optimize G.matchingInstance = some bits ∧ Logic.PL.CSP.IsOptimalLabeling Logic.PL.CSP.Table.sem (CSP.EdgeAugmenting.labeling G.matchingInstance bits)

The full optimizer always produces an optimal original occurrence labeling.

theorem Cslib.Complexity.Graph.selectedBit_eq_true {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (bits : List Bool) (x : ℕ) : selectedBit F bits x = true ↔ ∀ (o : F.Occurrence), o.var = x → CSP.EdgeAugmenting.labeling F bits o = true

The finite selected-edge scan reads exactly the actual occurrence labeling.

theorem Cslib.Complexity.Graph.mem_matchingPositions (G : Graph) (bits : List Bool) (i : ℕ) : i ∈ G.matchingPositions bits ↔ i < G.edgeList.length ∧ 2 * i ∈ Logic.PL.CSP.selectedVariables (CSP.EdgeAugmenting.labeling G.matchingInstance bits)

A returned position is in range and its original edge is mutually selected.