Formalizing randomized matching algorithms

Abstract

Using Jeřábek's framework for probabilistic reasoning, we formalize the correctness of two fundamental RNC2 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. © D. T. M. Lê and S.A. Cook.