Lax Lean Archive

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

Just-in-Time Scheduling on Unrelated Parallel Machines

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

proven

Loading review…

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 of R∥∑jZjR \parallel \sum_j Z_j consists of nn jobs and mm unrelated parallel machines. Job jj has a due date djd_j and a processing time pi,jp_{i,j} on machine ii. A job is just in time if it is executed on some machine and completes exactly at its due date, so that, when assigned to machine ii, it occupies the interval (dj−pi,j, dj](d_j - p_{i,j},\, d_j] of that machine; two jobs assigned to the same machine may not overlap. The objective ∑jZj\sum_j Z_j counts the jobs that are just in time, and the decision problem asks whether all nn jobs can be just in time at once. It is NP-hard.

    Concept map
    7 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax117284.Problems
    2
    3/-!
    4---
    5title: Just-in-Time Scheduling on Unrelated Parallel Machines
    6type: definition
    7---
    8An instance of R∥∑jZjR \parallel \sum_j Z_j consists of nn jobs and mm unrelated parallel
    9machines. Job jj has a due date djd_j and a processing time pi,jp_{i,j} on machine ii. A job
    10is *just in time* if it is executed on some machine and completes exactly at its due date,
    11so that, when assigned to machine ii, it occupies the interval
    12(dj−pi,j, dj](d_j - p_{i,j},\, d_j] of that machine; two jobs assigned to the same machine may not
    13overlap. The objective ∑jZj\sum_j Z_j counts the jobs that are just in time, and the decision
    14problem asks whether all nn jobs can be just in time at once. It is NP-hard.
    15
    16# Formalization Notes
    17
    18The problem is stated at the maximum value of the objective, which is the form the
    19reduction into fair repetitive interval scheduling uses and the form in which it is hard: a
    20schedule is an assignment of every job to a machine such that no two jobs on a machine
    21overlap.
    22
    23Due dates do not depend on the machine, and processing times do, which is what makes the
    24machines unrelated.
    25-/
    26
    27namespace Lax117284.JustInTime
    28
    29open Lax434930.PolynomialTime
    30
    31/-- An instance of `R || ∑_j Z_j`: `jobs` jobs and `machines` unrelated machines, where job
    32`j` has due date `d j` and processing time `p i j` on machine `i`. -/
    33structure Instance where
    34 /-- The number `n` of jobs. -/
    35 jobs : ℕ
    36 /-- The number `m` of machines. -/
    37 machines : ℕ
    38 /-- The processing time `p i j` of job `j` on machine `i`. -/
    39 p : Fin machines → Fin jobs → ℕ
    40 /-- The due date `d j` of job `j`, the same on every machine. -/
    41 d : Fin jobs → ℕ
    42 /-- Every job takes some time. -/
    43 p_pos : ∀ i j, 0 < p i j
    44 /-- No job starts before time `0`. -/
    45 p_le_d : ∀ i j, p i j ≤ d j
    46
    47namespace Instance
    48
    49variable (R : Instance)
    50
    51/-- The interval `(d j - p i j, d j]` occupied by job `j` when it is executed just in time
    52on machine `i`. -/
    53def job (i : Fin R.machines) (j : Fin R.jobs) : Set ℕ :=
    54 Set.Ioc (R.d j - R.p i j) (R.d j)
    55
    56/-- Jobs `j` and `j'` **overlap on machine `i`**: executing both just in time on that
    57machine would have them share a time point. -/
    58def Overlap (i : Fin R.machines) (j j' : Fin R.jobs) : Prop :=
    59 (R.job i j ∩ R.job i j').Nonempty
    60
    61/-- **The question of `R || ∑_j Z_j` at its maximum value**: can every job be executed just
    62in time, that is, is there an assignment of the jobs to machines under which no two jobs of
    63a machine overlap? -/
    64def AllJustInTime : Prop :=
    65 ∃ f : Fin R.jobs → Fin R.machines,
    66 ∀ j j', j ≠ j' → f j = f j' → ¬ R.Overlap (f j) j j'
    67
    68end Instance
    69
    70/-- An instance as a binary word: the number of jobs, the number of machines, the due
    71dates, and then the processing times machine by machine. -/
    72def encodeInstance (R : Instance) : Word :=
    73 Problems.encodeNat R.jobs ++ Problems.encodeNat R.machines ++
    74 ((List.finRange R.jobs).flatMap fun j => Problems.encodeNat (R.d j)) ++
    75 (List.finRange R.machines).flatMap fun i =>
    76 (List.finRange R.jobs).flatMap fun j => Problems.encodeNat (R.p i j)
    77
    78/-- **`R || ∑_j Z_j`**, as a language. -/
    79def AllJIT : Language :=
    80 {w | ∃ R : Instance, encodeInstance R = w ∧ R.AllJustInTime}
    81
    82/-- **`R || ∑_j Z_j` is NP-hard.** -/
    83axiom allJIT_npHard : Problems.NPHard AllJIT
    84
    85end Lax117284.JustInTime
    86
    Show Proof
    Formalization Notes

    The problem is stated at the maximum value of the objective, which is the form the reduction into fair repetitive interval scheduling uses and the form in which it is hard: a schedule is an assignment of every job to a machine such that no two jobs on a machine overlap.

    Due dates do not depend on the machine, and processing times do, which is what makes the machines unrelated.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…