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

1|r_j|L_max is para-NP-hard for the largest and the number of processing times

Lax434175.SanityParams · concepts/Lax434175/SanityParams.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

    The reduction that makes 1∣rj∣Lmax⁡1 \mid r_j \mid L_{\max} NP-hard (concept SanitySanity, from lax-391470 with the job lengths {3,2}\{3, 2\}) produces only instances whose processing times are 22 or 33; on a word that is not such an instance it produces the instance without jobs. So the problem is NP-hard already on the instances with pmax⁡≤3p_{\max} \le 3, and on those with at most two distinct processing times.

    Theorem. 1∣rj∣Lmax⁡1 \mid r_j \mid L_{\max} is para-NP-hard parameterized by pmax⁡p_{\max}, and parameterized by the number #p\#p of distinct processing times, on the standard reading.

    The explicit reductions of lax-391470 (Cook–Levin to satisfiability, then the formula instance, then the stacked instance) produce release times and deadlines at most a constant times the number of jobs: the time line of the formula instance has length 2nS2nS with SS linear in the number mm of clauses, the stacked instance has n+(2n−1)m≥n(m+1)n + (2n-1)m \ge n(m+1) connected pairs, five jobs each, and stacking adds at most (p+2q)(p + 2q) per pair. So every number of the emitted word is linear in its length.

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

    Concept map
    63 concepts
    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 rule1|r_j|L_max is para-NP-hard for the largestand the number of processing timesA 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 machinesResults of The Scheduling Zoo,non-preemptive problems on parallelmachinesParameters 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 6 statements. Each proof establishes one of them relative to its assumptions.

    Lean source view on GitHub

    1import Lax434175.Sanity
    2import Lax434175.ZooParallelResults
    3
    4/-!
    5---
    6title: 1|r_j|L_max is para-NP-hard for the largest and the number of processing times
    7type: theorem
    8---
    9The reduction that makes 1∣rj∣Lmax⁡1 \mid r_j \mid L_{\max} NP-hard (concept `Sanity`, from
    10lax-391470 with the job lengths {3,2}\{3, 2\}) produces only instances whose
    11processing times are 22 or 33; on a word that is not such an instance it produces
    12the instance without jobs. So the problem is NP-hard already on the instances with
    13pmax⁡≤3p_{\max} \le 3, and on those with at most two distinct processing times.
    14
    15**Theorem.** 1∣rj∣Lmax⁡1 \mid r_j \mid L_{\max} is para-NP-hard parameterized by pmax⁡p_{\max},
    16and parameterized by the number #p\#p of distinct processing times, on the
    17standard reading.
    18
    19The explicit reductions of lax-391470 (Cook–Levin to satisfiability, then the formula
    20instance, then the stacked instance) produce release times and deadlines at most a
    21constant times the number of jobs: the time line of the formula instance has length
    222nS2nS with SS linear in the number mm of clauses, the stacked instance has
    23n+(2n−1)m≥n(m+1)n + (2n-1)m \ge n(m+1) connected pairs, five jobs each, and stacking adds at most
    24(p+2q)(p + 2q) per pair. So every number of the emitted word is linear in its length.
    25
    26**Theorem.** 1∣rj∣Lmax⁡1 \mid r_j \mid L_{\max} is strongly NP-hard on the standard reading.
    27-/
    28
    29namespace Lax434175.SanityParams
    30open Lax434175 Lax434175.Results Lax434175.ResultParameters
    31
    32/-- `1|rj|Lmax`, parameter pmax: para-NP-hard on the standard reading. -/
    33-- zoo-result: {"problem": "1|r_j|L_{\\max}", "param": "pmax", "claim": "is para-NP-hard", "note": "through lax-391470 (job lengths 2 and 3): NP-hard already with pmax ≤ 3"}
    34axiom paraNPHard_pmax :
    35 ParaNPHard (StandardReading.ops.at ZooParallel.p158) (lift (Ops.pmax ZooParallel.p158))
    36
    37/-- `1|rj|Lmax`, parameter #p: para-NP-hard on the standard reading. -/
    38-- zoo-result: {"problem": "1|r_j|L_{\\max}", "param": "#p", "claim": "is para-NP-hard", "note": "through lax-391470 (job lengths 2 and 3), and #p ≤ pmax + 1"}
    39axiom paraNPHard_numP :
    40 ParaNPHard (StandardReading.ops.at ZooParallel.p158) (lift (Ops.numP ZooParallel.p158))
    41
    42/-- `1|rj|Lmax` is strongly NP-hard on the standard reading: with the explicit reductions
    43of lax-391470, every release time and deadline is at most a constant times the number of
    44jobs, so the emitted words have numbers linear in their length. -/
    45axiom p158_r0_holds : ZooParallelResults.p158_r0 StandardReading.ops
    46
    47/-- `1|rj|Lmax` is strongly NP-hard, the result as cited from Elffers and de Weerdt. -/
    48axiom p158_r1_holds : ZooParallelResults.p158_r1 StandardReading.ops
    49
    50/-- `1|rj|Lmax` is NP-hard for a fixed largest processing time. -/
    51axiom p158_r2_holds : ZooParallelResults.p158_r2 StandardReading.ops
    52
    53/-- `1|rj|Lmax` is NP-hard for a fixed number of distinct processing times. -/
    54axiom p158_r3_holds : ZooParallelResults.p158_r3 StandardReading.ops
    55
    56end Lax434175.SanityParams
    57
    Show ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    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…