Formalizing Randomized Matching Algorithms
Dai Tri Man Le (University of Toronto), Stephen A. Cook (University of, Toronto)
TL;DR
This paper formalizes the correctness of two fundamental randomized algorithms for bipartite perfect matching within a formal logical framework, using probabilistic reasoning and key algebraic lemmas.
Contribution
It provides a formal proof of correctness for two classic RNC^2 algorithms in a logical theory suitable for polynomial-time reasoning.
Findings
Formal proof of correctness for bipartite perfect matching algorithms
Application of Schwartz-Zippel Lemma within formal framework
Use of Isolating Lemma in formal verification
Abstract
Using Je\v{r}\'abek 's framework for probabilistic reasoning, we formalize the correctness of two fundamental RNC^2 algorithms for bipartite perfect matching within the theory VPV for polytime reasoning. The first algorithm is for testing if a bipartite graph has a perfect matching, and is based on the Schwartz-Zippel Lemma for polynomial identity testing applied to the Edmonds polynomial of the graph. The second algorithm, due to Mulmuley, Vazirani and Vazirani, is for finding a perfect matching, where the key ingredient of this algorithm is the Isolating Lemma.
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.