Fair Repetitive Interval Scheduling
Lax117284.Scheduling · concepts/Lax117284/Scheduling.lean · lax-117284
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
An instance consists of clients and days. Every client submits one job on every day: client 's job on day has a processing time and a due date . The schedule is just-in-time, so that job occupies exactly the interval , and two jobs of the same day conflict if their intervals intersect. One machine is available on each day, so a schedule selects, for every day, a set of clients whose day's jobs are pairwise non-conflicting; the jobs of the clients left out are rejected that day.
Write for the indicator that client 's job is executed on day . The objective is the fairness of the schedule, : the decision problem asks, given a fairness parameter , whether some schedule serves every client on at least of the days. In the generalization every client carries its own parameter and must be served on at least days.
Three restrictions of the instance recur. The processing times are day-independent if for all , the due dates are day-independent if for all , and the processing times are unit if throughout.
Concept map
In the paper
- page 1 of this submission's paper
Lean source view on GitHub
| 1 | import Mathlib.Data.Fintype.Card |
| 2 | import Mathlib.Order.Interval.Set.Basic |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Fair Repetitive Interval Scheduling |
| 7 | type: definition |
| 8 | --- |
| 9 | An instance consists of clients and days. Every client submits one job on every |
| 10 | day: client 's job on day has a processing time and a due date |
| 11 | . The schedule is just-in-time, so that job occupies exactly the |
| 12 | interval , and two jobs of the same day *conflict* if their |
| 13 | intervals intersect. One machine is available on each day, so a *schedule* selects, for |
| 14 | every day, a set of clients whose day's jobs are pairwise non-conflicting; the jobs of the |
| 15 | clients left out are rejected that day. |
| 16 | |
| 17 | Write for the indicator that client 's job is executed on day . The |
| 18 | objective is the fairness of the schedule, : the decision problem |
| 19 | asks, given a fairness parameter , |
| 20 | whether some schedule serves every client on at least of the days. In the |
| 21 | generalization every client |
| 22 | carries its own parameter and must be served on at least days. |
| 23 | |
| 24 | Three restrictions of the instance recur. The processing times are *day-independent* if |
| 25 | for all , the due dates are *day-independent* if for all |
| 26 | , and the processing times are *unit* if throughout. |
| 27 | |
| 28 | # Formalization Notes |
| 29 | |
| 30 | Clients and days are numbered rather than abstract finite types: an instance is something |
| 31 | an algorithm is handed as a word, and a word presents its clients and days in an order. |
| 32 | Nothing in the results depends on days carrying an order. |
| 33 | |
| 34 | A job is the set of time points it occupies, and conflict is the intersection of two such |
| 35 | sets being nonempty. Because processing times are positive, this agrees with the |
| 36 | arithmetic condition that each job starts before the other one is due. |
| 37 | |
| 38 | Fairness is stated for per-client parameters from the start and the uniform problem is the |
| 39 | constant case, so that the two problems are one definition rather than two. Both are |
| 40 | stated as the existence of a schedule and not as an optimization, which is the form in |
| 41 | which the source's complexity results are proved. |
| 42 | -/ |
| 43 | |
| 44 | namespace Lax117284.Scheduling |
| 45 | |
| 46 | /-- An instance of fair repetitive interval scheduling: `clients` clients each submitting |
| 47 | one job on each of `days` days, where client `j`'s job on day `i` has processing time |
| 48 | `p i j` and due date `d i j`. A job takes some time and does not start before time `0`. -/ |
| 49 | structure Instance where |
| 50 | /-- The number `n` of clients. -/ |
| 51 | clients : ℕ |
| 52 | /-- The number `m` of days. -/ |
| 53 | days : ℕ |
| 54 | /-- The processing time `p i j` of client `j`'s job on day `i`. -/ |
| 55 | p : Fin days → Fin clients → ℕ |
| 56 | /-- The due date `d i j` of client `j`'s job on day `i`. -/ |
| 57 | d : Fin days → Fin clients → ℕ |
| 58 | /-- Every job takes some time. -/ |
| 59 | p_pos : ∀ i j, 0 < p i j |
| 60 | /-- No job starts before time `0`. -/ |
| 61 | p_le_d : ∀ i j, p i j ≤ d i j |
| 62 | |
| 63 | namespace Instance |
| 64 | |
| 65 | variable (I : Instance) |
| 66 | |
| 67 | /-- The interval `(d i j - p i j, d i j]` occupied by client `j`'s job on day `i`: the job |
| 68 | is completed exactly at its due date. -/ |
| 69 | def job (i : Fin I.days) (j : Fin I.clients) : Set ℕ := |
| 70 | Set.Ioc (I.d i j - I.p i j) (I.d i j) |
| 71 | |
| 72 | /-- Clients `j` and `j'` **conflict on day `i`**: their day-`i` jobs share a time point, so |
| 73 | the machine of that day can execute at most one of them. -/ |
| 74 | def Conflict (i : Fin I.days) (j j' : Fin I.clients) : Prop := |
| 75 | (I.job i j ∩ I.job i j').Nonempty |
| 76 | |
| 77 | /-- A **schedule** names, for each day, the clients whose job is executed that day. -/ |
| 78 | abbrev Schedule := Fin I.days → Finset (Fin I.clients) |
| 79 | |
| 80 | variable {I} |
| 81 | |
| 82 | /-- A schedule is **feasible** if the jobs it executes on any one day are pairwise |
| 83 | non-conflicting. -/ |
| 84 | def Feasible (σ : I.Schedule) : Prop := |
| 85 | ∀ i, (σ i : Set (Fin I.clients)).Pairwise fun j j' => ¬ I.Conflict i j j' |
| 86 | |
| 87 | /-- `∑_i Z_{i,j}`, the number of days on which client `j`'s job is executed. -/ |
| 88 | def served (σ : I.Schedule) (j : Fin I.clients) : ℕ := |
| 89 | (Finset.univ.filter fun i => j ∈ σ i).card |
| 90 | |
| 91 | /-- A schedule is **fair** for the parameters `k` if every client `j` is served on at least |
| 92 | `k j` days. -/ |
| 93 | def Fair (k : Fin I.clients → ℕ) (σ : I.Schedule) : Prop := ∀ j, k j ≤ served σ j |
| 94 | |
| 95 | variable (I) |
| 96 | |
| 97 | /-- **The question of `1 | k_j, rep | min_j ∑_i Z_{i,j}`**: is there a feasible schedule |
| 98 | serving every client `j` on at least `k j` days? -/ |
| 99 | def HasFairSchedule (k : Fin I.clients → ℕ) : Prop := |
| 100 | ∃ σ : I.Schedule, Feasible σ ∧ Fair k σ |
| 101 | |
| 102 | /-- **The question of `1 | rep | min_j ∑_i Z_{i,j}`**: the uniform case, in which every |
| 103 | client carries the same fairness parameter `k`. -/ |
| 104 | def HasKFairSchedule (k : ℕ) : Prop := I.HasFairSchedule fun _ => k |
| 105 | |
| 106 | /-- `p_{i,j} = p_j`: the processing times are **day-independent**. -/ |
| 107 | def DayIndepP : Prop := ∀ i i' j, I.p i j = I.p i' j |
| 108 | |
| 109 | /-- `d_{i,j} = d_j`: the due dates are **day-independent**. -/ |
| 110 | def DayIndepD : Prop := ∀ i i' j, I.d i j = I.d i' j |
| 111 | |
| 112 | /-- The processing time of client `j`'s job on day `i`, read off unnumbered indices and |
| 113 | `1` outside the instance, so that a construction reading another instance need not carry |
| 114 | the proofs that its indices are in range. -/ |
| 115 | def pAt (i j : ℕ) : ℕ := |
| 116 | if h : i < I.days then if h' : j < I.clients then I.p ⟨i, h⟩ ⟨j, h'⟩ else 1 else 1 |
| 117 | |
| 118 | /-- The due date of client `j`'s job on day `i`, and `1` outside the instance. -/ |
| 119 | def dAt (i j : ℕ) : ℕ := |
| 120 | if h : i < I.days then if h' : j < I.clients then I.d ⟨i, h⟩ ⟨j, h'⟩ else 1 else 1 |
| 121 | |
| 122 | theorem pAt_pos (i j : ℕ) : 0 < I.pAt i j := by |
| 123 | unfold pAt |
| 124 | split |
| 125 | · split |
| 126 | · exact I.p_pos _ _ |
| 127 | · exact Nat.zero_lt_one |
| 128 | · exact Nat.zero_lt_one |
| 129 | |
| 130 | theorem pAt_le_dAt (i j : ℕ) : I.pAt i j ≤ I.dAt i j := by |
| 131 | unfold pAt dAt |
| 132 | split |
| 133 | · split |
| 134 | · exact I.p_le_d _ _ |
| 135 | · exact Nat.le_refl 1 |
| 136 | · exact Nat.le_refl 1 |
| 137 | |
| 138 | @[simp] theorem pAt_coe (i : Fin I.days) (j : Fin I.clients) : I.pAt i j = I.p i j := by |
| 139 | simp [pAt, i.isLt, j.isLt] |
| 140 | |
| 141 | @[simp] theorem dAt_coe (i : Fin I.days) (j : Fin I.clients) : I.dAt i j = I.d i j := by |
| 142 | simp [dAt, i.isLt, j.isLt] |
| 143 | |
| 144 | /-- Whether clients `j` and `j'` conflict on day `i`, read off unnumbered indices and in |
| 145 | the arithmetic form: each of the two jobs starts before the other one is due. It is this |
| 146 | form of the condition that a construction can decide. -/ |
| 147 | def ConflictAt (i j j' : ℕ) : Prop := |
| 148 | I.dAt i j - I.pAt i j < I.dAt i j' ∧ I.dAt i j' - I.pAt i j' < I.dAt i j |
| 149 | |
| 150 | instance (i j j' : ℕ) : Decidable (I.ConflictAt i j j') := by |
| 151 | unfold ConflictAt; infer_instance |
| 152 | |
| 153 | /-- **The arithmetic and the geometric form of conflict agree.** -/ |
| 154 | theorem conflictAt_iff (i : Fin I.days) (j j' : Fin I.clients) : |
| 155 | I.ConflictAt i j j' ↔ I.Conflict i j j' := by |
| 156 | have h1 := I.p_pos i j |
| 157 | have h2 := I.p_le_d i j |
| 158 | have h3 := I.p_pos i j' |
| 159 | have h4 := I.p_le_d i j' |
| 160 | simp only [ConflictAt, Conflict, job, pAt_coe, dAt_coe, Set.Nonempty, Set.mem_inter_iff, |
| 161 | Set.mem_Ioc] |
| 162 | constructor |
| 163 | · intro h |
| 164 | exact ⟨min (I.d i j) (I.d i j'), by omega, by omega⟩ |
| 165 | · rintro ⟨t, ⟨h5, h6⟩, h7, h8⟩ |
| 166 | omega |
| 167 | |
| 168 | /-- `p_{i,j} = 1`: the processing times are **unit**. -/ |
| 169 | def UnitP : Prop := ∀ i j, I.p i j = 1 |
| 170 | |
| 171 | /-- No two jobs of a day conflict, so every client can be served on every day. -/ |
| 172 | def ConflictFree : Prop := ∀ i, ∀ j j', j ≠ j' → ¬ I.Conflict i j j' |
| 173 | |
| 174 | end Instance |
| 175 | |
| 176 | end Lax117284.Scheduling |
| 177 |
Formalization Notes
Clients and days are numbered rather than abstract finite types: an instance is something an algorithm is handed as a word, and a word presents its clients and days in an order. Nothing in the results depends on days carrying an order.
A job is the set of time points it occupies, and conflict is the intersection of two such sets being nonempty. Because processing times are positive, this agrees with the arithmetic condition that each job starts before the other one is due.
Fairness is stated for per-client parameters from the start and the uniform problem is the constant case, so that the two problems are one definition rather than two. Both are stated as the existence of a schedule and not as an optimization, which is the form in which the source's complexity results are proved.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments