A Formal Analysis of RANKING
Mohammad Abdulaziz, Christoph Madlener
TL;DR
This paper provides a formal correctness proof for the RANKING algorithm in online bipartite matching, revealing a gap in previous combinatorial proofs and highlighting challenges in formalising graphical arguments.
Contribution
It presents the first formal proof of RANKING's correctness, identifying and addressing a gap in existing combinatorial proofs.
Findings
Identified a gap in all prior combinatorial proofs of RANKING
Formalised the correctness proof of RANKING
Highlighted difficulties in formalising graphical arguments
Abstract
We describe a formal correctness proof of RANKING, an online algorithm for online bipartite matching. An outcome of our formalisation is that it shows that there is a gap in all combinatorial proofs of the algorithm. Filling that gap constituted the majority of the effort which went into this work. This is despite the algorithm being one of the most studied algorithms and a central result in theoretical computer science. This gap is an example of difficulties in formalising graphical arguments which are ubiquitous in the theory of computing.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.