Per-Client Fairness Parameters Reduce to a Uniform One

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

proven

Loading review…

Natural Language Statement

Lemma

Lemma 15. There is a polynomial-time reduction from $1 \mid k_j, \mathrm{rep} \mid \min_j \sum_i Z_{i,j}$ to $1 \mid \mathrm{rep} \mid \min_j \sum_i Z_{i,j}$ which increases the treewidth of the overall conflict graph by at most $2$ .

Let $I$ have $n$ clients, $m$ days and fairness parameters $k_1, \ldots, k_n$ with $k_j \le m$ . Append another $m$ days, add two clients $c^-$ and $c^+$ , and ask for the uniform parameter $m$ . The jobs of $c^-$ and $c^+$ coincide on every day, so at most one of them runs on any day and, being asked for $m$ of the $2m$ days, each of them runs on exactly one day of every pair. Their common job occupies a stretch of time later than every due date of $I$ , so it conflicts with no original job on the original days. On the additional days each original client $j$ has a job of its own, which is placed inside that stretch on $k_j$ of them and after it on the others. A client of $I$ can therefore be served on all but $k_j$ of the additional days, and needs $k_j$ of the original days to reach $m$ — which is its original requirement.

The jobs the original clients receive on the additional days are pairwise disjoint, so the construction adds no edge between original clients: the overall conflict graph grows only by the two new vertices, and its treewidth by at most $2$ .

Concept map

10 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

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

In the paper

page 4 of this submission's paper

Lean source view on GitHub

Show types on hover

1	import Lax117284.ConflictGraph
2	import Lax117284.Corollary8
3	import Lax117284.Problems
4
5	/-!
6	---
7	title: Per-Client Fairness Parameters Reduce to a Uniform One
8	type: lemma
9	---
10	Lemma 15. There is a polynomial-time reduction from
11	$1 \mid k_j, \mathrm{rep} \mid \min_j \sum_i Z_{i,j}$ to
12	$1 \mid \mathrm{rep} \mid \min_j \sum_i Z_{i,j}$ which increases the treewidth of the
13	overall conflict graph by at most $2$ .
14
15	Let $I$ have $n$ clients, $m$ days and fairness parameters $k_1, \ldots, k_n$ with
16	$k_j \le m$ . Append another $m$ days, add two clients $c^-$ and $c^+$ , and ask for the
17	uniform parameter $m$ . The jobs of $c^-$ and $c^+$ coincide on every day, so at most one of
18	them runs on any day and, being asked for $m$ of the $2m$ days, each of them runs on
19	exactly one day of every pair. Their common job occupies a stretch of time later than every
20	due date of $I$ , so it conflicts with no original job on the original days. On the
21	additional days each original client $j$ has a job of its own, which is placed inside that
22	stretch on $k_j$ of them and after it on the others. A client of $I$ can therefore be served
23	on all but $k_j$ of the additional days, and needs $k_j$ of the original days to reach $m$ —
24	which is its original requirement.
25
26	The jobs the original clients receive on the additional days are pairwise disjoint, so the
27	construction adds no edge between original clients: the overall conflict graph grows only by
28	the two new vertices, and its treewidth by at most $2$ .
29
30	# Formalization Notes
31
32	The $k_j$ days on which client $j$ is blocked are the first $k_j$ of the additional days.
33	The source takes an arbitrary set of that size; taking the first ones makes the construction
34	a function of the instance and its parameters alone, which is what a reduction has to be.
35
36	The two new clients are numbered $n$ and $n+1$ , and day $m + i$ of the construction is the
37	additional copy of day $i$ . The private job of client $j$ ends at a time offset by $j+1$
38	inside a stretch of length $n+1$ , so distinct clients receive disjoint jobs and every such
39	job lies inside the stretch the two new clients occupy.
40
41	Correctness is stated for instances whose parameters do not exceed the number of days, which
42	is the only case that can be a yes-instance. The three statements separate what is
43	asserted: the combinatorial content of the construction, the treewidth of its output, and
44	the running time of the map on words. The lemma itself follows from them.
45
46	An instance without clients is a yes-instance whatever its parameters, and its table is empty, so
47	its code does not reflect its number of days: the construction, which has four cells for every
48	day, would write exponentially many in the length of the code. The map therefore sends such an
49	instance to the instance without clients and without days with the parameter `0`, which is
50	again a yes-instance.
51
52	The reduction is correct on all words, and the treewidth is not part of that statement: the
53	treewidth of the input instance is not something the map checks, and the construction
54	preserves the answer whatever it is. What the construction does to the treewidth is
55	`treewidth_le`; a reduction that starts from instances of treewidth at most `4`, such as the
56	one of Lemma 14, therefore lands among those of treewidth at most `6`.
57	-/
58
59	namespace Lax117284.Lemma15
60
61	open Lax117284.Scheduling Lax117284.Problems Lax434930.PolynomialTime
62	open Lax429075.Reductions
63
64	/-- A time not before any due date of `I`. -/
65	def dmax (I : Instance) : ℕ := Finset.univ.sup fun i => Finset.univ.sup fun j => I.d i j
66
67	/-- The length of the job the two new clients share: longer than the stretch of private
68	jobs, so that it contains all of them. -/
69	def span (I : Instance) : ℕ := I.clients + 1
70
71	/-- The instance of Lemma 15: `2m` days, the `n` clients of `I` together with two new
72	ones, and the uniform fairness parameter `m`. -/
73	def inst (I : Instance) (k : Fin I.clients → ℕ) : Instance where
74	clients := I.clients + 2
75	days := 2 * I.days
76	p i j :=
77	if (j : ℕ) < I.clients then
78	(if (i : ℕ) < I.days then I.pAt i j else 1)
79	else span I
80	d i j :=
81	if hj : (j : ℕ) < I.clients then
82	(if (i : ℕ) < I.days then I.dAt i j
83	else if (i : ℕ) - I.days < k ⟨j, hj⟩ then dmax I + ((j : ℕ) + 1)
84	else dmax I + span I + ((j : ℕ) + 1))
85	else dmax I + span I
86	p_pos i j := by
87	have h0 := I.pAt_pos (i : ℕ) (j : ℕ)
88	have hs : span I = I.clients + 1 := rfl
89	split_ifs <;> omega
90	p_le_d i j := by
91	have h1 := I.pAt_le_dAt (i : ℕ) (j : ℕ)
92	have hs : span I = I.clients + 1 := rfl
93	split_ifs <;> omega
94
95	/-- The construction is correct: the instance it produces admits a schedule serving
96	every client on `m` of its `2m` days exactly when the original instance admits one serving
97	every client `j` on `k j` of its `m` days. -/
98	axiom correct (I : Instance) (k : Fin I.clients → ℕ) (hk : ∀ j, k j ≤ I.days) :
99	I.HasFairSchedule k ↔ (inst I k).HasKFairSchedule I.days
100
101	/-- **The construction raises the treewidth of the overall conflict graph by at most
102	two.** -/
103	axiom treewidth_le (I : Instance) (k : Fin I.clients → ℕ) :
104	ConflictGraph.treewidth (inst I k) ≤ ConflictGraph.treewidth I + 2
105
106	open Classical in
107	/-- The reduction, as a map on words: a word encoding an instance with per-client
108	parameters not exceeding its number of days is sent to the encoding of the constructed
109	instance with the parameter `m`, an instance without clients to a fixed yes-instance, and
110	every other word to the rejected word. -/
111	noncomputable def reduce (w : Word) : Word :=
112	if h : ∃ (I : Instance) (k : Fin I.clients → ℕ),
113	encodePerClient I k = w ∧ ∀ j, k j ≤ I.days then
114	if h.choose.clients = 0 then encodeUniform (Corollary8.noClients 0) 0
115	else encodeUniform (inst h.choose h.choose_spec.choose) h.choose.days
116	else rejected
117
118	/-- The reduction is correct. -/
119	axiom reduce_correct (w : Word) :
120	w ∈ PerClient (fun I k => ∀ j, k j ≤ I.days) ↔ reduce w ∈ Uniform any
121
122	/-- The reduction runs in polynomial time. -/
123	axiom reduce_polyTime : Nonempty (Turing.TM2ComputableInPolyTime id id reduce)
124
125	/-- Lemma 15. The per-client problem reduces in polynomial time to the uniform problem;
126	by `treewidth_le` the reduction raises the treewidth of the overall conflict graph by at
127	most two. -/
128	axiom perClient_manyOne_uniform :
129	ManyOne (PerClient fun I k => ∀ j, k j ≤ I.days) (Uniform any)
130
131	end Lax117284.Lemma15
132

