Lax Lean Archive

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

Scheduling every job is hard for constant processing times and unit weights

Lax470956.Theorem2 · concepts/Lax470956/Theorem2.lean · lax-470956

open

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

    Deciding whether every job of an interval scheduling instance can be scheduled is NP-hard, and remains so on instances in which every processing time is at most 2525 and every weight is 11.

    The bound on the processing times is absolute: it does not grow with the instance. So the problem is para-NP-hard for the parameter pmax⁡p_{\max}, and no algorithm running in f(pmax⁡)⋅poly(n)f(p_{\max}) \cdot \mathrm{poly}(n) time can exist for any function ff unless P=NP\mathrm{P} = \mathrm{NP}. Together with the third theorem, which is fixed-parameter tractable for m+pmax⁡m + p_{\max}, this shows that neither half of that combined parameter can be dropped.

    The reduction is from (3,4)(3,4)-satisfiability. It gives each variable two machines, one for each truth value, and each clause three; each occurrence of a variable in a clause becomes a unit job flanked by two jobs filling the rest of a fixed window of length 2525, and each variable becomes one job spanning that whole window. The bounded number of occurrences of a variable is what keeps the window, and with it every processing time, bounded by a constant.

    Concept map
    21 concepts
    100%
    Proven claimOpen 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 npHard_allSchedulable open

    2 npHardOn_allSchedulable_pmax_le open

    3 sat34_polyReducesOn_allSchedulable proven

    Lean source view on GitHub

    1import Lax470956.Exact34Encoding
    2import Lax470956.PolynomialReduction
    3import Lax470956.SatVariant
    4import Lax470956.SchedulingProblems
    5
    6/-!
    7---
    8title: Scheduling every job is hard for constant processing times and unit weights
    9type: theorem
    10---
    11Deciding whether every job of an interval scheduling instance can be scheduled is
    12NP-hard, and remains so on instances in which every processing time is at most 2525 and
    13every weight is 11.
    14
    15The bound on the processing times is absolute: it does not grow with the instance. So the
    16problem is para-NP-hard for the parameter pmax⁡p_{\max}, and no algorithm running in
    17f(pmax⁡)⋅poly(n)f(p_{\max}) \cdot \mathrm{poly}(n) time can exist for any function ff unless
    18P=NP\mathrm{P} = \mathrm{NP}. Together with the third theorem, which is fixed-parameter
    19tractable for m+pmax⁡m + p_{\max}, this shows that neither half of that combined parameter can
    20be dropped.
    21
    22The reduction is from (3,4)(3,4)-satisfiability. It gives each variable two machines,
    23one for each truth value, and each clause three; each occurrence of a variable in a
    24clause becomes a unit job flanked by two jobs filling the rest of a fixed window of
    25length 2525, and each variable becomes one job spanning that whole window. The bounded
    26number of occurrences of a variable is what keeps the window, and with it every
    27processing time, bounded by a constant.
    28
    29# Formalization notes
    30
    31Three separate statements, because they are three assertions with different content and
    32different costs to establish.
    33
    34The first is the reduction itself, the paper's result: a polynomial-time
    35map on words sending satisfiable formulas exactly to schedulable instances, all of them
    36in the bounded slice. It is stated on the word RAM, where a program can be written and
    37its running time counted.
    38
    39The other two are the hardness conclusions. Each follows from the reduction together
    40with the NP-hardness of (3,4)(3,4)-satisfiability, and each is stated against the
    41classical Turing-machine notion of NP, since that is what a claim of NP-hardness means.
    42They are separate because they are reached differently: the reduction is a statement
    43about one map, while a hardness claim quantifies over every language in NP and composes
    44the reduction with the hardness of the problem it starts from.
    45
    46Nothing beyond ordinary work stands between the three. Polynomial-time computability on
    47the two machine models is interchangeable, and polynomial-time maps compose, so a
    48reduction certified on either model transports to the other and can be chained with a
    49cited hardness result. The only input this submission does not supply is that hardness
    50result itself.
    51-/
    52
    53namespace Lax470956.Theorem2
    54
    55open Lax470956.Scheduling Lax470956.NPHardness Lax470956.PolynomialReduction
    56
    57/-- The words encoding an instance in which every processing time is at most `25` and
    58every weight is `1`. -/
    59def BoundedSlice (y : List ℕ) : Prop :=
    60 ∃ I : Instance, InstanceEncoding.EncodesInstance y I ∧
    61 I.pmax ≤ 25 ∧ ∀ j, I.w j = 1
    62
    63/-- **Construction 2.** `(3,4)`-satisfiability reduces in polynomial time to
    64scheduling every job, by a reduction whose every output has processing times at most
    65`25` and unit weights. -/
    66axiom sat34_polyReducesOn_allSchedulable :
    67 PolyReducesOn Exact34Encoding.Satisfiable
    68 {y | ∃ I, InstanceEncoding.EncodesInstance y I ∧ I.AllSchedulable}
    69 BoundedSlice
    70
    71/-- **Theorem 2.** Deciding whether every job can be scheduled is NP-hard. -/
    72axiom npHard_allSchedulable : NPHard Instance.AllSchedulable
    73
    74/-- **Theorem 2, on the bounded slice.** Deciding whether every job can be scheduled is
    75NP-hard already on instances whose processing times are at most `25` and whose weights
    76are all `1` — so the problem is para-NP-hard for the parameter `p_max`. -/
    77axiom npHardOn_allSchedulable_pmax_le :
    78 NPHardOn Instance.AllSchedulable
    79 fun I => I.pmax ≤ 25 ∧ ∀ j, I.w j = 1
    80
    81end Lax470956.Theorem2
    82
    Show ProofShow ProofShow Proof
    Formalization notes

    Three separate statements, because they are three assertions with different content and different costs to establish.

    The first is the reduction itself, the paper's result: a polynomial-time map on words sending satisfiable formulas exactly to schedulable instances, all of them in the bounded slice. It is stated on the word RAM, where a program can be written and its running time counted.

    The other two are the hardness conclusions. Each follows from the reduction together with the NP-hardness of (3,4)(3,4)-satisfiability, and each is stated against the classical Turing-machine notion of NP, since that is what a claim of NP-hardness means. They are separate because they are reached differently: the reduction is a statement about one map, while a hardness claim quantifies over every language in NP and composes the reduction with the hardness of the problem it starts from.

    Nothing beyond ordinary work stands between the three. Polynomial-time computability on the two machine models is interchangeable, and polynomial-time maps compose, so a reduction certified on either model transports to the other and can be chained with a cited hardness result. The only input this submission does not supply is that hardness result itself.

    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…