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

Machine sets encoded by long processing times

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

    On unrelated machines every processing time is finite, and the problems on unrelated machines have no machine sets. A machine on which job jj may not run is instead encoded by a processing time too long for every schedule within the threshold. Four relations of the Scheduling Zoo rest on this encoding; each maps an instance with machine sets MjM_j and threshold DD to an instance on unrelated machines with the same jobs, machines and times pijp_{ij} for i∈Mji \in M_j, and a long time for i∉Mji \notin M_j.

    • P∣Mj∣Cmax⁡P \mid M_j \mid C_{\max} to R∣∣Cmax⁡R \mid\mid C_{\max} and Q∣Mj∣∑CjQ \mid M_j \mid \sum C_j to R∣∣∑CjR \mid\mid \sum C_j: the time D+1D + 1. A job on a machine outside its set completes after DD, so a schedule within the threshold uses only the machines of the sets, and it is a schedule of the instance with machine sets of the same cost. A job without a machine in its set makes both instances infeasible within the threshold.
    • P∣Mj∣∑wjCjP \mid M_j \mid \sum w_jC_j to R∣∣∑wjCjR \mid\mid \sum w_jC_j: the time D+1D + 1 again. A job of positive weight on a machine outside its set costs more than DD; a job of weight 00 costs nothing anywhere and is moved to the end of a machine of its set. An instance with a job whose set is empty is mapped to a threshold that no schedule meets.
    • P∣Mj∣∑wjZjP \mid M_j \mid \sum w_jZ_j to R∣∣∑wjZjR \mid\mid \sum w_jZ_j: the time dj+1d_j + 1, so a job outside its set is never just in time; such jobs are moved to the end of a machine of their set, which makes no just-in-time job late. An instance with a job whose set is empty is mapped to a threshold that no schedule meets.

    Theorem. The decision version of each of the four problems with machine sets reduces to that of the problem on unrelated machines, with the same numbers of jobs and machines.

    The reduction is computed on the standard words: a program reads the word of an instance with machine sets and its threshold and writes the word of the unrelated instance and its threshold, in polynomial time and with numbers at most one more than those it reads. So hardness goes up along the four relations.

    Theorem. Along each of the four relations, NP-hardness and strong NP-hardness on the standard reading go from the problem with machine sets to the problem on unrelated machines, and so does W[t]-hardness for the number of machines.

    Concept map
    61 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 jobsDeadlinesMachine sets encoded by long processingtimesForbidden 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 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 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 16 statements. Each proof establishes one of them relative to its assumptions.

    Lean source view on GitHub

    1import Lax434175.ZooParallel
    2import Lax434175.Parameters
    3import Lax434175.StandardReading
    4
    5/-!
    6---
    7title: Machine sets encoded by long processing times
    8type: theorem
    9---
    10On unrelated machines every processing time is finite, and the problems on
    11unrelated machines have no machine sets. A machine on which job jj may not run is instead encoded by a
    12processing time too long for every schedule within the threshold. Four
    13relations of the Scheduling Zoo rest on this encoding; each maps an instance
    14with machine sets MjM_j and threshold DD to an instance on unrelated machines
    15with the same jobs, machines and times pijp_{ij} for i∈Mji \in M_j, and a long
    16time for i∉Mji \notin M_j.
    17
    18- P∣Mj∣Cmax⁡P \mid M_j \mid C_{\max} to R∣∣Cmax⁡R \mid\mid C_{\max} and
    19 Q∣Mj∣∑CjQ \mid M_j \mid \sum C_j to R∣∣∑CjR \mid\mid \sum C_j: the time D+1D + 1. A job
    20 on a machine outside its set completes after DD, so a schedule within the
    21 threshold uses only the machines of the sets, and it is a schedule of the
    22 instance with machine sets of the same cost. A job without a machine in its
    23 set makes both instances infeasible within the threshold.
    24- P∣Mj∣∑wjCjP \mid M_j \mid \sum w_jC_j to R∣∣∑wjCjR \mid\mid \sum w_jC_j: the time
    25 D+1D + 1 again. A job of positive weight on a machine outside its set costs
    26 more than DD; a job of weight 00 costs nothing anywhere and is moved to
    27 the end of a machine of its set. An instance with a job whose set is empty
    28 is mapped to a threshold that no schedule meets.
    29- P∣Mj∣∑wjZjP \mid M_j \mid \sum w_jZ_j to R∣∣∑wjZjR \mid\mid \sum w_jZ_j: the time
    30 dj+1d_j + 1, so a job outside its set is never just in time; such jobs are
    31 moved to the end of a machine of their set, which makes no just-in-time job
    32 late. An instance with a job whose set is empty is mapped to a threshold
    33 that no schedule meets.
    34
    35**Theorem.** The decision version of each of the four problems with machine
    36sets reduces to that of the problem on unrelated machines, with the same
    37numbers of jobs and machines.
    38
    39The reduction is computed on the standard words: a program reads the word of an
    40instance with machine sets and its threshold and writes the word of the
    41unrelated instance and its threshold, in polynomial time and with numbers at
    42most one more than those it reads. So hardness goes up along the four
    43relations.
    44
    45**Theorem.** Along each of the four relations, NP-hardness and strong
    46NP-hardness on the standard reading go from the problem with machine sets to the
    47problem on unrelated machines, and so does W[t]-hardness for the number of
    48machines.
    49-/
    50
    51namespace Lax434175.EncodingsEligibility
    52open Lax434175 Lax434175.Problems Lax434175.Assembly Lax434175.Parameters
    53
    54/-- The numbers of jobs and machines of an instance. -/
    55def size {s : Spec OperationsFamily.family} (x : Inst OperationsFamily.family s) : ℕ × ℕ :=
    56 (x.base.jobs, x.base.machines)
    57
    58/-- `P|Mj|Cmax` reduces to `R||Cmax`. -/
    59axiom machineSets_makespan :
    60 ReducibleWith (A := problem _ ZooParallel.p107) (B := problem _ ZooParallel.p5) size size
    61 (fun a b => b = a)
    62
    63/-- `Q|Mj|ΣCj` reduces to `R||ΣCj`. -/
    64axiom machineSets_sumC :
    65 ReducibleWith (A := problem _ ZooParallel.p33) (B := problem _ ZooParallel.p31) size size
    66 (fun a b => b = a)
    67
    68/-- `P|Mj|ΣwjCj` reduces to `R||ΣwjCj`. -/
    69axiom machineSets_sumWC :
    70 ReducibleWith (A := problem _ ZooParallel.p130) (B := problem _ ZooParallel.p222) size size
    71 (fun a b => b = a)
    72
    73/-- `P|Mj|ΣwjZj` reduces to `R||ΣwjZj`. -/
    74axiom machineSets_sumWZ :
    75 ReducibleWith (A := problem _ ZooParallel.p200) (B := problem _ ZooParallel.p208) size size
    76 (fun a b => b = a)
    77
    78open Lax434175.Results Lax434175.ResultParameters
    79
    80/-- NP-hardness goes up along `P|Mj|Cmax → R||Cmax`. -/
    81axiom npHard_makespan :
    82 NPHard (StandardReading.ops.at ZooParallel.p107) → NPHard (StandardReading.ops.at ZooParallel.p5)
    83
    84/-- NP-hardness goes up along `Q|Mj|ΣCj → R||ΣCj`. -/
    85axiom npHard_sumC :
    86 NPHard (StandardReading.ops.at ZooParallel.p33) → NPHard (StandardReading.ops.at ZooParallel.p31)
    87
    88/-- NP-hardness goes up along `P|Mj|ΣwjCj → R||ΣwjCj`. -/
    89axiom npHard_sumWC :
    90 NPHard (StandardReading.ops.at ZooParallel.p130) → NPHard (StandardReading.ops.at ZooParallel.p222)
    91
    92/-- NP-hardness goes up along `P|Mj|ΣwjZj → R||ΣwjZj`. -/
    93axiom npHard_sumWZ :
    94 NPHard (StandardReading.ops.at ZooParallel.p200) → NPHard (StandardReading.ops.at ZooParallel.p208)
    95
    96/-- Strong NP-hardness goes up along `P|Mj|Cmax → R||Cmax`. -/
    97axiom stronglyNPHard_makespan :
    98 StronglyNPHard (StandardReading.ops.at ZooParallel.p107) →
    99 StronglyNPHard (StandardReading.ops.at ZooParallel.p5)
    100
    101/-- Strong NP-hardness goes up along `Q|Mj|ΣCj → R||ΣCj`. -/
    102axiom stronglyNPHard_sumC :
    103 StronglyNPHard (StandardReading.ops.at ZooParallel.p33) →
    104 StronglyNPHard (StandardReading.ops.at ZooParallel.p31)
    105
    106/-- Strong NP-hardness goes up along `P|Mj|ΣwjCj → R||ΣwjCj`. -/
    107axiom stronglyNPHard_sumWC :
    108 StronglyNPHard (StandardReading.ops.at ZooParallel.p130) →
    109 StronglyNPHard (StandardReading.ops.at ZooParallel.p222)
    110
    111/-- Strong NP-hardness goes up along `P|Mj|ΣwjZj → R||ΣwjZj`. -/
    112axiom stronglyNPHard_sumWZ :
    113 StronglyNPHard (StandardReading.ops.at ZooParallel.p200) →
    114 StronglyNPHard (StandardReading.ops.at ZooParallel.p208)
    115
    116/-- W[t]-hardness for the number of machines goes up along `P|Mj|Cmax → R||Cmax`. -/
    117axiom wHard_m_makespan (t : ℕ) :
    118 WHard (StandardReading.ops.at ZooParallel.p107) t (lift (Ops.m ZooParallel.p107)) →
    119 WHard (StandardReading.ops.at ZooParallel.p5) t (lift (Ops.m ZooParallel.p5))
    120
    121/-- W[t]-hardness for the number of machines goes up along `Q|Mj|ΣCj → R||ΣCj`. -/
    122axiom wHard_m_sumC (t : ℕ) :
    123 WHard (StandardReading.ops.at ZooParallel.p33) t (lift (Ops.m ZooParallel.p33)) →
    124 WHard (StandardReading.ops.at ZooParallel.p31) t (lift (Ops.m ZooParallel.p31))
    125
    126/-- W[t]-hardness for the number of machines goes up along `P|Mj|ΣwjCj → R||ΣwjCj`. -/
    127axiom wHard_m_sumWC (t : ℕ) :
    128 WHard (StandardReading.ops.at ZooParallel.p130) t (lift (Ops.m ZooParallel.p130)) →
    129 WHard (StandardReading.ops.at ZooParallel.p222) t (lift (Ops.m ZooParallel.p222))
    130
    131/-- W[t]-hardness for the number of machines goes up along `P|Mj|ΣwjZj → R||ΣwjZj`. -/
    132axiom wHard_m_sumWZ (t : ℕ) :
    133 WHard (StandardReading.ops.at ZooParallel.p200) t (lift (Ops.m ZooParallel.p200)) →
    134 WHard (StandardReading.ops.at ZooParallel.p208) t (lift (Ops.m ZooParallel.p208))
    135
    136end Lax434175.EncodingsEligibility
    137
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof

    Discussion

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

    Loading discussion…