Lax Lean Archive

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

Day-Independent Processing Times

Lax117284.Theorem2 · concepts/Lax117284/Theorem2.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 2. The problem 1∣rep, pi,j=pj∣min⁡j∑iZi,j1 \mid \mathrm{rep},\, p_{i,j} = p_j \mid \min_j \sum_i Z_{i,j} is NP-hard. It is solvable in polynomial time if pj=1p_j = 1 for every client jj.

    Hardness needs no more than three days and k=1k = 1, and the instances the reduction produces have all their processing times equal, which is a special case of day-independence. With unit processing times two jobs of a day conflict exactly when they have the same due date, and the problem becomes one of bipartite matching.

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

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

    1 uniform_dayIndepP_npHard proven

    2 uniform_unitP_mem_P proven

    In the paper

    • page 2 of this submission's paper

    Lean source view on GitHub

    1import Lax117284.Problems
    2
    3/-!
    4---
    5title: Day-Independent Processing Times
    6type: theorem
    7---
    8**Theorem 2.** The problem
    91∣rep, pi,j=pj∣min⁡j∑iZi,j1 \mid \mathrm{rep},\, p_{i,j} = p_j \mid \min_j \sum_i Z_{i,j} is NP-hard. It is
    10solvable in polynomial time if pj=1p_j = 1 for every client jj.
    11
    12Hardness needs no more than three days and k=1k = 1, and the instances the reduction
    13produces have all their processing times equal, which is a special case of
    14day-independence. With unit processing times two jobs of a day conflict exactly when they
    15have the same due date, and the problem becomes one of bipartite matching.
    16
    17# Formalization Notes
    18
    19The hard half is stated for the class of instances whose processing times are
    20day-independent, and not for the smaller class of instances in which all processing times
    21are equal, because that is the restriction the source names. That the reduction lands in
    22the smaller class as well is a statement about the construction.
    23-/
    24
    25namespace Lax117284.Theorem2
    26
    27open Lax117284.Scheduling Lax117284.Problems Lax434930.PolynomialTime
    28
    29/-- **Theorem 2, hardness.** With day-independent processing times the problem remains
    30NP-hard. -/
    31axiom uniform_dayIndepP_npHard : NPHard (Uniform fun I _ => I.DayIndepP)
    32
    33/-- **Theorem 2, tractability.** With unit processing times the problem is solvable in
    34polynomial time. -/
    35axiom uniform_unitP_mem_P : Uniform (fun I _ => I.UnitP) ∈ P
    36
    37end Lax117284.Theorem2
    38
    Show ProofShow Proof
    Formalization Notes

    The hard half is stated for the class of instances whose processing times are day-independent, and not for the smaller class of instances in which all processing times are equal, because that is the restriction the source names. That the reduction lands in the smaller class as well is a statement about the construction.

    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…