Improved Bounds for Online Matching with Random Edge Arrivals
Yilong Feng, Haolong Li, Zonghan Yang
cs.DS
Nov 10, 2026 · v1
TL;DR
A Lean 4 solver computes the exact optimal-policy value for the upper-bound graph, with machine-checked correctness proofs of the recurrence and memoization invariants.
Abstract
We study the unweighted online matching problem with random edge arrivals, where each edge arrives at an independent time drawn uniformly from $[0,1]$, and the algorithm must immediately and irrevocably accept or reject it while maintaining a matching. Guruganesh and Singla (IPCO, 2017) first broke the $1/2$ barrier of the naive Greedy algorithm by giving a $(1/2+\varepsilon)$-competitive algorithm for a small constant $\varepsilon>0$, a guarantee that has remained the best known for nearly a decade. We give a simple three-phase algorithm that achieves a competitive ratio of $0.5445$ by deliberately rejecting selected early edges to reserve their endpoints for later matching opportunities. With a different choice of parameters, the same algorithm is $0.5535$-competitive on triangle-free graphs, including bipartite graphs. We also establish competitive ratio upper bounds below $0.6964$ for general graphs and $0.7043$ for bipartite graphs via exact rational evaluation of an optimal-policy recurrence on fixed graphs, even when the input graph is known up to isomorphism.
Problem
In unweighted online matching with random edge arrivals, each edge arrives at an independent uniform time in [0,1] and must be accepted or rejected immediately. The best known competitive ratio had been only slightly above 1/2 for nearly a decade.
Approach
A three-phase Reserve-Retain-Recover algorithm deliberately rejects selected early edges so their endpoints stay free for later matches. The analysis uses local greedy comparisons and a polynomial expansion of survival probabilities. Upper bounds come from an exact rational dynamic program for the optimal policy on fixed graphs known up to isomorphism. This computation is implemented in Python, multithreaded C++, and Lean 4, and the recurrence and memoization correctness are proved in Lean 4.
Results
The algorithm is 0.5445-competitive on general graphs and 0.5535-competitive on triangle-free graphs, including bipartite graphs. Upper bounds are below 0.6964 for general graphs and 0.7043 for bipartite graphs. The Lean solver reproduces the exact value on G_10 in about 2 hours.
| Solver | Instance | Running time |
|---|
| Python (reference) | G_10 | ~2 min |
| Lean (verification) | G_10 | ~2 h |
| C++ (multithreaded) | B_{2,3,3} | ~14 min (128 threads, 63 GiB) |
Running times of the three implementations
