Saturating and Perfect Matchings, Decided in the Same Time
Lax117284.BipartiteDecision · concepts/Lax117284/BipartiteDecision.lean · lax-117284
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Corollary
Whether a bipartite graph split at has a matching saturating its left side, and whether it has a perfect matching, are decided within the same bound . The saturating question is also decided on every word, well formed or not, in the same time and in the sense of polynomial time on the word RAM of lax-759944, which is the form another submission can compose with its own reductions.
Concept map
Evidence
This concept declares 4 statements. Each proof establishes one of them relative to its assumptions.
1 decides_perfect proven
2 decides_saturating proven
3 decides_saturating_all proven
4 ramPolytime_saturating proven
Lean source view on GitHub
| 1 | import Lax117284.BipartiteKuhnTime |
| 2 | import Lax759944.RamPolytime |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Saturating and Perfect Matchings, Decided in the Same Time |
| 7 | type: corollary |
| 8 | --- |
| 9 | Whether a bipartite graph split at has a matching saturating its left side, and whether it |
| 10 | has a perfect matching, are decided within the same bound . The saturating |
| 11 | question is also decided *on every word*, well formed or not, in the same time and in the sense |
| 12 | of polynomial time on the word RAM of [lax-759944](https://laxarchive.org/lax-759944/), which is |
| 13 | the form another submission can compose with its own reductions. |
| 14 | |
| 15 | # Formalization Notes |
| 16 | |
| 17 | Both are comparisons of the matching number with a number the word carries: a matching |
| 18 | saturating the left side exists exactly when the matching number is , since a matching of a |
| 19 | graph split at has at most one edge at each left vertex, and a perfect matching exists exactly |
| 20 | when twice the matching number is the number of vertices. The programs compute the matching |
| 21 | number and compare. |
| 22 | |
| 23 | The total statements need a notion of a *well-formed* word that a program can check in linear |
| 24 | time: the counts, the offsets, the targets and the split are as the encoding demands, and every |
| 25 | listed edge crosses the split. Symmetry of the adjacency lists is *not* demanded, because the |
| 26 | graph a word denotes (`wordGraph`) is the symmetric closure of its lists, so the program may |
| 27 | symmetrize the lists itself in linear time; every word encoding a bipartite graph is well formed. |
| 28 | On a well-formed word the answer is that of `decides_saturating`; on any other word it is `0`. |
| 29 | The word `saturatingAnswer` is the function the total program computes, and |
| 30 | `ramPolytime_saturating` states it in the archive's polynomial-time form on a length-prefixed |
| 31 | input, at every word length in which the word fits. |
| 32 | -/ |
| 33 | |
| 34 | namespace Lax117284.BipartiteDecision |
| 35 | |
| 36 | open Lax808846.Ram Lax808846.RamComputes Lax117284.BipartiteGraph Lax117284.BipartiteMatching |
| 37 | open Lax271696.GraphEncoding |
| 38 | |
| 39 | /-- The admissible words: encodings of bipartite graphs split at their last entry, fitting the |
| 40 | word length. -/ |
| 41 | def Dom (c w : ℕ) : Set (List ℕ) := |
| 42 | {x | (∃ (V : ℕ) (G : SimpleGraph (Fin V)) (n : ℕ), EncodesBipartite x V G n) ∧ |
| 43 | c * (x.length + 1) ≤ 2 ^ w} |
| 44 | |
| 45 | open scoped Classical in |
| 46 | /-- **A matching saturating the left side is decided within `c · (n + 1) · (|x| + 1)` |
| 47 | instructions.** -/ |
| 48 | axiom decides_saturating : ∃ (prog : Program) (c : ℕ), ∀ w : ℕ, |
| 49 | ComputesInTime w prog (Dom c w) |
| 50 | (fun x => if ∃ M : (wordGraph x).Subgraph, M.IsMatching ∧ |
| 51 | Saturates (wordGraph x) M (leftSide (vertexCount x) (leftCount x)) then [1] else [0]) |
| 52 | (fun x => c * (leftCount x + 1) * (x.length + 1)) |
| 53 | |
| 54 | open scoped Classical in |
| 55 | /-- **A perfect matching is decided within `c · (n + 1) · (|x| + 1)` instructions.** -/ |
| 56 | axiom decides_perfect : ∃ (prog : Program) (c : ℕ), ∀ w : ℕ, |
| 57 | ComputesInTime w prog (Dom c w) |
| 58 | (fun x => if ∃ M : (wordGraph x).Subgraph, M.IsPerfectMatching then [1] else [0]) |
| 59 | (fun x => c * (leftCount x + 1) * (x.length + 1)) |
| 60 | |
| 61 | /-- **A well-formed bipartite word**: at least as many vertices as left vertices, the length of |
| 62 | a compressed sparse row block plus the split, offsets starting at `0`, ending at twice the edge |
| 63 | count and nondecreasing, every target a vertex, and every listed edge crossing the split. -/ |
| 64 | structure WellFormed (x : List ℕ) : Prop where |
| 65 | /-- The left vertices are among the vertices. -/ |
| 66 | left_le : leftCount x ≤ vertexCount x |
| 67 | /-- The compressed sparse row block, then the split. -/ |
| 68 | length_eq : x.length = 4 + vertexCount x + 2 * edgeCount x |
| 69 | /-- The first offset is `0`. -/ |
| 70 | offset_zero : offset x 0 = 0 |
| 71 | /-- The last offset is twice the edge count. -/ |
| 72 | offset_last : offset x (vertexCount x) = 2 * edgeCount x |
| 73 | /-- The offsets are nondecreasing. -/ |
| 74 | offset_mono : ∀ i < vertexCount x, offset x i ≤ offset x (i + 1) |
| 75 | /-- Every target is a vertex. -/ |
| 76 | target_lt : ∀ j < 2 * edgeCount x, target x j < vertexCount x |
| 77 | /-- Every listed edge crosses the split. -/ |
| 78 | crosses : ∀ u < vertexCount x, ∀ j, offset x u ≤ j → j < offset x (u + 1) → |
| 79 | (u < leftCount x ↔ leftCount x ≤ target x j) |
| 80 | |
| 81 | open scoped Classical in |
| 82 | /-- The answer of the total program: `1` on a well-formed word whose graph has a matching |
| 83 | saturating its left side, `0` on every other word. -/ |
| 84 | noncomputable def saturatingAnswer (x : List ℕ) : List ℕ := |
| 85 | if WellFormed x ∧ ∃ M : (wordGraph x).Subgraph, M.IsMatching ∧ |
| 86 | Saturates (wordGraph x) M (leftSide (vertexCount x) (leftCount x)) then [1] else [0] |
| 87 | |
| 88 | /-- **On every word whose length and entries fit the word length, a matching saturating the |
| 89 | left side is decided within `c · (n + 1) · (|x| + 1)` instructions**, `n` the last entry of the |
| 90 | word, well-formedness included. The entries must fit: the machine holds every entry modulo |
| 91 | `2 ^ w`, so a word with an entry beyond a word is indistinguishable from the well-formed word it |
| 92 | reduces to, and no program could answer both. -/ |
| 93 | axiom decides_saturating_all : ∃ (prog : Program) (c : ℕ), ∀ w : ℕ, |
| 94 | ComputesInTime w prog {x | c * (x.length + 1) ≤ 2 ^ w ∧ ∀ v ∈ x, c * (v + 1) ≤ 2 ^ w} |
| 95 | saturatingAnswer (fun x => c * (leftCount x + 1) * (x.length + 1)) |
| 96 | |
| 97 | /-- **The same, as polynomial time on the word RAM** in the sense of `lax-759944`: one program |
| 98 | reads the length-prefixed word and writes `saturatingAnswer` within a polynomial in the bit size |
| 99 | of the word, at every word length in which the word fits. -/ |
| 100 | axiom ramPolytime_saturating : Lax759944.RamPolytime.RamPolytime saturatingAnswer |
| 101 | |
| 102 | end Lax117284.BipartiteDecision |
| 103 |
Formalization Notes
Both are comparisons of the matching number with a number the word carries: a matching saturating the left side exists exactly when the matching number is , since a matching of a graph split at has at most one edge at each left vertex, and a perfect matching exists exactly when twice the matching number is the number of vertices. The programs compute the matching number and compare.
The total statements need a notion of a well-formed word that a program can check in linear time: the counts, the offsets, the targets and the split are as the encoding demands, and every listed edge crosses the split. Symmetry of the adjacency lists is not demanded, because the graph a word denotes () is the symmetric closure of its lists, so the program may symmetrize the lists itself in linear time; every word encoding a bipartite graph is well formed. On a well-formed word the answer is that of ; on any other word it is . The word is the function the total program computes, and states it in the archive's polynomial-time form on a length-prefixed input, at every word length in which the word fits.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments