Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Bipartite Exact Matching in P

Yuefeng Du

Abstract

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.

Bipartite Exact Matching in P

Abstract

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.

Paper Structure

This paper contains 48 sections, 52 theorems, 126 equations, 1 figure, 1 table.

Table of Contents

  1. Introduction
  2. The Exact Matching problem
  3. Our result
  4. Proof overview
  5. Step 1: Tight-cut reduction.
  6. Step 2: Minimal vs. nonminimal braces.
  7. Step 3: The superfluous-edge step (\ref{['thm:p84']}).
  8. Proof architecture
  9. Organization
  10. Preliminaries
  11. Bipartite graphs and perfect matchings
  12. The Vandermonde specialization
  13. Boundary-minor states
  14. Foundational properties
  15. Structural Induction Framework
  16. ...and 33 more sections

Key Result

Theorem 1.1

There exists a deterministic algorithm that solves the Exact Matching problem on bipartite graphs in $O(n^3)$ determinant evaluations, giving $O(n^6)$ arithmetic complexity. $\blacktriangleleft$$\blacktriangleleft$

Figures (1)

  • Figure 1: Proof dependency structure. The algebraic chain (left) and structural tools (right) both feed into the reduction theorem, yielding the main result.

Theorems & Definitions (122)

  • Theorem 1.1: Main Theorem
  • Theorem 1.2: Affine-Slice Nonvanishing, ASNC
  • Remark 1.3
  • Remark 1.4: ASNC scope
  • Definition 2.1: Vandermonde-weighted matrix
  • Definition 2.2: Exact-$t$ Vandermonde polynomial
  • Proposition 2.3: ASNC gives deterministic EM
  • proof
  • Definition 2.4: Boundary-minor polynomial
  • Theorem 2.5: Cycle reachability
  • ...and 112 more