Raising the Number of Days and the Fairness Parameter

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

proven

Loading review…

Natural Language Statement

Corollary

Corollary 8. The problem $1 \mid \mathrm{rep},\, p_{i,j} = p_j \mid \min_j \sum_i Z_{i,j}$ is NP-hard whenever $m \ge 3$ and $0 < k < m-1$ .

Two constructions lift hardness from one pair $(m, k)$ to the next. Adding a single day on which no two jobs conflict raises the attainable fairness by exactly one, so hardness for $(m, k)$ gives hardness for $(m+1, k+1)$ : every client is served on the new day, and on the old days nothing has changed. Adding one day together with one new client raises the number of days at $k = 1$ : the new client's job blocks every job on each of the old days, and on the new day all jobs coincide, so a $1$ -fair schedule must serve the new client on the new day and is otherwise a $1$ -fair schedule of the old instance. Together with the base case $(m, k) = (3, 1)$ these two steps reach every pair with $m \ge 3$ and $0 < k < m-1$ .

Both constructions give the new day the processing times of the first day, so an instance with day-independent processing times is sent to one with day-independent processing times, which is what makes the corollary a statement about that restriction.

Concept map

7 concepts; 1 descendant hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

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

In the paper

page 2 of this submission's paper

Lean source view on GitHub

Show types on hover

