LIPIcs.ITP.2023.3.pdf
- Filesize: 0.9 MB
- 18 pages
Document
A Formal Analysis of RANKING
Authors
Mohammad Abdulaziz 
,
Christoph Madlener
-
Part of:
Volume:
14th International Conference on Interactive Theorem Proving (ITP 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-26
File
Document Identifiers
Author Details
Acknowledgements
We thank the anonymous reviewers whose comments helped improve the text and the formal proofs. We also thank Kurt Mehlhorn for his insightful comments.
Cite AsGet BibTex
Mohammad Abdulaziz and Christoph Madlener. A Formal Analysis of RANKING. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.3
https://doi.org/10.4230/LIPIcs.ITP.2023.3
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.
Subject Classification
ACM Subject Classification
- Theory of computation
- Mathematics of computing
Keywords
- Matching Theory
- Formalized Mathematics
- Online Algorithms
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Mohammad Abdulaziz, Kurt Mehlhorn, and Tobias Nipkow. Trustworthy graph algorithms (invited paper). In The 44th International Symposium on Mathematical Foundations of Computer Science (MFCS), 2019.
-
Gagan Aggarwal, Gagan Goel, Chinmay Karande, and Aranyak Mehta. Online Vertex-Weighted Bipartite Matching and Single-bid Budgeted Allocations. In The 22nd Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), 2011.
-
Benjamin E. Birnbaum and Claire Mathieu. On-line bipartite matching made simple. SIGACT News, 2008.
-
Nikhil R. Devanur, Kamal Jain, and Robert D. Kleinberg. Randomized Primal-Dual Analysis of RANKING for Online Bipartite Matching. In The 24th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), January 2013.
-
Manuel Eberl. Verified Real Asymptotics in Isabelle/HOL. In The International Symposium on Symbolic and Algebraic Computation (ISSAC), 2019.
-
Alon Eden, Michal Feldman, Amos Fiat, and Kineret Segal. An Economics-Based Analysis of RANKING for Online Bipartite Matching. In Symposium on Simplicity in Algorithms (SOSA), January 2021.
- Buddhima Gamlath, Michael Kapralov, Andreas Maggiori, Ola Svensson, and David Wajc. Online Matching with General Arrivals, April 2019. URL: https://arxiv.org/abs/1904.08255.
-
Michele Giry. A categorical approach to probability theory. In Categorical Aspects of Topology and Analysis, 1982.
-
Gagan Goel and Aranyak Mehta. Online budgeted matching in random input models with applications to Adwords. In The 19th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), 2008.
-
Johannes Hölzl. Construction and Stochastic Applications of Measure Spaces in Higher-Order Logic. PhD thesis, Technical University Munich, 2013.
-
John E. Hopcroft and Richard M. Karp. An n^5/2 Algorithm for Maximum Matchings in Bipartite Graphs. SIAM J. Comput., 1973.
-
Bala Kalyanasundaram and Kirk Pruhs. An optimal deterministic algorithm for online b-matching. Theor. Comput. Sci., 2000.
-
R. M. Karp, U. V. Vazirani, and V. V. Vazirani. An optimal algorithm for on-line bipartite matching. In The 22nd ACM Symposium on Theory of Computing (STOC), 1990.
-
Harold W. Kuhn. The Hungarian method for the assignment problem. Naval Research Logistics Quarterly, 1955.
-
Aranyak Mehta, Amin Saberi, Umesh V. Vazirani, and Vijay V. Vazirani. AdWords and generalized online matching. J. ACM, 2007.
- Milena Mihail and Thorben Tröbst. Online Matching with High Probability, December 2021. URL: https://arxiv.org/abs/2112.07228.
- Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
- Vijay V. Vazirani. Online Bipartite Matching and Adwords, February 2022. URL: https://arxiv.org/abs/2107.10777.
-
Vijay V. Vazirani. Online Bipartite Matching and Adwords (Invited Talk). In The 47th International Symposium on Mathematical Foundations of Computer Science (MFCS), 2022.