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

Scheduling with two non-unit job lengths is NP-complete

Lax391470.Theorem1 · concepts/Lax391470/Theorem1.lean · lax-391470

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

    Let p>q>1p > q > 1 be two integer job lengths. Single machine scheduling with release times and deadlines, restricted to instances whose processing times all lie in {p,q}\{p, q\}, is NP-complete.

    Hardness is obtained by composing the reduction from satisfiability to the auxiliary problem AUX(p,q)\mathrm{AUX}(p, q) with the reduction from the auxiliary problem to scheduling on the lengths {p,q}\{p, q\}. Since pp and qq are constants, every number of the constructed instance is bounded by a polynomial in the size of the formula, so the source concludes that the problem is even strongly NP-complete. The two bounds are stated as SatConstruction.timesleSatConstruction.times_le and StackedConstruction.timesleStackedConstruction.times_le; strong NP-completeness itself, which would need a unary encoding of the instance, is not stated here.

    The cases left out are polynomial-time solvable: a single job length, and two job lengths of which the shorter is 11.

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

    Lean source view on GitHub

    1import Lax391470.Lemma1
    2import Lax391470.Lemma2
    3
    4/-!
    5---
    6title: Scheduling with two non-unit job lengths is NP-complete
    7type: theorem
    8---
    9Let p>q>1p > q > 1 be two integer job lengths. Single machine scheduling with release times
    10and deadlines, restricted to instances whose processing times all lie in {p,q}\{p, q\}, is
    11NP-complete.
    12
    13Hardness is obtained by composing the reduction from satisfiability to the auxiliary
    14problem AUX(p,q)\mathrm{AUX}(p, q) with the reduction from the auxiliary problem to scheduling
    15on the lengths {p,q}\{p, q\}. Since pp and qq are constants, every number of the
    16constructed instance is bounded by a polynomial in the size of the formula, so the source
    17concludes that the problem is even strongly NP-complete. The two bounds are stated as
    18`SatConstruction.times_le` and `StackedConstruction.times_le`; strong NP-completeness
    19itself, which would need a unary encoding of the instance, is not stated here.
    20
    21The cases left out are polynomial-time solvable: a single job length, and two job
    22lengths of which the shorter is 11.
    23
    24# Formalization notes
    25
    26Membership in NP holds for every pair of lengths and is stated without hypotheses. A
    27certificate is a schedule with integer start times; feasibility confines every start
    28time between a release time and a deadline of the instance, so its encoding is no longer
    29than that of the instance.
    30-/
    31
    32namespace Lax391470.Theorem1
    33
    34open Lax391470.BinaryEncoding Lax434930.PolynomialTime
    35open Lax434930.NondeterministicPolynomialTime Lax429075.Reductions
    36
    37/-- Scheduling on the lengths `{p, q}` belongs to NP. -/
    38axiom twoLengths_mem_NP (p q : ℕ) : TwoLengths p q ∈ NP
    39
    40/-- For job lengths `p > q > 1`, scheduling on the lengths `{p, q}` is NP-hard. -/
    41axiom twoLengths_npHard (p q : ℕ) (hq : 1 < q) (hqp : q < p) :
    42 ∀ A : Language, A ∈ NPManyOne A (TwoLengths p q)
    43
    44/-- **Theorem 1.** For job lengths `p > q > 1`, scheduling on the lengths `{p, q}` is
    45NP-complete. -/
    46axiom twoLengths_npComplete (p q : ℕ) (hq : 1 < q) (hqp : q < p) :
    47 NPComplete (TwoLengths p q)
    48
    49end Lax391470.Theorem1
    50
    Show ProofShow ProofShow Proof
    Formalization notes

    Membership in NP holds for every pair of lengths and is stated without hypotheses. A certificate is a schedule with integer start times; feasibility confines every start time between a release time and a deadline of the instance, so its encoding is no longer than that of the instance.

    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…