{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:34:53Z","timestamp":1753889693513,"version":"3.41.2"},"reference-count":33,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,8,10]],"date-time":"2012-08-10T00:00:00Z","timestamp":1344556800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Using Je\\v{r}\\'abek 's framework for probabilistic reasoning, we formalize\nthe correctness of two fundamental RNC^2 algorithms for bipartite perfect\nmatching within the theory VPV for polytime reasoning. The first algorithm is\nfor testing if a bipartite graph has a perfect matching, and is based on the\nSchwartz-Zippel Lemma for polynomial identity testing applied to the Edmonds\npolynomial of the graph. The second algorithm, due to Mulmuley, Vazirani and\nVazirani, is for finding a perfect matching, where the key ingredient of this\nalgorithm is the Isolating Lemma.<\/jats:p>","DOI":"10.2168\/lmcs-8(3:5)2012","type":"journal-article","created":{"date-parts":[[2013,11,29]],"date-time":"2013-11-29T08:17:46Z","timestamp":1385713066000},"source":"Crossref","is-referenced-by-count":4,"title":["Formalizing Randomized Matching Algorithms"],"prefix":"10.46298","volume":"Volume 8, Issue 3","author":[{"given":"Dai Tri Man","family":"Le","sequence":"first","affiliation":[]},{"given":"Stephen A.","family":"Cook","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,8,10]]},"reference":[{"issue":"4","key":"10.2168\/LMCS-8(3:5)2012_AB03","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1145\/792538.792540","volume":"50","author":"M. Agrawal and S. Biswas","year":"2003","journal-title":"Journal of the ACM"},{"issue":"3","key":"10.2168\/LMCS-8(3:5)2012_Aro98","doi-asserted-by":"crossref","first-page":"501","DOI":"10.1145\/278298.278306","volume":"45","author":"S. Arora, C. Lund, R. Motwani, M. Sudan,","year":"1998","journal-title":"Journal of the ACM"},{"issue":"1","key":"10.2168\/LMCS-8(3:5)2012_AS98","first-page":"122","volume":"45","author":"S. Arora and S. Safra","year":"1998","journal-title":"Journal of the ACM"},{"key":"10.2168\/LMCS-8(3:5)2012_Bus86","unstructured":"S.R. Buss.Bounded arithmetic. Bibliopolis, Naples, 1986."},{"key":"10.2168\/LMCS-8(3:5)2012_Cob65","unstructured":"A. Cobham. The Intrinsic Computational Difficulty of Functions. InProceedings of the 1995 International Congress for Logic, Methodology and Philosophy of Science, pages 24-30. North-Holland, 1965."},{"key":"10.2168\/LMCS-8(3:5)2012_CF10","doi-asserted-by":"crossref","unstructured":"S. Cook and L. Fontes. Formal Theories for Linear Algebra. InComputer Science Logic, pages 245-259. Springer, 2010.","DOI":"10.1007\/978-3-642-15205-4_21"},{"key":"10.2168\/LMCS-8(3:5)2012_CN10","doi-asserted-by":"crossref","unstructured":"S. Cook and P. Nguyen.Logical foundations of proof complexity. Cambridge University Press, 2010.","DOI":"10.1017\/CBO9780511676277"},{"key":"10.2168\/LMCS-8(3:5)2012_Coo75","doi-asserted-by":"crossref","unstructured":"S.A. Cook. Feasibly constructive proofs and the propositional calculus (preliminary version). InProceedings of the seventh annual ACM symposium on Theory of computing, pages 83-97. ACM, 1975.","DOI":"10.1145\/800116.803756"},{"key":"10.2168\/LMCS-8(3:5)2012_Edm67","doi-asserted-by":"crossref","unstructured":"J. Edmonds. Systems of distinct representatives and linear algebra.J. Res. Natl. Bureau of Standards, 71A:241-245, 1967.","DOI":"10.6028\/jres.071B.033"},{"issue":"1","key":"10.2168\/LMCS-8(3:5)2012_IM83","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1145\/322358.322373","volume":"30","author":"O.H. Ibarra and S. Moran","year":"1983","journal-title":"Journal of the ACM (JACM)"},{"key":"10.2168\/LMCS-8(3:5)2012_IK10","doi-asserted-by":"crossref","unstructured":"R. Impagliazzo and V. Kabanets. Constructive proofs of concentration bounds.Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques, pages 617-631, 2010.","DOI":"10.1007\/978-3-642-15369-3_46"},{"key":"10.2168\/LMCS-8(3:5)2012_IW97","doi-asserted-by":"crossref","unstructured":"R. Impagliazzo and A. Wigderson. P= BPP if E requires exponential circuits: Derandomizing the XOR lemma. InProceedings of the twenty-ninth annual ACM symposium on Theory of computing, pages 220-229. ACM, 1997.","DOI":"10.1145\/258533.258590"},{"issue":"1-3","key":"10.2168\/LMCS-8(3:5)2012_Jer04","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.apal.2003.12.003","volume":"129","author":"E. Jer\u00e1bek","year":"2004","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.2168\/LMCS-8(3:5)2012_Jer05","unstructured":"E. Jer\u00e1bek.Weak pigeonhole principle, and randomized computation. PhD thesis, Faculty of Mathematics and Physics, Charles University, Prague, 2005."},{"issue":"3","key":"10.2168\/LMCS-8(3:5)2012_Jer07","doi-asserted-by":"crossref","first-page":"959","DOI":"10.2178\/jsl\/1191333850","volume":"72","author":"E. Jer\u00e1bek","year":"2007","journal-title":"Journal of Symbolic Logic"},{"key":"10.2168\/LMCS-8(3:5)2012_KV08","unstructured":"B.H. Korte and J. Vygen.Combinatorial optimization: theory and algorithms. Springer Verlag, 2008."},{"key":"10.2168\/LMCS-8(3:5)2012_Kra95","doi-asserted-by":"crossref","unstructured":"J. Kraj\u00edcek.Bounded arithmetic, propositional logic, and complexity theory. Cambridge University Press, 1995.","DOI":"10.1017\/CBO9780511529948"},{"key":"10.2168\/LMCS-8(3:5)2012_KPT91","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/0168-0072(91)90043-L","volume":"52","author":"Jan Kraj\u00edcek, Pavel Pudl\u00e1k, and Gaisi Ta","year":"1991","journal-title":"Annals of Pure and Applied Logic"},{"issue":"1-2","key":"10.2168\/LMCS-8(3:5)2012_Kuh55","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1002\/nav.3800020109","volume":"2","author":"H.W. Kuhn","year":"1955","journal-title":"Naval research logistics quarterly"},{"key":"10.2168\/LMCS-8(3:5)2012_Lov79","unstructured":"L. Lov\u00e1sz. On determinants, matchings and random algorithms. In L. Budach, editor,Fundamentals of Computation Theory, pages 565-574. Akademia-Verlag, 1979."},{"issue":"2","key":"10.2168\/LMCS-8(3:5)2012_MT10","first-page":"1","volume":"57","author":"R.A. Moser and G. Tardos","year":"2010","journal-title":"Journal of the ACM (JACM)"},{"issue":"1","key":"10.2168\/LMCS-8(3:5)2012_MVV87","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/BF02579206","volume":"7","author":"K. Mulmuley, U.V. Vazirani, and V.V. Vaz","year":"1987","journal-title":"Combinatorica"},{"key":"10.2168\/LMCS-8(3:5)2012_Mun57","doi-asserted-by":"crossref","unstructured":"J. Munkres. Algorithms for the assignment and transportation problems.Journal of the Society for Industrial and Applied Mathematics, pages 32-38, 1957.","DOI":"10.1137\/0105003"},{"issue":"2","key":"10.2168\/LMCS-8(3:5)2012_NW94","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/S0022-0000(05)80043-1","volume":"49","author":"N. Nisan and A. Wigderson","year":"1994","journal-title":"Journal of Computer and System Sciences"},{"issue":"4","key":"10.2168\/LMCS-8(3:5)2012_PWW88","doi-asserted-by":"crossref","first-page":"1235","DOI":"10.2307\/2274618","volume":"53","author":"J.B. Paris, A.J. Wilkie, and A.R. Woods","year":"1988","journal-title":"Journal of Symbolic Logic"},{"key":"10.2168\/LMCS-8(3:5)2012_Pud91","doi-asserted-by":"crossref","unstructured":"P. Pudl\u00e1k. Ramsey's theorem in bounded arithmetic. InComputer Science Logic, pages 308-317. Springer, 1991.","DOI":"10.1007\/3-540-54487-9_67"},{"issue":"4","key":"10.2168\/LMCS-8(3:5)2012_Sch80","doi-asserted-by":"crossref","first-page":"717","DOI":"10.1145\/322217.322225","volume":"27","author":"J.T. Schwartz","year":"1980","journal-title":"Journal of the ACM (JACM)"},{"issue":"4","key":"10.2168\/LMCS-8(3:5)2012_Sha92","doi-asserted-by":"crossref","first-page":"869","DOI":"10.1145\/146585.146609","volume":"39","author":"A. Shamir","year":"1992","journal-title":"Journal of the ACM"},{"key":"10.2168\/LMCS-8(3:5)2012_SC04","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1016\/j.apal.2003.10.018","volume":"130","author":"M. Soltys and S. Cook","year":"2004","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.2168\/LMCS-8(3:5)2012_Tha02","unstructured":"N. Thapen.The weak pigeonhole principle in models of bounded arithmetic. PhD thesis, University of Oxford, 2002."},{"issue":"5","key":"10.2168\/LMCS-8(3:5)2012_Tod91","doi-asserted-by":"crossref","first-page":"865","DOI":"10.1137\/0220053","volume":"20","author":"S. Toda","year":"1991","journal-title":"SIAM Journal on Computing"},{"issue":"6","key":"10.2168\/LMCS-8(3:5)2012_WB97","doi-asserted-by":"crossref","first-page":"826","DOI":"10.1145\/268999.269003","volume":"44","author":"H. Wasserman and M. Blum","year":"1997","journal-title":"Journal of the ACM"},{"issue":"4","key":"10.2168\/LMCS-8(3:5)2012_Zip89","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/0020-0190(89)90143-9","volume":"33","author":"R. Zippel","year":"1989","journal-title":"Information Processing Letters"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/973\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/973\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:00:26Z","timestamp":1681243226000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/973"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8,10]]},"references-count":33,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(3:5)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1103.5215","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1103.5215","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,8,10]]},"article-number":"973"}}