FORMALIZING RANDOMIZED MATCHING ALGORITHMS

作     者：Le, Dai Tri Man Cook, Stephen A. 

作者机构：Univ Toronto Dept Comp Sci Toronto ON Canada 

出 版 物：《LOGICAL METHODS IN COMPUTER SCIENCE》 (Log. Methods Comp. Sci.)

年 卷 期：2012年第8卷第3期

页      面：6-6页

核心收录：

学科分类：08[工学] 0701[理学-数学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：Ontario Graduate Scholarship Natural Sciences and Engineering Research Council of Canada 

主　　题：bounded arithmetic computational complexity weak pigeonhole principle probabilistic reasoning randomized algorithms polynomial identity testing 

摘      要：Using Jerabek 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.