Document Open Access Logo

A Formal Analysis of RANKING

Authors Mohammad Abdulaziz , Christoph Madlener

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2023.3.pdf
  • Filesize: 0.9 MB
  • 18 pages

Document Identifiers

Related Versions

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)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get 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

Author Details

Mohammad Abdulaziz
  • King’s College London, UK
  • Technische Universität München, Germany
Christoph Madlener
  • Technische Universität München, Germany

Funding

  • Abdulaziz, Mohammad: Part of this work was funded by DFG Koselleck Grant NI 491/16-1.

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.

References

  1. 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. Google Scholar
  2. 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. Google Scholar
  3. Benjamin E. Birnbaum and Claire Mathieu. On-line bipartite matching made simple. SIGACT News, 2008. Google Scholar
  4. 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. Google Scholar
  5. Manuel Eberl. Verified Real Asymptotics in Isabelle/HOL. In The International Symposium on Symbolic and Algebraic Computation (ISSAC), 2019. Google Scholar
  6. 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. Google Scholar
  7. 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.
  8. Michele Giry. A categorical approach to probability theory. In Categorical Aspects of Topology and Analysis, 1982. Google Scholar
  9. 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. Google Scholar
  10. Johannes Hölzl. Construction and Stochastic Applications of Measure Spaces in Higher-Order Logic. PhD thesis, Technical University Munich, 2013. Google Scholar
  11. John E. Hopcroft and Richard M. Karp. An n^5/2 Algorithm for Maximum Matchings in Bipartite Graphs. SIAM J. Comput., 1973. Google Scholar
  12. Bala Kalyanasundaram and Kirk Pruhs. An optimal deterministic algorithm for online b-matching. Theor. Comput. Sci., 2000. Google Scholar
  13. 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. Google Scholar
  14. Harold W. Kuhn. The Hungarian method for the assignment problem. Naval Research Logistics Quarterly, 1955. Google Scholar
  15. Aranyak Mehta, Amin Saberi, Umesh V. Vazirani, and Vijay V. Vazirani. AdWords and generalized online matching. J. ACM, 2007. Google Scholar
  16. Milena Mihail and Thorben Tröbst. Online Matching with High Probability, December 2021. URL: https://arxiv.org/abs/2112.07228.
  17. 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.
  18. Vijay V. Vazirani. Online Bipartite Matching and Adwords, February 2022. URL: https://arxiv.org/abs/2107.10777.
  19. Vijay V. Vazirani. Online Bipartite Matching and Adwords (Invited Talk). In The 47th International Symposium on Mathematical Foundations of Computer Science (MFCS), 2022. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact