While this submission is a draft, it cannot be used by other submissions.

Per-Client Fairness Parameters at Treewidth Four

Lax117284.Lemma14 · concepts/Lax117284/Lemma14.lean · lax-117284

proven

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Lemma

    Lemma 14. The problem 1∣kj,rep∣min⁡j∑iZi,j1 \mid k_j, \mathrm{rep} \mid \min_j \sum_i Z_{i,j} is NP-hard even when the overall conflict graph has treewidth at most 44.

    Let GG be an instance of Multicoloured Independent Set in normal form: rr-regular with r≥1r \ge 1, ℓ\ell classes V1,…,VℓV_1, \ldots, V_\ell of n≥4n \ge 4 vertices, and an even number ∣E∣|E| of edges, every edge directed from the smaller class to the larger. The constructed instance has ℓ(n+1)+∣E∣\ell(n+1) + |E| days — for every colour nn vertex days and one validation day, and one edge day per edge — and the clients: a vertex client cvc_v with kcv=1k_{c_v} = 1 for every vertex; a selection client cic_i with kci=1k_{c_i} = 1 for every colour; two edge clients cv,uc_{v,u} and cu,vc_{u,v} with parameter 11 for every edge (v,u)(v,u); two interaction clients c+c^+ and c−c^- with k+=k−=∣E∣/2k^+ = k^- = |E|/2; and a dummy client c0c_0 with k0=ℓ(n+1)+∣E∣k_0 = \ell(n+1) + |E|.

    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 c0c_0 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 NN for the number of clients other than c0c_0 and π\pi for a bijection between them and {1,…,N}\{1, \ldots, N\}, the job of c0c_0 has processing time NN, and the job of such a client cc occupies the π(c)\pi(c)'th time unit of it. On the vertex day of a vertex vv, the clients cvc_v and cic_i of vv's colour have due date rr and processing time rr, the job of c0c_0 has due date r+Nr + N, and every other client cc has due date r+π(c)r + \pi(c) and processing time 11. On the validation day of colour ii, the client of the pp'th vertex of ViV_i has due date rprp and processing time rr, the client cv,uc_{v,u} of the qq'th neighbour uu of that vertex has due date r(p−1)+qr(p-1) + q and processing time 11, the job of c0c_0 has due date rn+Nrn + N, and every other client has due date rn+π(c)rn + \pi(c) and processing time 11. On the edge day of an edge (v,u)(v,u), the client c−c^- has due date 22 and processing time 22, c+c^+ due date 33 and processing time 22, cv,uc_{v,u} due date 33 and processing time 11, cu,vc_{u,v} due date 11 and processing time 11, the job of c0c_0 due date 3+N3 + N, and every other client due date 3+π(c)3 + \pi(c) and processing time 11.

    The overall conflict graph of the constructed instance has a tree decomposition of width four: a root bag {c0,c+,c−}\{c_0, c^+, c^-\}, a bag {c0,c+,c−,ci}\{c_0, c^+, c^-, c_i\} per colour below it, a bag {c0,c+,c−,cv,ci}\{c_0, c^+, c^-, c_v, c_i\} per vertex of that colour below that, and a bag {c0,c+,c−,cv,cv,u}\{c_0, c^+, c^-, c_v, c_{v,u}\} per neighbour uu of vv below that.

    Concept map
    10 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 6 statements. Each proof establishes one of them relative to its assumptions.

    1 correct proven

    2 kvec_le_days proven

    In the paper

    • page 4 of this submission's paper

    Lean source view on GitHub

    1import Lax117284.ConflictGraph
    2import Lax117284.MulticolouredIndepSet
    3import Lax117284.Problems
    4
    5/-!
    6---
    7title: Per-Client Fairness Parameters at Treewidth Four
    8type: lemma
    9---
    10**Lemma 14.** The problem
    111∣kj,rep∣min⁡j∑iZi,j1 \mid k_j, \mathrm{rep} \mid \min_j \sum_i Z_{i,j} is NP-hard even when the overall
    12conflict graph has treewidth at most 44.
    13
    14Let GG be an instance of Multicoloured Independent Set in normal form: rr-regular with
    15r≥1r \ge 1, ℓ\ell classes V1,…,VℓV_1, \ldots, V_\ell of n≥4n \ge 4 vertices, and an even number
    16∣E∣|E| of edges, every edge directed from the smaller class to the larger. The constructed
    17instance has ℓ(n+1)+∣E∣\ell(n+1) + |E| days — for every colour nn *vertex days* and one
    18*validation day*, and one *edge day* per edge — and the clients: a vertex client cvc_v with
    19kcv=1k_{c_v} = 1 for every vertex; a selection client cic_i with kci=1k_{c_i} = 1 for every
    20colour; two edge clients cv,uc_{v,u} and cu,vc_{u,v} with parameter 11 for every edge (v,u)(v,u);
    21two interaction clients c+c^+ and c−c^- with k+=k−=∣E∣/2k^+ = k^- = |E|/2; and a dummy client c0c_0
    22with k0=ℓ(n+1)+∣E∣k_0 = \ell(n+1) + |E|.
    23
    24For every colour the vertex days and the validation day form a *vertex-selection gadget*
    25which compels the selection of a single vertex client for that colour, and the edge days
    26form an *incidence-checking gadget* which certifies that all clients can be satisfied only
    27if the selected vertices form a multicoloured independent set. On each day only a few
    28clients take part in the gadget, and the job of c0c_0 blocks the jobs of all the others: it
    29starts right after the last job of the gadget, and every client not taking part has a
    30unit-length job of its own inside it. Writing NN for the number of clients other than
    31c0c_0 and π\pi for a bijection between them and {1,…,N}\{1, \ldots, N\}, the job of c0c_0 has
    32processing time NN, and the job of such a client cc occupies the π(c)\pi(c)'th time unit of
    33it. On the vertex day of a vertex vv, the clients cvc_v and cic_i of vv's colour have due
    34date rr and processing time rr, the job of c0c_0 has due date r+Nr + N, and every other
    35client cc has due date r+π(c)r + \pi(c) and processing time 11. On the validation day of
    36colour ii, the client of the pp'th vertex of ViV_i has due date rprp and processing time
    37rr, the client cv,uc_{v,u} of the qq'th neighbour uu of that vertex has due date
    38r(p−1)+qr(p-1) + q and processing time 11, the job of c0c_0 has due date rn+Nrn + N, and every
    39other client has due date rn+π(c)rn + \pi(c) and processing time 11. On the edge day of an edge
    40(v,u)(v,u), the client c−c^- has due date 22 and processing time 22, c+c^+ due date 33 and
    41processing time 22, cv,uc_{v,u} due date 33 and processing time 11, cu,vc_{u,v} due date 11
    42and processing time 11, the job of c0c_0 due date 3+N3 + N, and every other client due date
    433+π(c)3 + \pi(c) and processing time 11.
    44
    45The overall conflict graph of the constructed instance has a tree decomposition of width
    46four: a root bag {c0,c+,c−}\{c_0, c^+, c^-\}, a bag {c0,c+,c−,ci}\{c_0, c^+, c^-, c_i\} per colour below it, a
    47bag {c0,c+,c−,cv,ci}\{c_0, c^+, c^-, c_v, c_i\} per vertex of that colour below that, and a bag
    48{c0,c+,c−,cv,cv,u}\{c_0, c^+, c^-, c_v, c_{v,u}\} per neighbour uu of vv below that.
    49
    50# Formalization Notes
    51
    52The clients are numbered: c0c_0 is 00, c+c^+ is 11, c−c^- is 22, then one number per
    53colour, then one per vertex, then one per pair of a vertex and a neighbour index. So
    54π(c)=c\pi(c) = c, the bijection of the source being this numbering, and a client's job inside
    55the job of c0c_0 is its own numbered time unit. The days are numbered by colour blocks of
    56n+1n+1 — the nn vertex days and then the validation day — followed by the edge days in the
    57order the edges are listed.
    58
    59The slot for a vertex and a neighbour index exists for every index below the degree read off
    60the graph, whether or not the vertex has that many neighbours; on a regular graph, which is
    61what the statements assume, every slot is a neighbour. A closed formula for the number of a
    62client is what a reduction can compute, where enumerating only the admissible pairs would
    63need a search.
    64
    65The degree is read off the graph as the number of neighbours of the vertex 00, raised to
    6611 so that no processing time is zero on an instance outside the normal form; on an
    67instance in normal form it is rr.
    68
    69The correctness statement carries the normal form as a hypothesis. The treewidth statement
    70does not: the decomposition above is one of the constructed graph whatever the input, which
    71is what makes the reduction land in the slice.
    72
    73The map on words checks the normal form before it builds anything, and sends a word that
    74fails the check to the rejected word. That check is part of the reduction and not of the
    75source: without it the map would send an instance outside the normal form — one with no
    76colour and one vertex per class, say, whose construction has no day and asks for nothing —
    77to a yes-instance, and would then not be a reduction from the language of the normal form.
    78It is a matter of counting neighbours and edges, and takes quadratic time.
    79
    80That the selected vertices can be checked at all needs rℓ≤∣E∣/2r\ell \le |E|/2, so that the edge
    81days incident to a multicoloured independent set do not exhaust the requirement of one
    82interaction client; this is where n≥4n \ge 4 enters, since ∣E∣=rnℓ/2|E| = rn\ell/2. The source does
    83not state it.
    84-/
    85
    86namespace Lax117284.Lemma14
    87
    88open Lax117284.Problems Lax117284.MulticolouredIndepSet
    89open Lax434930.PolynomialTime Lax429075.Reductions
    90
    91variable (G : Instance)
    92
    93/-- The degree of the graph, read off the vertex `0` and raised to `1`. -/
    94noncomputable def deg : ℕ := max 1 G.degree
    95
    96/-- The number of clients: the dummy client, the two interaction clients, one per colour,
    97one per vertex, and one per pair of a vertex and a neighbour index. -/
    98noncomputable 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
    102and the number of time units inside it. -/
    103noncomputable 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
    106per edge. -/
    107noncomputable def dayCount : ℕ := G.colours * (G.size + 1) + G.edgeCount
    108
    109/-- The number of the selection client of colour `i`. -/
    110def selId (i : ℕ) : ℕ := 3 + i
    111
    112/-- The number of the vertex client of the vertex numbered `w`. -/
    113def 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
    116its `q`'th neighbour. -/
    117noncomputable 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
    121numbered `w₀`. -/
    122noncomputable 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₀`. -/
    129noncomputable 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
    141vertex numbered `w` to the vertex numbered `w'`. -/
    142noncomputable 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`
    151vertex days and a validation day come first, then the edge days. -/
    152noncomputable 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
    161theorem one_le_deg : 1 ≤ deg G := le_max_left 1 _
    162
    163theorem two_le_span : 2 ≤ span G := by unfold span; omega
    164
    165theorem 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
    171theorem 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.** -/
    181noncomputable 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
    190on every day, the two interaction clients on half the edge days each, and every other
    191client once. -/
    192noncomputable 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
    198when the constructed instance admits a schedule meeting every client's own fairness
    199parameter. -/
    200axiom 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
    204four.** -/
    205axiom treewidth_le : ConflictGraph.treewidth (inst G) ≤ 4
    206
    207/-- **No fairness parameter of the constructed instance exceeds its number of days.** -/
    208axiom kvec_le_days (j : Fin (inst G).clients) : kvec G j ≤ (inst G).days
    209
    210open Classical in
    211/-- **The reduction**, as a map on words: a word encoding an instance of Multicoloured
    212Independent Set *in normal form* is sent to the encoding of the constructed instance with
    213its fairness parameters, and every other word — one that encodes an instance outside the
    214normal form as much as one that encodes nothing — to the rejected word. -/
    215noncomputable 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.** -/
    221axiom 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.** -/
    226axiom 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
    229graph has treewidth at most `4`. -/
    230axiom perClient_npHard :
    231 NPHard (PerClient fun I k => ConflictGraph.treewidth I ≤ 4 ∧ ∀ j, k j ≤ I.days)
    232
    233end Lax117284.Lemma14
    234
    Show ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Formalization Notes

    The clients are numbered: c0c_0 is 00, c+c^+ is 11, c−c^- is 22, then one number per colour, then one per vertex, then one per pair of a vertex and a neighbour index. So π(c)=c\pi(c) = c, the bijection of the source being this numbering, and a client's job inside the job of c0c_0 is its own numbered time unit. The days are numbered by colour blocks of n+1n+1 — the nn 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 00, raised to 11 so that no processing time is zero on an instance outside the normal form; on an instance in normal form it is rr.

    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 rℓ≤∣E∣/2r\ell \le |E|/2, so that the edge days incident to a multicoloured independent set do not exhaust the requirement of one interaction client; this is where n≥4n \ge 4 enters, since ∣E∣=rnℓ/2|E| = rn\ell/2. The source does not state it.

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…