Multicoloured Independent Set
Lax117284.MulticolouredIndepSet · concepts/Lax117284/MulticolouredIndepSet.lean · lax-117284
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
An instance consists of colour classes of vertices each and a graph on those vertices whose edges join vertices of different classes. It is a yes-instance if one vertex can be chosen from every class so that no two chosen vertices are adjacent — a multicoloured independent set, necessarily of size .
The problem is NP-hard, and remains NP-hard on the instances the reduction of the last section consumes: those in which every vertex has the same number of neighbours, every class holds at least four vertices, and the number of edges is even.
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
In the paper
- page 3 of this submission's paper
Lean source view on GitHub
| 1 | import Lax117284.Problems |
| 2 | import Mathlib.Combinatorics.SimpleGraph.Finite |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Multicoloured Independent Set |
| 7 | type: definition |
| 8 | --- |
| 9 | An instance consists of colour classes of vertices each and a graph on those |
| 10 | vertices whose edges join vertices of different classes. It is a yes-instance if |
| 11 | one vertex can be chosen from every class so that no two chosen vertices are adjacent — a |
| 12 | *multicoloured independent set*, necessarily of size . |
| 13 | |
| 14 | The problem is NP-hard, and remains NP-hard on the instances the reduction of the last |
| 15 | section consumes: those in which every vertex has the same number of neighbours, |
| 16 | every class holds at least four vertices, and the number of edges is even. |
| 17 | |
| 18 | # Formalization Notes |
| 19 | |
| 20 | A vertex is a pair, its class and its index inside the class, so that the colouring is part |
| 21 | of the vertex set rather than a function to be constrained, and a solution is a choice of |
| 22 | one index per class rather than a set whose size and multicolouredness must be argued. |
| 23 | |
| 24 | Vertices are also numbered, the vertex of class and index being , and the |
| 25 | graph is read off those numbers by `adjAt`. A construction reading an instance works with |
| 26 | the numbers, and the numbering has the property the source's convention needs: an edge runs |
| 27 | from the smaller number to the larger exactly when it runs from the smaller class to the |
| 28 | larger. The neighbours of a vertex are listed in increasing order, which is the arbitrary |
| 29 | order the source fixes on them, and the edges are listed likewise. |
| 30 | |
| 31 | Whether two vertices of a finite graph are adjacent is decided by inspection. The |
| 32 | definitions below nevertheless appeal to classical decidability, so that they do not carry |
| 33 | a decision procedure as an argument; no statement about them needs one. |
| 34 | |
| 35 | The three side conditions of the hard slice are the normal form the source assumes of its |
| 36 | input. Regularity and the parity of the edge count let the construction distribute the |
| 37 | edges evenly between two clients; four vertices per class make the number of edges large |
| 38 | enough against the number of classes. All three are reached from an arbitrary instance by |
| 39 | padding, which is part of what the hardness of the slice asserts. |
| 40 | -/ |
| 41 | |
| 42 | namespace Lax117284.MulticolouredIndepSet |
| 43 | |
| 44 | open Lax434930.PolynomialTime |
| 45 | |
| 46 | /-- An instance of Multicoloured Independent Set: a graph on `colours` classes of `size` |
| 47 | vertices whose edges join vertices of different classes. -/ |
| 48 | structure Instance where |
| 49 | /-- The number `ℓ` of colour classes. -/ |
| 50 | colours : ℕ |
| 51 | /-- The number `n` of vertices in each class. -/ |
| 52 | size : ℕ |
| 53 | /-- The graph, on the vertices `(class, index)`. -/ |
| 54 | graph : SimpleGraph (Fin colours × Fin size) |
| 55 | /-- Adjacent vertices lie in different classes. -/ |
| 56 | adj_colour_ne : ∀ u v, graph.Adj u v → u.1 ≠ v.1 |
| 57 | |
| 58 | namespace Instance |
| 59 | |
| 60 | variable (G : Instance) |
| 61 | |
| 62 | /-- **The question of Multicoloured Independent Set**: is there one vertex of every class |
| 63 | such that no two of them are adjacent? -/ |
| 64 | def HasIndepSet : Prop := |
| 65 | ∃ f : Fin G.colours → Fin G.size, ∀ i i', ¬ G.graph.Adj (i, f i) (i', f i') |
| 66 | |
| 67 | /-- The number `ℓn` of vertices. -/ |
| 68 | def vertices : ℕ := G.colours * G.size |
| 69 | |
| 70 | /-- The class of the vertex numbered `w`. -/ |
| 71 | def classOf (w : ℕ) : ℕ := w / G.size |
| 72 | |
| 73 | /-- The index inside its class of the vertex numbered `w`. -/ |
| 74 | def indexOf (w : ℕ) : ℕ := w % G.size |
| 75 | |
| 76 | open Classical in |
| 77 | /-- Whether the vertices numbered `w` and `w'` are adjacent, and `false` for numbers that |
| 78 | name no vertex. -/ |
| 79 | noncomputable def adjAt (w w' : ℕ) : Bool := |
| 80 | if h : w < G.vertices ∧ w' < G.vertices then |
| 81 | have hs : 0 < G.size := by |
| 82 | by_contra h0 |
| 83 | have hz : G.size = 0 := by omega |
| 84 | rw [vertices, hz, Nat.mul_zero] at h |
| 85 | omega |
| 86 | decide (G.graph.Adj |
| 87 | (⟨w / G.size, (Nat.div_lt_iff_lt_mul hs).2 h.1⟩, ⟨w % G.size, Nat.mod_lt _ hs⟩) |
| 88 | (⟨w' / G.size, (Nat.div_lt_iff_lt_mul hs).2 h.2⟩, ⟨w' % G.size, Nat.mod_lt _ hs⟩)) |
| 89 | else false |
| 90 | |
| 91 | /-- The neighbours of the vertex numbered `w`, in increasing order. -/ |
| 92 | noncomputable def nbrs (w : ℕ) : List ℕ := |
| 93 | (List.range G.vertices).filter fun w' => G.adjAt w w' |
| 94 | |
| 95 | /-- The number of neighbours the vertex `0` has; on a regular graph, the degree `r`. -/ |
| 96 | noncomputable def degree : ℕ := (G.nbrs 0).length |
| 97 | |
| 98 | /-- The edges, each listed as the pair of its endpoints from the smaller number to the |
| 99 | larger — which, since adjacent vertices lie in different classes, is from the smaller class |
| 100 | to the larger. -/ |
| 101 | noncomputable def edgeList : List (ℕ × ℕ) := |
| 102 | (List.range G.vertices).flatMap fun w => ((G.nbrs w).filter fun w' => w < w').map (w, ·) |
| 103 | |
| 104 | /-- The number `|E|` of edges. -/ |
| 105 | noncomputable def edgeCount : ℕ := G.edgeList.length |
| 106 | |
| 107 | /-- Every vertex of `G` has exactly `r` neighbours. -/ |
| 108 | def Regular (r : ℕ) : Prop := ∀ w < G.vertices, (G.nbrs w).length = r |
| 109 | |
| 110 | /-- The normal form the reduction into fair repetitive interval scheduling consumes: the |
| 111 | graph is regular of some positive degree, every class holds at least four vertices, and the |
| 112 | number of edges is even. -/ |
| 113 | def Normal : Prop := (∃ r, 0 < r ∧ G.Regular r) ∧ 4 ≤ G.size ∧ 2 ∣ G.edgeCount |
| 114 | |
| 115 | end Instance |
| 116 | |
| 117 | /-- An instance as a binary word: the number of classes, the number of vertices per class, |
| 118 | and then the adjacency matrix, one bit per ordered pair of vertices. -/ |
| 119 | noncomputable def encodeInstance (G : Instance) : Word := |
| 120 | Problems.encodeNat G.colours ++ Problems.encodeNat G.size ++ |
| 121 | (List.range G.vertices).flatMap fun w => |
| 122 | (List.range G.vertices).map fun w' => G.adjAt w w' |
| 123 | |
| 124 | /-- **Multicoloured Independent Set on the instances in normal form**, as a language. -/ |
| 125 | def NormalMulticolouredIndepSet : Language := |
| 126 | {w | ∃ G : Instance, encodeInstance G = w ∧ G.Normal ∧ G.HasIndepSet} |
| 127 | |
| 128 | /-- **Multicoloured Independent Set is NP-hard on the instances in normal form.** -/ |
| 129 | axiom normalMulticolouredIndepSet_npHard : |
| 130 | Problems.NPHard NormalMulticolouredIndepSet |
| 131 | |
| 132 | end Lax117284.MulticolouredIndepSet |
| 133 |
Formalization Notes
A vertex is a pair, its class and its index inside the class, so that the colouring is part of the vertex set rather than a function to be constrained, and a solution is a choice of one index per class rather than a set whose size and multicolouredness must be argued.
Vertices are also numbered, the vertex of class and index being , and the graph is read off those numbers by . A construction reading an instance works with the numbers, and the numbering has the property the source's convention needs: an edge runs from the smaller number to the larger exactly when it runs from the smaller class to the larger. The neighbours of a vertex are listed in increasing order, which is the arbitrary order the source fixes on them, and the edges are listed likewise.
Whether two vertices of a finite graph are adjacent is decided by inspection. The definitions below nevertheless appeal to classical decidability, so that they do not carry a decision procedure as an argument; no statement about them needs one.
The three side conditions of the hard slice are the normal form the source assumes of its input. Regularity and the parity of the edge count let the construction distribute the edges evenly between two clients; four vertices per class make the number of edges large enough against the number of classes. All three are reached from an arbitrary instance by padding, which is part of what the hardness of the slice asserts.
Builds on
Used by
From Mathlib
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments