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

P | M_j | Σ w_j Z_j is strongly W[1]-hard for the number of machines

Lax434175.IsemStrong · concepts/Lax434175/IsemStrong.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 behind IsemStandardIsemStandard starts from a Multicoloured Clique instance with nn vertices and kk colours, writes the interval scheduling instance of Construction 1 of lax-888481 with its threshold, pads it (IsemLinkIsemLink), and writes the standard word of the zoo instance. The numbers Construction 1 writes are at most (n+k+2)15(n + k + 2)^{15}, and it has nk+k2nnk + k^2 n jobs and one more per edge.

    Before the standard word is written, the threshold WW is lowered to min⁡(W,∑jwj+1)\min(W, \sum_j w_j + 1). No schedule has weight above ∑jwj\sum_j w_j, so the answer is kept; the map is computed in polynomial time on the word RAM, and it keeps the number of machines.

    If n≥1n \ge 1, then k≥1k \ge 1, the instance has at least n+kn + k jobs, and the standard word has a record for each, so its length ℓ\ell is at least n+kn + k. Padding, dropping the unused machines and writing the standard word raise the numbers and the length only polynomially, so every number of the standard word is at most (n+k+2)31≤231(ℓ+1)31(n + k + 2)^{31} \le 2^{31} (\ell + 1)^{31}. If n=0n = 0, the instance has no job, the lowered threshold is at most 11, and every number of the standard word is at most 4040.

    Theorem. Multicoloured Clique fpt-reduces to P∣Mj∣∑wjZjP \mid M_j \mid \sum w_j Z_j under the standard reading, parameterized by the number of machines, restricted to the words whose numbers are at most 231(ℓ+1)312^{31} (\ell + 1)^{31}. Since Multicoloured Clique is W[1]-complete (lax-496464), the problem is strongly W[1]-hard for the number of machines.

    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-machineschedulingHardness of P | M_j | Σ w_j Z_j under thestandard readingP | M_j | Σ w_j Z_j is strongly W[1]-hardfor the number of machinesScheduling 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 problemsA 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

    Lean source view on GitHub

    1import Lax434175.IsemStandard
    2
    3/-!
    4---
    5title: P | M_j | Σ w_j Z_j is strongly W[1]-hard for the number of machines
    6type: theorem
    7---
    8The reduction behind `IsemStandard` starts from a Multicoloured Clique instance with nn
    9vertices and kk colours, writes the interval scheduling instance of Construction 1 of
    10lax-888481 with its threshold, pads it (`IsemLink`), and writes the standard word of the zoo
    11instance. The numbers Construction 1 writes are at most (n+k+2)15(n + k + 2)^{15}, and it has
    12nk+k2nnk + k^2 n jobs and one more per edge.
    13
    14Before the standard word is written, the threshold WW is lowered to
    15min⁡(W,∑jwj+1)\min(W, \sum_j w_j + 1). No schedule has weight above ∑jwj\sum_j w_j, so the answer is kept;
    16the map is computed in polynomial time on the word RAM, and it keeps the number of machines.
    17
    18If n≥1n \ge 1, then k≥1k \ge 1, the instance has at least n+kn + k jobs, and the standard word
    19has a record for each, so its length ℓ\ell is at least n+kn + k. Padding, dropping the unused
    20machines and writing the standard word raise the numbers and the length only polynomially, so
    21every number of the standard word is at most (n+k+2)31≤231(ℓ+1)31(n + k + 2)^{31} \le 2^{31} (\ell + 1)^{31}. If
    22n=0n = 0, the instance has no job, the lowered threshold is at most 11, and every number of the
    23standard word is at most 4040.
    24
    25**Theorem.** Multicoloured Clique fpt-reduces to P∣Mj∣∑wjZjP \mid M_j \mid \sum w_j Z_j under the
    26standard reading, parameterized by the number of machines, restricted to the words whose
    27numbers are at most 231(ℓ+1)312^{31} (\ell + 1)^{31}. Since Multicoloured Clique is W[1]-complete
    28(lax-496464), the problem is strongly W[1]-hard for the number of machines.
    29-/
    30
    31namespace Lax434175.IsemStrong
    32open Lax434175 Lax434175.Results Lax434175.ResultParameters
    33
    34/-- `P|M_j|Σ w_j Z_j` is strongly W[1]-hard in the number of machines under the standard
    35reading. -/
    36axiom p200_r0_holds : ZooParallelResults.p200_r0 StandardReading.ops
    37
    38end Lax434175.IsemStrong
    39
    Show 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…