1	import Lax117284.Problems
2
3	/-!
4	---
5	title: Raising the Number of Days and the Fairness Parameter
6	type: corollary
7	---
8	Corollary 8. The problem
9	$1 \mid \mathrm{rep},\, p_{i,j} = p_j \mid \min_j \sum_i Z_{i,j}$ is NP-hard whenever
10	$m \ge 3$ and $0 < k < m-1$ .
11
12	Two constructions lift hardness from one pair $(m, k)$ to the next. Adding a single day on
13	which no two jobs conflict raises the attainable fairness by exactly one, so hardness for
14	$(m, k)$ gives hardness for $(m+1, k+1)$ : every client is served on the new day, and on the
15	old days nothing has changed. Adding one day together with one new client raises the number
16	of days at $k = 1$ : the new client's job blocks every job on each of the old days, and on the
17	new day all jobs coincide, so a $1$ -fair schedule must serve the new client on the new day
18	and is otherwise a $1$ -fair schedule of the old instance. Together with the base case
19	$(m, k) = (3, 1)$ these two steps reach every pair with $m \ge 3$ and $0 < k < m-1$ .
20
21	Both constructions give the new day the processing times of the first day, so an instance
22	with day-independent processing times is sent to one with day-independent processing times,
23	which is what makes the corollary a statement about that restriction.
24
25	# Formalization Notes
26
27	The conflict-free day is laid out explicitly: client $j$ receives the interval ending at
28	$(j+1)Q$ , where $Q$ is at least every processing time of the first day. Consecutive clients
29	are then separated by at least $Q$ , so no two of their jobs meet. The source does not say
30	how to lay such a day out.
31
32	On the blocking day every job ends at the same time, one later than every due date of the
33	instance, so all of them pairwise conflict; the new client receives that same job on every
34	day, which is why it blocks every old job as well.
35
36	The new client is numbered $n$ and the new day $m$ .
37
38	An instance without clients is a yes-instance, and its table is empty, so its code does not
39	reflect its number of days. Adding a blocking client to it would add one cell per day, which is
40	exponentially many cells in the length of the code, so the map does not add one: it sends such
41	an instance to the instance without clients and one more day, which is again a yes-instance of
42	the same fairness parameter. Everything else is as in the source.
43	-/
44
45	namespace Lax117284.Corollary8
46
47	open Lax117284.Scheduling Lax117284.Problems Lax434930.PolynomialTime
48	open Lax429075.Reductions
49
50	/-- A time later than every due date of `I`. -/
51	def bound (I : Instance) : ℕ :=
52	(Finset.univ.sup fun i => Finset.univ.sup fun j => I.d i j) + 1
53
54	/-- A length at least every processing time of the first day of `I`. -/
55	def gap (I : Instance) : ℕ := Finset.univ.sup fun j : Fin I.clients => I.pAt 0 j
56
57	/-- The instance with one conflict-free day added: on the new day client `j`'s job has
58	the processing time it has on the first day and ends at `(j+1)` times a length at least
59	every such processing time, so no two jobs of the new day meet. -/
60	def addFreeDay (I : Instance) : Instance where
61	clients := I.clients
62	days := I.days + 1
63	p i j := if (i : ℕ) < I.days then I.pAt i j else I.pAt 0 j
64	d i j := if (i : ℕ) < I.days then I.dAt i j else ((j : ℕ) + 1) * gap I
65	p_pos i j := by
66	have h0 := I.pAt_pos (i : ℕ) (j : ℕ)
67	have h1 := I.pAt_pos 0 (j : ℕ)
68	split_ifs <;> omega
69	p_le_d i j := by
70	have h1 := I.pAt_le_dAt (i : ℕ) (j : ℕ)
71	have h2 : I.pAt 0 (j : ℕ) ≤ gap I := by
72	have := Finset.le_sup (f := fun j' : Fin I.clients => I.pAt 0 (j' : ℕ))
73	(Finset.mem_univ j)
74	simp only [gap]
75	omega
76	have h3 : 1 * gap I ≤ ((j : ℕ) + 1) * gap I := Nat.mul_le_mul_right _ (by omega)
77	split_ifs <;> omega
78
79	/-- The instance with one blocking client and one blocking day added: the new client's
80	job ends later than every due date of `I` and starts at time `0`, so on an old day it
81	conflicts with every job, and on the new day every job ends at that same time, so all jobs
82	of the new day pairwise conflict. -/
83	def addBlockingDay (I : Instance) : Instance where
84	clients := I.clients + 1
85	days := I.days + 1
86	p i j :=
87	if (j : ℕ) < I.clients then
88	(if (i : ℕ) < I.days then I.pAt i j else I.pAt 0 j)
89	else bound I
90	d i j := if (j : ℕ) < I.clients ∧ (i : ℕ) < I.days then I.dAt i j else bound I
91	p_pos i j := by
92	have h0 := I.pAt_pos (i : ℕ) (j : ℕ)
93	have h1 := I.pAt_pos 0 (j : ℕ)
94	have h2 : 0 < bound I := by simp [bound]
95	split_ifs <;> omega
96	p_le_d i j := by
97	have h1 := I.pAt_le_dAt (i : ℕ) (j : ℕ)
98	have h2 : I.dAt (i : ℕ) (j : ℕ) ≤ bound I := by
99	unfold Instance.dAt bound
100	split_ifs with h h'
101	· have h3 : I.d ⟨(i : ℕ), h⟩ ⟨(j : ℕ), h'⟩ ≤
102	Finset.univ.sup fun j' => I.d ⟨(i : ℕ), h⟩ j' :=
103	Finset.le_sup (Finset.mem_univ _)
104	have h4 : (Finset.univ.sup fun j' => I.d ⟨(i : ℕ), h⟩ j') ≤
105	Finset.univ.sup fun i' => Finset.univ.sup fun j' => I.d i' j' :=
106	Finset.le_sup (f := fun i' => Finset.univ.sup fun j' => I.d i' j') (Finset.mem_univ _)
107	omega
108	· omega
109	· omega
110	have h5 : I.pAt 0 (j : ℕ) ≤ I.dAt 0 (j : ℕ) := I.pAt_le_dAt 0 (j : ℕ)
111	have h6 : I.dAt 0 (j : ℕ) ≤ bound I := by
112	unfold Instance.dAt bound
113	split_ifs with h h'
114	· have h3 : I.d ⟨0, h⟩ ⟨(j : ℕ), h'⟩ ≤ Finset.univ.sup fun j' => I.d ⟨0, h⟩ j' :=
115	Finset.le_sup (Finset.mem_univ _)
116	have h4 : (Finset.univ.sup fun j' => I.d ⟨0, h⟩ j') ≤
117	Finset.univ.sup fun i' => Finset.univ.sup fun j' => I.d i' j' :=
118	Finset.le_sup (f := fun i' => Finset.univ.sup fun j' => I.d i' j') (Finset.mem_univ _)
119	omega
120	· omega
121	· omega
122	split_ifs <;> omega
123
124	/-- The instance without clients and with `m` days. -/
125	def noClients (m : ℕ) : Instance where
126	clients := 0
127	days := m
128	p _ j := j.elim0
129	d _ j := j.elim0
130	p_pos _ j := j.elim0
131	p_le_d _ j := j.elim0
132
133	/-- Adding a conflict-free day raises the attainable fairness by exactly one. -/
134	axiom addFreeDay_correct (I : Instance) (hm : 0 < I.days) (k : ℕ) :
135	I.HasKFairSchedule k ↔ (addFreeDay I).HasKFairSchedule (k + 1)
136
137	/-- Adding a blocking client and a blocking day preserves one-fairness. -/
138	axiom addBlockingDay_correct (I : Instance) (hm : 0 < I.days) :
139	I.HasKFairSchedule 1 ↔ (addBlockingDay I).HasKFairSchedule 1
140
141	/-- The conflict-free day keeps the processing times day-independent. -/
142	axiom addFreeDay_dayIndepP {I : Instance} (h : I.DayIndepP) : (addFreeDay I).DayIndepP
143
144	/-- The blocking day keeps the processing times day-independent. -/
145	axiom addBlockingDay_dayIndepP {I : Instance} (h : I.DayIndepP) :
146	(addBlockingDay I).DayIndepP
147
148	open Classical in
149	/-- The first reduction, as a map on words: a word encoding an instance with `m` days
150	and the fairness parameter `k` is sent to the encoding of the instance with one
151	conflict-free day added and the parameter `k + 1`. -/
152	noncomputable def reduceFreeDay (w : Word) : Word :=
153	if h : ∃ (I : Instance) (k : ℕ), encodeUniform I k = w ∧ 0 < I.days then
154	encodeUniform (addFreeDay h.choose) (h.choose_spec.choose + 1)
155	else rejected
156
157	open Classical in
158	/-- The second reduction, as a map on words: a word encoding an instance with `m` days
159	and the fairness parameter `1` is sent to the encoding of the instance with one blocking
160	client and one blocking day added, with the parameter `1`; an instance without clients is
161	sent to the instance without clients and one more day. -/
162	noncomputable def reduceBlockingDay (w : Word) : Word :=
163	if h : ∃ (I : Instance) (k : ℕ), encodeUniform I k = w ∧ 0 < I.days ∧ k = 1 then
164	if h.choose.clients = 0 then encodeUniform (noClients (h.choose.days + 1)) 1
165	else encodeUniform (addBlockingDay h.choose) 1
166	else rejected
167
168	/-- The first reduction is correct. -/
169	axiom reduceFreeDay_correct (m k : ℕ) (hm : 0 < m) (w : Word) :
170	w ∈ Uniform (fun I k' => I.days = m ∧ k' = k ∧ I.DayIndepP) ↔
171	reduceFreeDay w ∈ Uniform fun I k' => I.days = m + 1 ∧ k' = k + 1 ∧ I.DayIndepP
172
173	/-- The second reduction is correct. -/
174	axiom reduceBlockingDay_correct (m : ℕ) (hm : 0 < m) (w : Word) :
175	w ∈ Uniform (fun I k' => I.days = m ∧ k' = 1 ∧ I.DayIndepP) ↔
176	reduceBlockingDay w ∈ Uniform fun I k' => I.days = m + 1 ∧ k' = 1 ∧ I.DayIndepP
177
178	/-- The first reduction runs in polynomial time. -/
179	axiom reduceFreeDay_polyTime :
180	Nonempty (Turing.TM2ComputableInPolyTime id id reduceFreeDay)
181
182	/-- The second reduction runs in polynomial time. -/
183	axiom reduceBlockingDay_polyTime :
184	Nonempty (Turing.TM2ComputableInPolyTime id id reduceBlockingDay)
185
186	/-- The first step of Corollary 8: hardness for `(m, k)` gives hardness for
187	`(m+1, k+1)`. -/
188	axiom manyOne_freeDay (m k : ℕ) (hm : 0 < m) :
189	ManyOne (Uniform fun I k' => I.days = m ∧ k' = k ∧ I.DayIndepP)
190	(Uniform fun I k' => I.days = m + 1 ∧ k' = k + 1 ∧ I.DayIndepP)
191
192	/-- The second step of Corollary 8: hardness for `(m, 1)` gives hardness for
193	`(m+1, 1)`. -/
194	axiom manyOne_blockingDay (m : ℕ) (hm : 0 < m) :
195	ManyOne (Uniform fun I k' => I.days = m ∧ k' = 1 ∧ I.DayIndepP)
196	(Uniform fun I k' => I.days = m + 1 ∧ k' = 1 ∧ I.DayIndepP)
197
198	end Lax117284.Corollary8
199

Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof

