Per-Client Fairness Parameters at Treewidth Four
Lax117284.Lemma14 · concepts/Lax117284/Lemma14.lean · lax-117284
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Lemma
Lemma 14. The problem is NP-hard even when the overall conflict graph has treewidth at most .
Let be an instance of Multicoloured Independent Set in normal form: -regular with , classes of vertices, and an even number of edges, every edge directed from the smaller class to the larger. The constructed instance has days — for every colour vertex days and one validation day, and one edge day per edge — and the clients: a vertex client with for every vertex; a selection client with for every colour; two edge clients and with parameter for every edge ; two interaction clients and with ; and a dummy client with .
For every colour the vertex days and the validation day form a vertex-selection gadget which compels the selection of a single vertex client for that colour, and the edge days form an incidence-checking gadget which certifies that all clients can be satisfied only if the selected vertices form a multicoloured independent set. On each day only a few clients take part in the gadget, and the job of blocks the jobs of all the others: it starts right after the last job of the gadget, and every client not taking part has a unit-length job of its own inside it. Writing for the number of clients other than and for a bijection between them and , the job of has processing time , and the job of such a client occupies the 'th time unit of it. On the vertex day of a vertex , the clients and of 's colour have due date and processing time , the job of has due date , and every other client has due date and processing time . On the validation day of colour , the client of the 'th vertex of has due date and processing time , the client of the 'th neighbour of that vertex has due date and processing time , the job of has due date , and every other client has due date and processing time . On the edge day of an edge , the client has due date and processing time , due date and processing time , due date and processing time , due date and processing time , the job of due date , and every other client due date and processing time .
The overall conflict graph of the constructed instance has a tree decomposition of width four: a root bag , a bag per colour below it, a bag per vertex of that colour below that, and a bag per neighbour of below that.
Concept map
Evidence
In the paper
- page 4 of this submission's paper
Lean source view on GitHub
| 1 | import Lax117284.ConflictGraph |
| 2 | import Lax117284.MulticolouredIndepSet |
| 3 | import Lax117284.Problems |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Per-Client Fairness Parameters at Treewidth Four |
| 8 | type: lemma |
| 9 | --- |
| 10 | **Lemma 14.** The problem |
| 11 | is NP-hard even when the overall |
| 12 | conflict graph has treewidth at most . |
| 13 | |
| 14 | Let be an instance of Multicoloured Independent Set in normal form: -regular with |
| 15 | , classes of vertices, and an even number |
| 16 | of edges, every edge directed from the smaller class to the larger. The constructed |
| 17 | instance has days — for every colour *vertex days* and one |
| 18 | *validation day*, and one *edge day* per edge — and the clients: a vertex client with |
| 19 | for every vertex; a selection client with for every |
| 20 | colour; two edge clients and with parameter for every edge ; |
| 21 | two interaction clients and with ; and a dummy client |
| 22 | with . |
| 23 | |
| 24 | For every colour the vertex days and the validation day form a *vertex-selection gadget* |
| 25 | which compels the selection of a single vertex client for that colour, and the edge days |
| 26 | form an *incidence-checking gadget* which certifies that all clients can be satisfied only |
| 27 | if the selected vertices form a multicoloured independent set. On each day only a few |
| 28 | clients take part in the gadget, and the job of blocks the jobs of all the others: it |
| 29 | starts right after the last job of the gadget, and every client not taking part has a |
| 30 | unit-length job of its own inside it. Writing for the number of clients other than |
| 31 | and for a bijection between them and , the job of has |
| 32 | processing time , and the job of such a client occupies the 'th time unit of |
| 33 | it. On the vertex day of a vertex , the clients and of 's colour have due |
| 34 | date and processing time , the job of has due date , and every other |
| 35 | client has due date and processing time . On the validation day of |
| 36 | colour , the client of the 'th vertex of has due date and processing time |
| 37 | , the client of the 'th neighbour of that vertex has due date |
| 38 | and processing time , the job of has due date , and every |
| 39 | other client has due date and processing time . On the edge day of an edge |
| 40 | , the client has due date and processing time , due date and |
| 41 | processing time , due date and processing time , due date |
| 42 | and processing time , the job of due date , and every other client due date |
| 43 | and processing time . |
| 44 | |
| 45 | The overall conflict graph of the constructed instance has a tree decomposition of width |
| 46 | four: a root bag , a bag per colour below it, a |
| 47 | bag per vertex of that colour below that, and a bag |
| 48 | per neighbour of below that. |
| 49 | |
| 50 | # Formalization Notes |
| 51 | |
| 52 | The clients are numbered: is , is , is , then one number per |
| 53 | colour, then one per vertex, then one per pair of a vertex and a neighbour index. So |
| 54 | , the bijection of the source being this numbering, and a client's job inside |
| 55 | the job of is its own numbered time unit. The days are numbered by colour blocks of |
| 56 | — the vertex days and then the validation day — followed by the edge days in the |
| 57 | order the edges are listed. |
| 58 | |
| 59 | The slot for a vertex and a neighbour index exists for every index below the degree read off |
| 60 | the graph, whether or not the vertex has that many neighbours; on a regular graph, which is |
| 61 | what the statements assume, every slot is a neighbour. A closed formula for the number of a |
| 62 | client is what a reduction can compute, where enumerating only the admissible pairs would |
| 63 | need a search. |
| 64 | |
| 65 | The degree is read off the graph as the number of neighbours of the vertex , raised to |
| 66 | so that no processing time is zero on an instance outside the normal form; on an |
| 67 | instance in normal form it is . |
| 68 | |
| 69 | The correctness statement carries the normal form as a hypothesis. The treewidth statement |
| 70 | does not: the decomposition above is one of the constructed graph whatever the input, which |
| 71 | is what makes the reduction land in the slice. |
| 72 | |
| 73 | The map on words checks the normal form before it builds anything, and sends a word that |
| 74 | fails the check to the rejected word. That check is part of the reduction and not of the |
| 75 | source: without it the map would send an instance outside the normal form — one with no |
| 76 | colour and one vertex per class, say, whose construction has no day and asks for nothing — |
| 77 | to a yes-instance, and would then not be a reduction from the language of the normal form. |
| 78 | It is a matter of counting neighbours and edges, and takes quadratic time. |
| 79 | |
| 80 | That the selected vertices can be checked at all needs , so that the edge |
| 81 | days incident to a multicoloured independent set do not exhaust the requirement of one |
| 82 | interaction client; this is where enters, since . The source does |
| 83 | not state it. |
| 84 | -/ |
| 85 | |
| 86 | namespace Lax117284.Lemma14 |
| 87 | |
| 88 | open Lax117284.Problems Lax117284.MulticolouredIndepSet |
| 89 | open Lax434930.PolynomialTime Lax429075.Reductions |
| 90 | |
| 91 | variable (G : Instance) |
| 92 | |
| 93 | /-- The degree of the graph, read off the vertex `0` and raised to `1`. -/ |
| 94 | noncomputable def deg : ℕ := max 1 G.degree |
| 95 | |
| 96 | /-- The number of clients: the dummy client, the two interaction clients, one per colour, |
| 97 | one per vertex, and one per pair of a vertex and a neighbour index. -/ |
| 98 | noncomputable def clientCount : ℕ := |
| 99 | 3 + G.colours + G.vertices + G.vertices * deg G |
| 100 | |
| 101 | /-- The number `N` of clients other than the dummy client, which is the length of its job |
| 102 | and the number of time units inside it. -/ |
| 103 | noncomputable def span : ℕ := 2 + G.colours + G.vertices + G.vertices * deg G |
| 104 | |
| 105 | /-- The number of days: `n` vertex days and one validation day per colour, and one edge day |
| 106 | per edge. -/ |
| 107 | noncomputable def dayCount : ℕ := G.colours * (G.size + 1) + G.edgeCount |
| 108 | |
| 109 | /-- The number of the selection client of colour `i`. -/ |
| 110 | def selId (i : ℕ) : ℕ := 3 + i |
| 111 | |
| 112 | /-- The number of the vertex client of the vertex numbered `w`. -/ |
| 113 | def vtxId (w : ℕ) : ℕ := 3 + G.colours + w |
| 114 | |
| 115 | /-- The number of the edge client `c_{v,u}` where `v` is the vertex numbered `w` and `u` is |
| 116 | its `q`'th neighbour. -/ |
| 117 | noncomputable def incId (w q : ℕ) : ℕ := |
| 118 | 3 + G.colours + G.vertices + w * deg G + q |
| 119 | |
| 120 | /-- The processing time and the due date of client `c` on the vertex day of the vertex |
| 121 | numbered `w₀`. -/ |
| 122 | noncomputable def vertexDay (w₀ c : ℕ) : ℕ × ℕ := |
| 123 | if c = 0 then (span G, deg G + span G) |
| 124 | else if c = vtxId G w₀ ∨ c = selId (G.classOf w₀) then (deg G, deg G) |
| 125 | else (1, deg G + c) |
| 126 | |
| 127 | /-- The processing time and the due date of client `c` on the validation day of colour |
| 128 | `i₀`. -/ |
| 129 | noncomputable def validationDay (i₀ c : ℕ) : ℕ × ℕ := |
| 130 | if c = 0 then (span G, deg G * G.size + span G) |
| 131 | else if 3 + G.colours ≤ c ∧ c < 3 + G.colours + G.vertices ∧ |
| 132 | G.classOf (c - (3 + G.colours)) = i₀ then |
| 133 | (deg G, deg G * (G.indexOf (c - (3 + G.colours)) + 1)) |
| 134 | else if 3 + G.colours + G.vertices ≤ c ∧ |
| 135 | G.classOf ((c - (3 + G.colours + G.vertices)) / deg G) = i₀ then |
| 136 | (1, deg G * G.indexOf ((c - (3 + G.colours + G.vertices)) / deg G) |
| 137 | + (c - (3 + G.colours + G.vertices)) % deg G + 1) |
| 138 | else (1, deg G * G.size + c) |
| 139 | |
| 140 | /-- The processing time and the due date of client `c` on the edge day of the edge from the |
| 141 | vertex numbered `w` to the vertex numbered `w'`. -/ |
| 142 | noncomputable def edgeDay (w w' c : ℕ) : ℕ × ℕ := |
| 143 | if c = 0 then (span G, 3 + span G) |
| 144 | else if c = 2 then (2, 2) |
| 145 | else if c = 1 then (2, 3) |
| 146 | else if c = incId G w ((G.nbrs w).idxOf w') then (1, 3) |
| 147 | else if c = incId G w' ((G.nbrs w').idxOf w) then (1, 1) |
| 148 | else (1, 3 + c) |
| 149 | |
| 150 | /-- The processing time and the due date of client `c` on day `i`: the colour blocks of `n` |
| 151 | vertex days and a validation day come first, then the edge days. -/ |
| 152 | noncomputable def job (i c : ℕ) : ℕ × ℕ := |
| 153 | if i < G.colours * (G.size + 1) then |
| 154 | (if i % (G.size + 1) < G.size then |
| 155 | vertexDay G ((i / (G.size + 1)) * G.size + i % (G.size + 1)) c |
| 156 | else validationDay G (i / (G.size + 1)) c) |
| 157 | else |
| 158 | edgeDay G (G.edgeList.getD (i - G.colours * (G.size + 1)) (0, 0)).1 |
| 159 | (G.edgeList.getD (i - G.colours * (G.size + 1)) (0, 0)).2 c |
| 160 | |
| 161 | theorem one_le_deg : 1 ≤ deg G := le_max_left 1 _ |
| 162 | |
| 163 | theorem two_le_span : 2 ≤ span G := by unfold span; omega |
| 164 | |
| 165 | theorem job_pos (i c : ℕ) : 0 < (job G i c).1 := by |
| 166 | have hd := one_le_deg G |
| 167 | have hs := two_le_span G |
| 168 | unfold job vertexDay validationDay edgeDay |
| 169 | split_ifs <;> simp only [] <;> omega |
| 170 | |
| 171 | theorem job_le (i c : ℕ) : (job G i c).1 ≤ (job G i c).2 := by |
| 172 | have hd := one_le_deg G |
| 173 | have hs := two_le_span G |
| 174 | have hm : ∀ a b : ℕ, a ≤ a * (b + 1) := fun a b => Nat.le_mul_of_pos_right a (Nat.succ_pos b) |
| 175 | unfold job vertexDay validationDay edgeDay |
| 176 | split_ifs <;> simp only [] <;> first |
| 177 | | omega |
| 178 | | exact hm _ _ |
| 179 | |
| 180 | /-- **The instance of Lemma 14.** -/ |
| 181 | noncomputable def inst : Scheduling.Instance where |
| 182 | clients := clientCount G |
| 183 | days := dayCount G |
| 184 | p i c := (job G i c).1 |
| 185 | d i c := (job G i c).2 |
| 186 | p_pos i c := job_pos G i c |
| 187 | p_le_d i c := job_le G i c |
| 188 | |
| 189 | /-- **The fairness parameters of the constructed instance**: the dummy client is required |
| 190 | on every day, the two interaction clients on half the edge days each, and every other |
| 191 | client once. -/ |
| 192 | noncomputable def kvec : Fin (inst G).clients → ℕ := fun c => |
| 193 | if (c : ℕ) = 0 then dayCount G |
| 194 | else if (c : ℕ) = 1 ∨ (c : ℕ) = 2 then G.edgeCount / 2 |
| 195 | else 1 |
| 196 | |
| 197 | /-- **The construction is correct**: the graph has a multicoloured independent set exactly |
| 198 | when the constructed instance admits a schedule meeting every client's own fairness |
| 199 | parameter. -/ |
| 200 | axiom correct (hG : G.Normal) : |
| 201 | G.HasIndepSet ↔ (inst G).HasFairSchedule (kvec G) |
| 202 | |
| 203 | /-- **The overall conflict graph of the constructed instance has treewidth at most |
| 204 | four.** -/ |
| 205 | axiom treewidth_le : ConflictGraph.treewidth (inst G) ≤ 4 |
| 206 | |
| 207 | /-- **No fairness parameter of the constructed instance exceeds its number of days.** -/ |
| 208 | axiom kvec_le_days (j : Fin (inst G).clients) : kvec G j ≤ (inst G).days |
| 209 | |
| 210 | open Classical in |
| 211 | /-- **The reduction**, as a map on words: a word encoding an instance of Multicoloured |
| 212 | Independent Set *in normal form* is sent to the encoding of the constructed instance with |
| 213 | its fairness parameters, and every other word — one that encodes an instance outside the |
| 214 | normal form as much as one that encodes nothing — to the rejected word. -/ |
| 215 | noncomputable def reduce (w : Word) : Word := |
| 216 | if h : ∃ G : Instance, encodeInstance G = w ∧ G.Normal then |
| 217 | encodePerClient (inst h.choose) (kvec h.choose) |
| 218 | else rejectedPerClient |
| 219 | |
| 220 | /-- **The reduction is correct.** -/ |
| 221 | axiom reduce_correct (w : Word) : |
| 222 | w ∈ NormalMulticolouredIndepSet ↔ |
| 223 | reduce w ∈ PerClient fun I k => ConflictGraph.treewidth I ≤ 4 ∧ ∀ j, k j ≤ I.days |
| 224 | |
| 225 | /-- **The reduction runs in polynomial time.** -/ |
| 226 | axiom reduce_polyTime : Nonempty (Turing.TM2ComputableInPolyTime id id reduce) |
| 227 | |
| 228 | /-- **Lemma 14.** The per-client problem is NP-hard on the instances whose overall conflict |
| 229 | graph has treewidth at most `4`. -/ |
| 230 | axiom perClient_npHard : |
| 231 | NPHard (PerClient fun I k => ConflictGraph.treewidth I ≤ 4 ∧ ∀ j, k j ≤ I.days) |
| 232 | |
| 233 | end Lax117284.Lemma14 |
| 234 |
Formalization Notes
The clients are numbered: is , is , is , then one number per colour, then one per vertex, then one per pair of a vertex and a neighbour index. So , the bijection of the source being this numbering, and a client's job inside the job of is its own numbered time unit. The days are numbered by colour blocks of — the vertex days and then the validation day — followed by the edge days in the order the edges are listed.
The slot for a vertex and a neighbour index exists for every index below the degree read off the graph, whether or not the vertex has that many neighbours; on a regular graph, which is what the statements assume, every slot is a neighbour. A closed formula for the number of a client is what a reduction can compute, where enumerating only the admissible pairs would need a search.
The degree is read off the graph as the number of neighbours of the vertex , raised to so that no processing time is zero on an instance outside the normal form; on an instance in normal form it is .
The correctness statement carries the normal form as a hypothesis. The treewidth statement does not: the decomposition above is one of the constructed graph whatever the input, which is what makes the reduction land in the slice.
The map on words checks the normal form before it builds anything, and sends a word that fails the check to the rejected word. That check is part of the reduction and not of the source: without it the map would send an instance outside the normal form — one with no colour and one vertex per class, say, whose construction has no day and asks for nothing — to a yes-instance, and would then not be a reduction from the language of the normal form. It is a matter of counting neighbours and edges, and takes quadratic time.
That the selected vertices can be checked at all needs , so that the edge days incident to a multicoloured independent set do not exhaust the requirement of one interaction client; this is where enters, since . The source does not state it.
Used by
none
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments