A graph with a parameter appended
Lax271696.VertexCover · concepts/Lax271696/VertexCover.lean · lax-271696
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A parameterized graph problem is handed to the machine as one word: the compressed sparse row block encoding the graph, followed by the single entry k. This file defines that instance format and nothing else.
Concept map
Lean source view on GitHub
| 1 | import Lax808846.RamComputes |
| 2 | import Lax271696.GraphEncoding |
| 3 | import Mathlib.Combinatorics.SimpleGraph.VertexCover |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: A graph with a parameter appended |
| 8 | type: definition |
| 9 | --- |
| 10 | A parameterized graph problem is handed to the machine as one word: the |
| 11 | compressed sparse row block encoding the graph, followed by the single |
| 12 | entry *k*. This file defines that instance format and nothing else. |
| 13 | |
| 14 | # Formalization notes |
| 15 | |
| 16 | The instance word is the graph block with one entry appended. The |
| 17 | compressed sparse row block is self-delimiting — its own header |
| 18 | determines its length — so nothing needs to separate it from the |
| 19 | parameter, and the split of the word into the two parts is determined |
| 20 | by the word itself, not chosen. The parameter comes last so that the |
| 21 | graph block sits at the same offsets as in every other statement built |
| 22 | on this encoding. |
| 23 | |
| 24 | The format is defined here, next to the encoding it extends, and the |
| 25 | statements made on it live in the proof packages that import it rather |
| 26 | than restate it, so that every bound stated over it is a claim about |
| 27 | literally the same inputs. Its first consumer is in this submission's |
| 28 | own proof package: the bounded search tree of Downey and Fellows, which |
| 29 | decides vertex cover within *c* · 2^*k* · (|x|+1) steps over this |
| 30 | format. |
| 31 | -/ |
| 32 | |
| 33 | namespace Lax271696.VertexCover |
| 34 | |
| 35 | open Lax808846.Ram Lax808846.RamComputes Lax271696.GraphEncoding |
| 36 | |
| 37 | /-- The word `x` presents the graph `G` on `n` vertices together with |
| 38 | the parameter `k`: a compressed sparse row block encoding `G`, followed |
| 39 | by the single entry `k`. -/ |
| 40 | def EncodesParamInstance (x : List ℕ) (n : ℕ) (G : SimpleGraph (Fin n)) (k : ℕ) : Prop := |
| 41 | ∃ g, x = g ++ [k] ∧ EncodesGraph g n G |
| 42 | |
| 43 | end Lax271696.VertexCover |
| 44 |
Formalization notes
The instance word is the graph block with one entry appended. The compressed sparse row block is self-delimiting — its own header determines its length — so nothing needs to separate it from the parameter, and the split of the word into the two parts is determined by the word itself, not chosen. The parameter comes last so that the graph block sits at the same offsets as in every other statement built on this encoding.
The format is defined here, next to the encoding it extends, and the statements made on it live in the proof packages that import it rather than restate it, so that every bound stated over it is a claim about literally the same inputs. Its first consumer is in this submission's own proof package: the bounded search tree of Downey and Fellows, which decides vertex cover within c · 2^k · (|x|+1) steps over this format.
Used by
none
From Mathlib
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments