Formalizing Randomized Matching Algorithms
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...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2012-08-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/973/pdf |
| _version_ | 1827322947587538944 |
|---|---|
| author | Dai Tri Man Le Stephen A. Cook |
| author_facet | Dai Tri Man Le Stephen A. Cook |
| author_sort | Dai Tri Man Le |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:36:55Z |
| format | Article |
| id | doaj.art-b503d6a303e44a4388e33037d0ea75d8 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:55Z |
| publishDate | 2012-08-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-b503d6a303e44a4388e33037d0ea75d82024-03-08T09:28:00ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742012-08-01Volume 8, Issue 310.2168/LMCS-8(3:5)2012973Formalizing Randomized Matching AlgorithmsDai Tri Man LeStephen A. CookUsing 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.https://lmcs.episciences.org/973/pdfcomputer science - logic in computer sciencecomputer science - computational complexitymathematics - logicf.2.2, f.4.1 |
| spellingShingle | Dai Tri Man Le Stephen A. Cook Formalizing Randomized Matching Algorithms Logical Methods in Computer Science computer science - logic in computer science computer science - computational complexity mathematics - logic f.2.2, f.4.1 |
| title | Formalizing Randomized Matching Algorithms |
| title_full | Formalizing Randomized Matching Algorithms |
| title_fullStr | Formalizing Randomized Matching Algorithms |
| title_full_unstemmed | Formalizing Randomized Matching Algorithms |
| title_short | Formalizing Randomized Matching Algorithms |
| title_sort | formalizing randomized matching algorithms |
| topic | computer science - logic in computer science computer science - computational complexity mathematics - logic f.2.2, f.4.1 |
| url | https://lmcs.episciences.org/973/pdf |
| work_keys_str_mv | AT daitrimanle formalizingrandomizedmatchingalgorithms AT stephenacook formalizingrandomizedmatchingalgorithms |