The Exact Matching problem asks whether a bipartite graph with edges colored red and blue admits a perfect matching with exactly t red edges. Introduced by Papadimitriou and Yannakakis in 1982, the problem has resisted deterministic polynomial-time algorithms for over four decades, despite admitting a randomized solution via the Schwartz-Zippel lemma since 1987. We prove the Affine-Slice Nonvanishing Conjecture (ASNC) for all bipartite braces and give a deterministic O(n^6) algorithm for Exact Matching on all bipartite graphs. The algorithm follows via the tight-cut decomposition, which reduces the decision problem to brace blocks. The proof proceeds by structural induction on McCuaig's brace decomposition. We establish the McCuaig exceptional families, the replacement determinant algebra, and the narrow-extension cases (KA, J3 to D1). For the superfluous-edge step, we introduce two closure tools: a matching-induced Two-extra Hall theorem that resolves the rank-(m-2) branch via projective-collapse contradiction, and a distinguished-state q-circuit lemma that eliminates the rank-(m-1) branch entirely by showing that any minimal dependent set containing the superfluous state forces rank m-2. The entire proof has been formally verified in the Lean 4 proof assistant.

翻译：暂无翻译