Theorem 1

Lax496464.Theorem1 · concepts/Lax496464/Theorem1.lean · lax-496464

proven

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

    Theorem

    Just-in-time scheduling in a two-stage flexible flow shop is strongly NP-hard, already when every weight is one.

    The reduction is from Hitting Set. For 2≤k≤n2 \le k \le n, the shop built from a family F1,…,FmF_1, \dots, F_m over {1,…,n}\{1, \dots, n\} admits R⋅m⋅(2k−1)R \cdot m \cdot (2k-1) just-in-time jobs exactly when the family has a hitting set of size kk.

    One direction schedules: a hitting set assigns to each of its kk elements one machine, which runs in every epoch either the selection job of the element that hits that epoch's set or the two dummies of the element it is responsible for, and the preprocessing of those dummies fits into the epoch exactly. The other direction extracts: the preprocessing budget of an epoch admits at most 2(k−1)2(k-1) dummies, so a solution of the target size holds exactly one selection job and 2(k−1)2(k-1) dummies in every epoch, the element a machine is responsible for never decreases from one segment to the next, and with more than k(n−1)k(n-1) gaps between segments some gap sees no change at all — the kk elements of that segment hit every set.

    The numbers of the constructed shop are polynomial in nn, mm and kk, and hence in the length of the Hitting Set instance, so the hardness is strong: no algorithm polynomial in the magnitudes of the due dates can exist unless P=NP\mathrm{P} = \mathrm{NP}.

    Concept map
    12 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 construct_correct proven

    In the paper

    • page 8 of this submission's paper

    Lean source view on GitHub

    1import Lax496464.Construction
    2import Lax496464.NPHardness
    3
    4/-!
    5---
    6title: Theorem 1
    7type: theorem
    8---
    9Just-in-time scheduling in a two-stage flexible flow shop is strongly NP-hard, already
    10when every weight is one.
    11
    12The reduction is from Hitting Set. For 2≤k≤n2 \le k \le n, the shop built from a family
    13F1,…,FmF_1, \dots, F_m over {1,…,n}\{1, \dots, n\} admits R⋅m⋅(2k−1)R \cdot m \cdot (2k-1) just-in-time
    14jobs exactly when the family has a hitting set of size kk.
    15
    16One direction schedules: a hitting set assigns to each of its kk elements one machine,
    17which runs in every epoch either the selection job of the element that hits that epoch's
    18set or the two dummies of the element it is responsible for, and the preprocessing of
    19those dummies fits into the epoch exactly. The other direction extracts: the
    20preprocessing budget of an epoch admits at most 2(k−1)2(k-1) dummies, so a solution of the
    21target size holds exactly one selection job and 2(k−1)2(k-1) dummies in every epoch, the
    22element a machine is responsible for never decreases from one segment to the next, and
    23with more than k(n−1)k(n-1) gaps between segments some gap sees no change at all — the kk
    24elements of that segment hit every set.
    25
    26The numbers of the constructed shop are polynomial in nn, mm and kk, and hence in the
    27length of the Hitting Set instance, so the hardness is strong: no algorithm polynomial in
    28the magnitudes of the due dates can exist unless P=NP\mathrm{P} = \mathrm{NP}.
    29
    30# Formalization Notes
    31
    32Two statements, with different content and different costs.
    33
    34The first is the correctness of the construction, which is what the section proves, and
    35it is an equivalence between two combinatorial facts — no machine and no encoding occur
    36in it. It carries the hypothesis 2≤k≤n2 \le k \le n, which the problem reduced from
    37supplies, and without which the construction is false.
    38
    39The second is the hardness claim, which quantifies over every language in NP and composes
    40the construction with the NP-hardness of Hitting Set. It is stated against the classical
    41Turing-machine notion, since that is what a claim of NP-hardness means, and on the
    42unit-weight slice, because the construction lands there: the theorem is about
    43FF(1,m)∣∣∑jZjFF(1,m) \mid\mid \sum_j Z_j, the shop with no weights at all.
    44
    45What stands between the two is the ordinary work of a reduction: composing two
    46polynomial-time maps, and reading the composite's output size off the construction. The
    47hardness of Hitting Set itself is `HittingSetHardness`.
    48-/
    49
    50namespace Lax496464.Theorem1
    51
    52open Lax496464.FlowShop Lax496464.FlowShop.Instance
    53open Lax496464.HittingSet Lax496464.Construction Lax496464.NPHardness
    54
    55/-- **Theorem 1, the construction.** For `2 ≤ k ≤ n`, the constructed shop has a feasible
    56set of `R·m·(2k−1)` just-in-time jobs exactly when `P` has a hitting set of size `k`. -/
    57axiom construct_correct (P : HittingSet.Instance) (k : ℕ) (hk : 2 ≤ k) (hkn : k ≤ P.n) :
    58 Instance.HasHittingSet P k ↔ HasWeight (construct P k) (target P k)
    59
    60/-- **Theorem 1.** Just-in-time scheduling in a two-stage flexible flow shop is strongly
    61NP-hard, already on instances all of whose weights are one. -/
    62axiom stronglyNPHard_hasWeight :
    63 StronglyNPHardOn (fun I W => HasWeight I W) fun I => ∀ j : I.Job, I.w j = 1
    64
    65end Lax496464.Theorem1
    66
    Show ProofShow Proof
    Formalization Notes

    Two statements, with different content and different costs.

    The first is the correctness of the construction, which is what the section proves, and it is an equivalence between two combinatorial facts — no machine and no encoding occur in it. It carries the hypothesis 2≤k≤n2 \le k \le n, which the problem reduced from supplies, and without which the construction is false.

    The second is the hardness claim, which quantifies over every language in NP and composes the construction with the NP-hardness of Hitting Set. It is stated against the classical Turing-machine notion, since that is what a claim of NP-hardness means, and on the unit-weight slice, because the construction lands there: the theorem is about FF(1,m)∣∣∑jZjFF(1,m) \mid\mid \sum_j Z_j, the shop with no weights at all.

    What stands between the two is the ordinary work of a reduction: composing two polynomial-time maps, and reading the composite's output size off the construction. The hardness of Hitting Set itself is HittingSetHardnessHittingSetHardness.

    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…