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

Two tests from the words up: NP-hardness of 1|r_j|L_max and Smith's rule

Lax434175.Sanity · concepts/Lax434175/Sanity.lean · lax-434175

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

    A test of the hardness statements end to end, on a registered result. Elffers and de Weerdt prove single-machine scheduling with release times and deadlines NP-complete when the job lengths lie in {p,q}\{p, q\} for fixed p>q>1p > q > 1 (formalized in lax-391470, on binary words). An instance with integer release times rjr_j and deadlines djd_j, all shifted up by the largest absolute value among them, is an instance of 1∣rj∣Lmax⁡1 \mid r_j \mid L_{\max} with due dates the shifted deadlines, and it is feasible exactly when the maximum lateness can be made at most 00; its standard word with threshold 00 is computed from the binary word in polynomial time.

    Theorem. 1∣rj∣Lmax⁡1 \mid r_j \mid L_{\max} is NP-hard on the standard reading.

    A test of the algorithmic side end to end: Smith's rule. On one machine, the total weighted completion time is smallest when the jobs run without idle time in the order of pj/wjp_j / w_j (jobs of weight 00 last). A program reads the standard word of an instance of 1∣∣∑wjCj1 \mid\mid \sum w_jC_j (not a problem of the zoo's data, which leaves out problems this easy) and its threshold, sorts the jobs by comparing piwjp_iw_j with pjwip_jw_i, adds up the weighted completion times and compares with the threshold.

    Theorem. 1∣∣∑wjCj1 \mid\mid \sum w_jC_j is decided within O(nlog⁡n)O(n \log n) instructions, plus the length of the word, on short words.

    Concept map
    61 concepts; 1 descendant hidden
    100%
    Conjunctive normal formAssembling problems from fieldsOne family for serial and parallel batchingBatching problems in three-field notationBatch scheduling on a single machineCommunication delaysBounds on the number of machines and jobsDeadlinesForbidden times and input encodingsInterruption as a field of parallel-machineschedulingScheduling kernelsMaximizing the minimum machine loadMachine sets and multiprocessor tasksConstraint modules and objectivesNon-preemptive scheduling on parallelmachinesCompletion-time objectivesOnline scheduling as a gameScheduling with operationsOne family for parallel machines and shopsOne family for parallel machines with andwithout preemptionParallel machinesProblems on parallel machines in three-fieldnotationParameters along embeddingsPrecedence constraints and time lagsPreemptive scheduling on parallel machinesPreemptive shop problems in three-fieldnotationPreemptive shop schedulingOptimization problems and embeddingsSingle-machine scheduling with rejectionRelease datesPreemption with restarts on parallelmachinesParameters of the zoo's resultsThe kinds of results on scheduling problemsTwo tests from the words up: NP-hardness of1|r_j|L_max and Smith's ruleA single server with setup timesNo-idle shops and batch setup timesOne family for shops with and withoutpreemptionShop problems in three-field notationShop schedulingThe standard reading of scheduling instancesand schedulesThreshold reductions between objectivesTransportation delays and a transport robotScheduling problems as parameterizedproblems on wordsThe Scheduling Zoo, non-preemptiveproblems on parallel machinesParameters of scheduling problemsBinary encoding of an input and a certificateThe complexity class NPThe complexity class PFixed-Parameter Time on the Word RAMFPT-Reductions, FPT, Hardness andCompletenessFinite Relational StructuresFirst-Order Formulas and the Classes Σ_tand Π_tModel Checking and Weighted FaginDefinabilityThe W-Hierarchy and the A-HierarchyNP-Hardness of a Problem on Words ofNumbersBinary encoding of finite wordsPolynomial-time computation by a wordRAMPolynomial-time computation by a TuringmachineThe word RAMComputing a function within a time boundParameterized Problems andFPT-Reductions on a Word RAM
    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.

    2 smith proven

    Lean source view on GitHub

    1import Lax434175.ZooParallel
    2import Lax434175.StandardReading
    3
    4/-!
    5---
    6title: Two tests from the words up: NP-hardness of 1|r_j|L_max and Smith's rule
    7type: theorem
    8---
    9A test of the hardness statements end to end, on a registered result. Elffers
    10and de Weerdt prove single-machine scheduling with release times and deadlines
    11NP-complete when the job lengths lie in {p,q}\{p, q\} for fixed p>q>1p > q > 1
    12(formalized in lax-391470, on binary words). An instance with integer release
    13times rjr_j and deadlines djd_j, all shifted up by the largest absolute value
    14among them, is an instance of 1∣rj∣Lmax⁡1 \mid r_j \mid L_{\max} with due dates the shifted
    15deadlines, and it is feasible exactly when the maximum lateness can be made at
    16most 00; its standard word with threshold 00 is computed from the binary word
    17in polynomial time.
    18
    19**Theorem.** 1∣rj∣Lmax⁡1 \mid r_j \mid L_{\max} is NP-hard on the standard reading.
    20
    21A test of the algorithmic side end to end: Smith's rule. On one machine, the
    22total weighted completion time is smallest when the jobs run without idle time
    23in the order of pj/wjp_j / w_j (jobs of weight 00 last). A program reads the
    24standard word of an instance of 1∣∣∑wjCj1 \mid\mid \sum w_jC_j (not a problem of the
    25zoo's data, which leaves out problems this easy) and its threshold, sorts the
    26jobs by comparing piwjp_iw_j with pjwip_jw_i, adds up the weighted completion times
    27and compares with the threshold.
    28
    29**Theorem.** 1∣∣∑wjCj1 \mid\mid \sum w_jC_j is decided within O(nlog⁡n)O(n \log n) instructions,
    30plus the length of the word, on short words.
    31-/
    32
    33namespace Lax434175.Sanity
    34open Lax434175 Lax434175.Results Lax434175.Assembly
    35
    36/-- `1|rj|Lmax` is NP-hard on the standard reading. -/
    37-- zoo-result: {"problem": "1|r_j|L_{\\max}", "param": "", "claim": "is NP-hard", "note": "through lax-391470 (two job lengths), a test of the hardness statements end to end"}
    38axiom npHard_rjLmax : NPHard (StandardReading.ops.at ZooParallel.p158)
    39
    40/-- `1||ΣwjCj`, a single machine and the total weighted completion time. -/
    41def singleWC : Spec OperationsFamily.family :=
    42 OperationsFamily.spec (machineCount := .atMost 1) (objective := .sumWC)
    43
    44/-- **Smith's rule**, end to end: `1||ΣwjCj` is decided within `O(n log n)`
    45instructions plus the length of the word. -/
    46axiom smith :
    47 DecidesWithin (StandardReading.ops.at singleWC) fun x =>
    48 (ResultParameters.Ops.n singleWC x + 1) * (Nat.log 2 (ResultParameters.Ops.n singleWC x) + 1) +
    49 inputSize (StandardReading.ops.at singleWC) x
    50
    51end Lax434175.Sanity
    52
    Show ProofShow Proof

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…