Formalization Notes

The conflict-free day is laid out explicitly: client $j$ receives the interval ending at $(j+1)Q$ , where $Q$ is at least every processing time of the first day. Consecutive clients are then separated by at least $Q$ , so no two of their jobs meet. The source does not say how to lay such a day out.

On the blocking day every job ends at the same time, one later than every due date of the instance, so all of them pairwise conflict; the new client receives that same job on every day, which is why it blocks every old job as well.

The new client is numbered $n$ and the new day $m$ .

An instance without clients is a yes-instance, and its table is empty, so its code does not reflect its number of days. Adding a blocking client to it would add one cell per day, which is exponentially many cells in the length of the code, so the map does not add one: it sends such an instance to the instance without clients and one more day, which is again a yes-instance of the same fairness parameter. Everything else is as in the source.

Builds on

Lax117284.Problems

Used by

Lax117284.Lemma15

From Mathlib

none

Discussion

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

Loading discussion…

Lax Lean Archive

Raising the Number of Days and the Fairness Parameter

Flags

Flag this concept

Natural Language Statement

Corollary

1 `addBlockingDay_correct` proven

2 `addBlockingDay_dayIndepP` proven

3 `addFreeDay_correct` proven

4 `addFreeDay_dayIndepP` proven

5 `manyOne_blockingDay` proven

6 `manyOne_freeDay` proven

7 `reduceBlockingDay_correct` proven

8 `reduceBlockingDay_polyTime` proven

9 `reduceFreeDay_correct` proven

10 `reduceFreeDay_polyTime` proven

In the paper

Lean source view on GitHub

Discussion

Settings