max_matching

std.linalg.max_matching · Level L4

A maximum matching of a finite undirected simple graph with its two certificates. First ν(G) by the Tutte–Berge formula, ν(G) = min over U of (n + |U| − odd(G − U))/2, a While over tutte_step through all 2ⁿ vertex sets U; the first U that attains it is returned, and it bounds every matching from above. Then a matching of ν edges, by a backtracking While over matching_step, as a symmetric 0/1 matrix. The two meet, so the matching is maximum. A maximum matching need not be perfect or unique, and a maximal one (no edge can be added) need not be maximum.

ν(G) = min_U (n + |U| − odd(G − U))/2

Signature

max_matching(A: f64[n, n]) → f64[], f64[n, n], f64[n]

Structure

The function as NOVA stores it: one box per input, operation and output, and arrows that carry values. A double border marks another library function this one runs — called once, or by Scan once per element; select it to open that function.

input
operation
constant
call
output

Verification

Signature proven by NOVA’s shape solver, for every size.
Equal to the reference ν by recursion on the lowest vertex; U and the matching in the graph's search orders in exact rational arithmetic, on all 40 test cases.
All 564 float64 results are exact: the error is zero.
Interpreter and NumPy backend return bit-identical results.
At float32 too: the 40 test cases rounded to float32, and 40 of them exact, with zero error.

Accuracy in detail

correctly rounded (the float64 nearest the exact value): 100%
bit-equal to the NumPy formula in float64: 100%
largest error, in units in the last place: 0

Identity

Calls

matching_running matching_step tutte_open tutte_step growth_step

Called by

—

sha256:98d628659e9b012a659a787584995dd1e4fe8629e8d9d3bb8ed38d689d5c1284

The semantic hash of the graph. It changes when the program changes, and never when only its documentation does.

Control handle

Symbol: Ω:std.linalg.max_matching · Ω:max_matching
Pins: sha256:c31a47f8b5f8c1ec6bc6fc6a25e468411e3f70d5a3ec33bac8cc338591d4da25this graph and the 8 it reaches through calls
Evidence: sha256:d89d47b9f5cd8511de551b0ce908f6756bf21e3b1075ca686b5648b2cd5ad45ethe hash of its verification record
Needs: no capability: a pure function

Through NOVA’s control layer, the symbol launches this function only while the program still matches what it pins: a change to this graph, or to any graph it reaches, needs a migration first.