Lax Lean Archive

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

Just-in-Time Scheduling on Unrelated Machines as Day-Independent Due Dates

Lax117284.Theorem11 · concepts/Lax117284/Theorem11.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

    Theorem

    Theorem 11. The problem 1∣rep, di,j=dj∣min⁡j∑iZi,j1 \mid \mathrm{rep},\, d_{i,j} = d_j \mid \min_j \sum_i Z_{i,j} is NP-hard.

    An instance of R∥∑jZjR \parallel \sum_j Z_j is read as an instance of fair repetitive interval scheduling by taking its jobs as clients and its machines as days: client jj's job on day ii has the processing time of job jj on machine ii and the due date of job jj, which does not depend on the day. Executing every job just in time on some machine is then the same thing as serving every client on at least one day, so the constructed instance is a yes-instance at k=1k = 1 exactly when the given one admits an all-just-in-time schedule. Since R∥∑jZjR \parallel \sum_j Z_j is NP-hard, so is the problem with day-independent due dates.

    Concept map
    8 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.

    1 allJIT_manyOne_dayIndepD proven

    2 correct proven

    3 inst_dayIndepD proven

    4 reduce_correct proven

    5 reduce_polyTime proven

    In the paper

    • page 2 of this submission's paper

    Lean source view on GitHub

    1import Lax117284.JustInTime
    2import Lax117284.Problems
    3
    4/-!
    5---
    6title: Just-in-Time Scheduling on Unrelated Machines as Day-Independent Due Dates
    7type: theorem
    8---
    9**Theorem 11.** The problem
    101∣rep, di,j=dj∣min⁡j∑iZi,j1 \mid \mathrm{rep},\, d_{i,j} = d_j \mid \min_j \sum_i Z_{i,j} is NP-hard.
    11
    12An instance of R∥∑jZjR \parallel \sum_j Z_j is read as an instance of fair repetitive interval
    13scheduling by taking its jobs as clients and its machines as days: client jj's job on day
    14ii has the processing time of job jj on machine ii and the due date of job jj, which
    15does not depend on the day. Executing every job just in time on some machine is then the
    16same thing as serving every client on at least one day, so the constructed instance is a
    17yes-instance at k=1k = 1 exactly when the given one admits an all-just-in-time schedule.
    18Since R∥∑jZjR \parallel \sum_j Z_j is NP-hard, so is the problem with day-independent due dates.
    19
    20# Formalization Notes
    21
    22The two models are already the same up to naming, the whole content of the reduction being
    23that both ask for a partition of intervals ending at fixed times. The construction is
    24therefore a renaming, and what has to be checked is that it is one.
    25-/
    26
    27namespace Lax117284.Theorem11
    28
    29open Lax117284.Scheduling Lax117284.Problems Lax434930.PolynomialTime
    30open Lax429075.Reductions
    31
    32/-- **The instance of Theorem 11**: clients are jobs, days are machines, the due date of a
    33client is that of its job and so does not depend on the day. -/
    34def inst (R : JustInTime.Instance) : Instance where
    35 clients := R.jobs
    36 days := R.machines
    37 p i j := R.p i j
    38 d _ j := R.d j
    39 p_pos := R.p_pos
    40 p_le_d := R.p_le_d
    41
    42/-- **The constructed instance has day-independent due dates.** -/
    43axiom inst_dayIndepD (R : JustInTime.Instance) : (inst R).DayIndepD
    44
    45/-- **The construction is correct**: every job can be executed just in time exactly when
    46every client can be served on at least one day. -/
    47axiom correct (R : JustInTime.Instance) :
    48 R.AllJustInTime ↔ (inst R).HasKFairSchedule 1
    49
    50open Classical in
    51/-- **The reduction**, as a map on words: a word encoding an instance of
    52`R || ∑_j Z_j` is sent to the encoding of the constructed instance with the fairness
    53parameter `1`, and every other word to the rejected word. -/
    54noncomputable def reduce (w : Word) : Word :=
    55 if h : ∃ R : JustInTime.Instance, JustInTime.encodeInstance R = w then
    56 encodeUniform (inst h.choose) 1
    57 else rejected
    58
    59/-- **The reduction is correct.** -/
    60axiom reduce_correct (w : Word) :
    61 w ∈ JustInTime.AllJIT ↔ reduce w ∈ Uniform fun I _ => I.DayIndepD
    62
    63/-- **The reduction runs in polynomial time.** -/
    64axiom reduce_polyTime : Nonempty (Turing.TM2ComputableInPolyTime id id reduce)
    65
    66/-- **Theorem 11.** `R || ∑_j Z_j` reduces in polynomial time to the problem on the
    67instances with day-independent due dates. -/
    68axiom allJIT_manyOne_dayIndepD :
    69 ManyOne JustInTime.AllJIT (Uniform fun I _ => I.DayIndepD)
    70
    71end Lax117284.Theorem11
    72
    Show ProofShow ProofShow ProofShow ProofShow Proof
    Formalization Notes

    The two models are already the same up to naming, the whole content of the reduction being that both ask for a partition of intervals ending at fixed times. The construction is therefore a renaming, and what has to be checked is that it is one.

    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…