Lax Lean Archive

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

Day-Independent Due Dates

Lax117284.Theorem3 · concepts/Lax117284/Theorem3.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 3. 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. It is solvable in polynomial time under either of two additional restrictions: (i) the number mm of days is a constant; (ii) the processing times are day-independent as well.

    Hardness comes from the problem of maximizing the number of just-in-time jobs on unrelated parallel machines. Under (i) a dynamic program over the clients in order of their due dates decides the problem, carrying for each day the time at which its machine is next free. Under (ii) every day has the same conflict graph, and a kk-fair schedule exists exactly when kk times the chromatic number of that graph is at most mm.

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

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

    1 uniform_dayIndepD_dayIndepP_mem_P proven

    2 uniform_dayIndepD_days_mem_P proven

    3 uniform_dayIndepD_npHard proven

    Lean source view on GitHub

    1import Lax117284.Problems
    2
    3/-!
    4---
    5title: Day-Independent Due Dates
    6type: theorem
    7---
    8**Theorem 3.** The problem
    91∣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. It is
    10solvable in polynomial time under either of two additional restrictions: (i) the number mm
    11of days is a constant; (ii) the processing times are day-independent as well.
    12
    13Hardness comes from the problem of maximizing the number of just-in-time jobs on unrelated
    14parallel machines. Under (i) a dynamic program over the clients in order of their due dates
    15decides the problem, carrying for each day the time at which its machine is next free.
    16Under (ii) every day has the same conflict graph, and a kk-fair schedule exists exactly
    17when kk times the chromatic number of that graph is at most mm.
    18
    19# Formalization Notes
    20
    21Restriction (i) is a constant of the slice rather than part of the input, so the claim is
    22one language per number of days. This is what "mm is a constant" means: the algorithm may
    23depend on mm, and its running time is polynomial for each fixed mm while the exponent may
    24grow with mm.
    25-/
    26
    27namespace Lax117284.Theorem3
    28
    29open Lax117284.Scheduling Lax117284.Problems Lax434930.PolynomialTime
    30
    31/-- **Theorem 3, hardness.** With day-independent due dates the problem remains
    32NP-hard. -/
    33axiom uniform_dayIndepD_npHard : NPHard (Uniform fun I _ => I.DayIndepD)
    34
    35/-- **Theorem 3(i).** With day-independent due dates and a fixed number `m` of days the
    36problem is solvable in polynomial time. -/
    37axiom uniform_dayIndepD_days_mem_P (m : ℕ) :
    38 Uniform (fun I _ => I.DayIndepD ∧ I.days = m) ∈ P
    39
    40/-- **Theorem 3(ii).** With day-independent due dates and day-independent processing times
    41the problem is solvable in polynomial time. -/
    42axiom uniform_dayIndepD_dayIndepP_mem_P :
    43 Uniform (fun I _ => I.DayIndepD ∧ I.DayIndepP) ∈ P
    44
    45end Lax117284.Theorem3
    46
    Show ProofShow ProofShow Proof
    Formalization Notes

    Restriction (i) is a constant of the slice rather than part of the input, so the claim is one language per number of days. This is what "mm is a constant" means: the algorithm may depend on mm, and its running time is polynomial for each fixed mm while the exponent may grow with mm.

    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…