Show ProofShow ProofShow ProofShow ProofShow Proof

Formalization Notes

The $k_j$ days on which client $j$ is blocked are the first $k_j$ of the additional days. The source takes an arbitrary set of that size; taking the first ones makes the construction a function of the instance and its parameters alone, which is what a reduction has to be.

The two new clients are numbered $n$ and $n+1$ , and day $m + i$ of the construction is the additional copy of day $i$ . The private job of client $j$ ends at a time offset by $j+1$ inside a stretch of length $n+1$ , so distinct clients receive disjoint jobs and every such job lies inside the stretch the two new clients occupy.

Correctness is stated for instances whose parameters do not exceed the number of days, which is the only case that can be a yes-instance. The three statements separate what is asserted: the combinatorial content of the construction, the treewidth of its output, and the running time of the map on words. The lemma itself follows from them.

An instance without clients is a yes-instance whatever its parameters, and its table is empty, so its code does not reflect its number of days: the construction, which has four cells for every day, would write exponentially many in the length of the code. The map therefore sends such an instance to the instance without clients and without days with the parameter $0$ , which is again a yes-instance.

The reduction is correct on all words, and the treewidth is not part of that statement: the treewidth of the input instance is not something the map checks, and the construction preserves the answer whatever it is. What the construction does to the treewidth is $treewidth_le$ ; a reduction that starts from instances of treewidth at most $4$ , such as the one of Lemma 14, therefore lands among those of treewidth at most $6$ .

Builds on

Used by

none

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

Per-Client Fairness Parameters Reduce to a Uniform One

Flags

Flag this concept

Natural Language Statement

Lemma

1 `correct` proven

2 `perClient_manyOne_uniform` proven

3 `reduce_correct` proven

4 `reduce_polyTime` proven

5 `treewidth_le` proven

In the paper

Lean source view on GitHub

Discussion

Settings

Your comments

Per-Client Fairness Parameters Reduce to a Uniform One

Natural Language Statement

Lemma

1 correct proven

2 perClient_manyOne_uniform proven

3 reduce_correct proven

4 reduce_polyTime proven

5 treewidth_le proven

In the paper

Lean source view on GitHub

Discussion

1 `correct` proven

2 `perClient_manyOne_uniform` proven

3 `reduce_correct` proven

4 `reduce_polyTime` proven

5 `treewidth_le` proven