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

Fair Repetitive Interval Scheduling

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

definition

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

    Definition

    An instance consists of nn clients and mm days. Every client submits one job on every day: client jj's job on day ii has a processing time pi,j≥1p_{i,j} \ge 1 and a due date di,j≥pi,jd_{i,j} \ge p_{i,j}. The schedule is just-in-time, so that job occupies exactly the interval (di,j−pi,j, di,j](d_{i,j} - p_{i,j},\, d_{i,j}], 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 Zi,jZ_{i,j} for the indicator that client jj's job is executed on day ii. The objective is the fairness of the schedule, min⁡j∑iZi,j\min_j \sum_i Z_{i,j}: the decision problem 1∣rep∣min⁡j∑iZi,j1 \mid \mathrm{rep} \mid \min_j \sum_i Z_{i,j} asks, given a fairness parameter kk, whether some schedule serves every client on at least kk of the mm days. In the generalization 1∣kj,rep∣min⁡j∑iZi,j1 \mid k_j, \mathrm{rep} \mid \min_j \sum_i Z_{i,j} every client jj carries its own parameter kjk_j and must be served on at least kjk_j days.

    Three restrictions of the instance recur. The processing times are day-independent if pi,j=pjp_{i,j} = p_j for all ii, the due dates are day-independent if di,j=djd_{i,j} = d_j for all ii, and the processing times are unit if pi,j=1p_{i,j} = 1 throughout.

    Concept map
    1 concept; 22 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 1 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Data.Fintype.Card
    2import Mathlib.Order.Interval.Set.Basic
    3
    4/-!
    5---
    6title: Fair Repetitive Interval Scheduling
    7type: definition
    8---
    9An instance consists of nn clients and mm days. Every client submits one job on every
    10day: client jj's job on day ii has a processing time pi,j≥1p_{i,j} \ge 1 and a due date
    11di,j≥pi,jd_{i,j} \ge p_{i,j}. The schedule is just-in-time, so that job occupies exactly the
    12interval (di,j−pi,j, di,j](d_{i,j} - p_{i,j},\, d_{i,j}], and two jobs of the same day *conflict* if their
    13intervals intersect. One machine is available on each day, so a *schedule* selects, for
    14every day, a set of clients whose day's jobs are pairwise non-conflicting; the jobs of the
    15clients left out are rejected that day.
    16
    17Write Zi,jZ_{i,j} for the indicator that client jj's job is executed on day ii. The
    18objective is the fairness of the schedule, min⁡j∑iZi,j\min_j \sum_i Z_{i,j}: the decision problem
    191∣rep∣min⁡j∑iZi,j1 \mid \mathrm{rep} \mid \min_j \sum_i Z_{i,j} asks, given a fairness parameter kk,
    20whether some schedule serves every client on at least kk of the mm days. In the
    21generalization 1∣kj,rep∣min⁡j∑iZi,j1 \mid k_j, \mathrm{rep} \mid \min_j \sum_i Z_{i,j} every client jj
    22carries its own parameter kjk_j and must be served on at least kjk_j days.
    23
    24Three restrictions of the instance recur. The processing times are *day-independent* if
    25pi,j=pjp_{i,j} = p_j for all ii, the due dates are *day-independent* if di,j=djd_{i,j} = d_j for all
    26ii, and the processing times are *unit* if pi,j=1p_{i,j} = 1 throughout.
    27
    28# Formalization Notes
    29
    30Clients and days are numbered rather than abstract finite types: an instance is something
    31an algorithm is handed as a word, and a word presents its clients and days in an order.
    32Nothing in the results depends on days carrying an order.
    33
    34A job is the set of time points it occupies, and conflict is the intersection of two such
    35sets being nonempty. Because processing times are positive, this agrees with the
    36arithmetic condition that each job starts before the other one is due.
    37
    38Fairness is stated for per-client parameters from the start and the uniform problem is the
    39constant case, so that the two problems are one definition rather than two. Both are
    40stated as the existence of a schedule and not as an optimization, which is the form in
    41which the source's complexity results are proved.
    42-/
    43
    44namespace Lax117284.Scheduling
    45
    46/-- An instance of fair repetitive interval scheduling: `clients` clients each submitting
    47one 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`. -/
    49structure 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
    63namespace Instance
    64
    65variable (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
    68is completed exactly at its due date. -/
    69def 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
    73the machine of that day can execute at most one of them. -/
    74def 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. -/
    78abbrev Schedule := Fin I.days → Finset (Fin I.clients)
    79
    80variable {I}
    81
    82/-- A schedule is **feasible** if the jobs it executes on any one day are pairwise
    83non-conflicting. -/
    84def 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. -/
    88def 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. -/
    93def Fair (k : Fin I.clients → ℕ) (σ : I.Schedule) : Prop := ∀ j, k j ≤ served σ j
    94
    95variable (I)
    96
    97/-- **The question of `1 | k_j, rep | min_j ∑_i Z_{i,j}`**: is there a feasible schedule
    98serving every client `j` on at least `k j` days? -/
    99def 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
    103client carries the same fairness parameter `k`. -/
    104def HasKFairSchedule (k : ℕ) : Prop := I.HasFairSchedule fun _ => k
    105
    106/-- `p_{i,j} = p_j`: the processing times are **day-independent**. -/
    107def 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**. -/
    110def 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
    114the proofs that its indices are in range. -/
    115def 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. -/
    119def 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
    122theorem 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
    130theorem 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
    145the arithmetic form: each of the two jobs starts before the other one is due. It is this
    146form of the condition that a construction can decide. -/
    147def 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
    150instance (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.** -/
    154theorem 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**. -/
    169def 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. -/
    172def ConflictFree : Prop := ∀ i, ∀ j j', j ≠ j' → ¬ I.Conflict i j j'
    173
    174end Instance
    175
    176end 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.

    Loading discussion…