Lax Lean Archive

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

Results of The Scheduling Zoo, parallel batching problems

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

definition

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

    Definition

    The 35 results of The Scheduling Zoo on its parallel batching problems that are stated here, each as a proposition about a reading of the problem (Results.PReadingResults.PReading; for a family, Results.ReadingResults.Reading at the problem's specification): its words of instances and schedules and what an online scheduler sees. Each names its source; where the proposition is weaker than the wording, a note says what is left out.

    Concept map
    60 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 problemsA single server with setup timesNo-idle shops and batch setup timesOne family for shops with and withoutpreemptionShop problems in three-field notationShop schedulingThreshold reductions between objectivesTransportation delays and a transport robotScheduling problems as parameterizedproblems on wordsThe Scheduling Zoo, parallel batchingproblemsResults of The Scheduling Zoo, parallelbatching problemsParameters 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

    Lean source view on GitHub

    1import Lax434175.ZooParallelBatching
    2import Lax434175.Results
    3import Lax434175.ResultParameters
    4
    5/-!
    6---
    7title: Results of The Scheduling Zoo, parallel batching problems
    8type: definition
    9---
    10The 35 results of The Scheduling Zoo on its parallel batching problems that are
    11stated here, each as a proposition about a reading of the problem
    12(`Results.PReading`; for a family, `Results.Reading` at the problem's
    13specification): its words of instances and schedules and what an online
    14scheduler sees. Each names its source; where the proposition is weaker than
    15the wording, a note says what is left out.
    16-/
    17
    18namespace Lax434175.ZooParallelBatchingResults
    19open Lax434175 Lax434175.Problems Lax434175.Results Lax434175.ResultParameters Lax434175.ZooParallelBatching
    20
    21/-- `1|pj=p;p-batch;rj|ΣwjCj`: is in P.
    22
    23Baptiste, P. (2000). Batching identical jobs. https://doi.org/10.1007/s001860000088
    24-/
    25def p0_r0 (R : Reading F) : Prop :=
    26 InP (R.at p0)
    27
    28/-- `1|pj=p;p-batch;rj|ΣwjUj`: is in P.
    29
    30Baptiste, P. (2000). Batching identical jobs. https://doi.org/10.1007/s001860000088
    31-/
    32def p1_r0 (R : Reading F) : Prop :=
    33 InP (R.at p1)
    34
    35/-- `1|pj=p;p-batch;rj|ΣTj`: is in P.
    36
    37Baptiste, P. (2000). Batching identical jobs. https://doi.org/10.1007/s001860000088
    38-/
    39def p2_r0 (R : Reading F) : Prop :=
    40 InP (R.at p2)
    41
    42/-- `1|pj=p;p-batch(∞);rj|ΣwjTj`: is in P.
    43
    44Baptiste, P. and Brucker, P. and Knust, S. and Timkovsky, V. (2004). Ten notes on equal-execution-time scheduling. None
    45-/
    46def p3_r0 (R : Reading F) : Prop :=
    47 InP (R.at p3)
    48
    49/-- `1|p-batch(∞);rj|ΣwjTj`: is in Ppseudo.
    50
    51Baptiste, P. and Brucker, P. and Knust, S. and Timkovsky, V. (2004). Ten notes on equal-execution-time scheduling. None
    52-/
    53def p4_r0 (R : Reading F) : Prop :=
    54 PseudoPoly (R.at p4)
    55
    56/-- `1|p-batch(∞);rj|ΣwjUj`: is in Ppseudo.
    57
    58Baptiste, P. and Brucker, P. and Knust, S. and Timkovsky, V. (2004). Ten notes on equal-execution-time scheduling. None
    59-/
    60def p5_r0 (R : Reading F) : Prop :=
    61 PseudoPoly (R.at p5)
    62
    63/-- `1|p-batch|Cmax`: is in P.
    64
    65Brucker, P. and Gladky, A. and Hoogeveen, H. and Kovalyov, M.Y. and Potts, C.N. and Tautenhahn, T. and van de Velde, S.L. (1998). Scheduling a batching machine. https://doi.org/10.1002/(sici)1099-1425(199806)1:1<31::aid-jos4>3.0.co;2-r
    66-/
    67def p6_r0 (R : Reading F) : Prop :=
    68 InP (R.at p6)
    69
    70/-- `1|p-batch(∞)|ΣwjCj`: is in P.
    71
    72Brucker, P. and Gladky, A. and Hoogeveen, H. and Kovalyov, M.Y. and Potts, C.N. and Tautenhahn, T. and van de Velde, S.L. (1998). Scheduling a batching machine. https://doi.org/10.1002/(sici)1099-1425(199806)1:1<31::aid-jos4>3.0.co;2-r
    73-/
    74def p7_r0 (R : Reading F) : Prop :=
    75 InP (R.at p7)
    76
    77/-- `1|p-batch(∞)|ΣUj`: is in P.
    78
    79Brucker, P. and Gladky, A. and Hoogeveen, H. and Kovalyov, M.Y. and Potts, C.N. and Tautenhahn, T. and van de Velde, S.L. (1998). Scheduling a batching machine. https://doi.org/10.1002/(sici)1099-1425(199806)1:1<31::aid-jos4>3.0.co;2-r
    80-/
    81def p8_r0 (R : Reading F) : Prop :=
    82 InP (R.at p8)
    83
    84/-- `1|p-batch(∞)|ΣwjUj`: is in Ppseudo.
    85
    86Brucker, P. and Gladky, A. and Hoogeveen, H. and Kovalyov, M.Y. and Potts, C.N. and Tautenhahn, T. and van de Velde, S.L. (1998). Scheduling a batching machine. https://doi.org/10.1002/(sici)1099-1425(199806)1:1<31::aid-jos4>3.0.co;2-r
    87-/
    88def p9_r0 (R : Reading F) : Prop :=
    89 PseudoPoly (R.at p9)
    90
    91/-- `1|p-batch(∞)|ΣwjUj`: is NP-hard.
    92
    93Brucker, P. and Gladky, A. and Hoogeveen, H. and Kovalyov, M.Y. and Potts, C.N. and Tautenhahn, T. and van de Velde, S.L. (1998). Scheduling a batching machine. https://doi.org/10.1002/(sici)1099-1425(199806)1:1<31::aid-jos4>3.0.co;2-r
    94-/
    95def p9_r1 (R : Reading F) : Prop :=
    96 NPHard (R.at p9)
    97
    98/-- `1|p-batch(∞)|ΣwjTj`: is in Ppseudo.
    99
    100Brucker, P. and Gladky, A. and Hoogeveen, H. and Kovalyov, M.Y. and Potts, C.N. and Tautenhahn, T. and van de Velde, S.L. (1998). Scheduling a batching machine. https://doi.org/10.1002/(sici)1099-1425(199806)1:1<31::aid-jos4>3.0.co;2-r
    101-/
    102def p10_r0 (R : Reading F) : Prop :=
    103 PseudoPoly (R.at p10)
    104
    105/-- `1|p-batch(∞)|ΣwjTj`: is NP-hard.
    106
    107Brucker, P. and Gladky, A. and Hoogeveen, H. and Kovalyov, M.Y. and Potts, C.N. and Tautenhahn, T. and van de Velde, S.L. (1998). Scheduling a batching machine. https://doi.org/10.1002/(sici)1099-1425(199806)1:1<31::aid-jos4>3.0.co;2-r
    108-/
    109def p10_r1 (R : Reading F) : Prop :=
    110 NPHard (R.at p10)
    111
    112/-- `1|p-batch;rj|Cmax`: is strongly NP-hard.
    113
    114Brucker, P. and Gladky, A. and Hoogeveen, H. and Kovalyov, M.Y. and Potts, C.N. and Tautenhahn, T. and van de Velde, S.L. (1998). Scheduling a batching machine. https://doi.org/10.1002/(sici)1099-1425(199806)1:1<31::aid-jos4>3.0.co;2-r
    115-/
    116def p11_r0 (R : Reading F) : Prop :=
    117 StronglyNPHard (R.at p11)
    118
    119/-- `1|p-batch|Lmax`: is strongly NP-hard.
    120
    121Brucker, P. and Gladky, A. and Hoogeveen, H. and Kovalyov, M.Y. and Potts, C.N. and Tautenhahn, T. and van de Velde, S.L. (1998). Scheduling a batching machine. https://doi.org/10.1002/(sici)1099-1425(199806)1:1<31::aid-jos4>3.0.co;2-r
    122-/
    123def p12_r0 (R : Reading F) : Prop :=
    124 StronglyNPHard (R.at p12)
    125
    126/-- `1|prec;pj=p;p-batch(∞)|ΣwjUj`: is in P.
    127
    128unknown author (unknown year). see: Earliest Start Schedule. None
    129-/
    130def p13_r0 (R : Reading F) : Prop :=
    131 InP (R.at p13)
    132
    133/-- `1|prec;pj=p;p-batch(∞)|ΣwjTj`: is in P.
    134
    135unknown author (unknown year). see: Earliest Start Schedule. None
    136-/
    137def p14_r0 (R : Reading F) : Prop :=
    138 InP (R.at p14)
    139
    140/-- `1|tree;pj=p;p-batch|Cmax`: is in P.
    141
    142unknown author (unknown year). see: Parallel Machine Problem. None
    143-/
    144def p15_r0 (R : Reading F) : Prop :=
    145 InP (R.at p15)
    146
    147/-- `1|outtree;pj=p;p-batch;rj|Cmax`: is in P.
    148
    149unknown author (unknown year). see: Parallel Machine Problem. None
    150-/
    151def p16_r0 (R : Reading F) : Prop :=
    152 InP (R.at p16)
    153
    154/-- `1|intree;pj=p;p-batch|Lmax`: is in P.
    155
    156unknown author (unknown year). see: Parallel Machine Problem. None
    157-/
    158def p17_r0 (R : Reading F) : Prop :=
    159 InP (R.at p17)
    160
    161/-- `1|pj=1;p-batch;chains;rj|Lmax`: is in P.
    162
    163unknown author (unknown year). see: Parallel Machine Problem. None
    164-/
    165def p18_r0 (R : Reading F) : Prop :=
    166 InP (R.at p18)
    167
    168/-- `1|pj=1;p-batch;outtree;rj|ΣCj`: is in P.
    169
    170unknown author (unknown year). see: Parallel Machine Problem. None
    171-/
    172def p19_r0 (R : Reading F) : Prop :=
    173 InP (R.at p19)
    174
    175/-- `1|pj=p;p-batch;tree|ΣCj`: is in P.
    176
    177unknown author (unknown year). see: Parallel Machine Problem. None
    178-/
    179def p20_r0 (R : Reading F) : Prop :=
    180 InP (R.at p20)
    181
    182/-- `1|pj=p;p-batch|ΣwjTj`: is in P.
    183
    184unknown author (unknown year). see: Parallel Machine Problem. None
    185-/
    186def p21_r0 (R : Reading F) : Prop :=
    187 InP (R.at p21)
    188
    189/-- `1|pj=1;p-batch;rj|ΣwjTj`: is in P.
    190
    191unknown author (unknown year). see: Parallel Machine Problem. None
    192-/
    193def p22_r0 (R : Reading F) : Prop :=
    194 InP (R.at p22)
    195
    196/-- `1|intree;pj=1;p-batch;rj|Cmax`: is strongly NP-hard.
    197
    198unknown author (unknown year). see: Parallel Machine Problem. None
    199-/
    200def p23_r0 (R : Reading F) : Prop :=
    201 StronglyNPHard (R.at p23)
    202
    203/-- `1|prec;pj=1;p-batch|Cmax`: is strongly NP-hard.
    204
    205unknown author (unknown year). see: Parallel Machine Problem. None
    206-/
    207def p24_r0 (R : Reading F) : Prop :=
    208 StronglyNPHard (R.at p24)
    209
    210/-- `1|outtree;pj=1;p-batch|Lmax`: is strongly NP-hard.
    211
    212unknown author (unknown year). see: Parallel Machine Problem. None
    213-/
    214def p25_r0 (R : Reading F) : Prop :=
    215 StronglyNPHard (R.at p25)
    216
    217/-- `1|prec;pj=1;p-batch|ΣCj`: is strongly NP-hard.
    218
    219unknown author (unknown year). see: Parallel Machine Problem. None
    220-/
    221def p26_r0 (R : Reading F) : Prop :=
    222 StronglyNPHard (R.at p26)
    223
    224/-- `1|intree;pj=1;p-batch;rj|ΣCj`: is strongly NP-hard.
    225
    226unknown author (unknown year). see: Parallel Machine Problem. None
    227-/
    228def p27_r0 (R : Reading F) : Prop :=
    229 StronglyNPHard (R.at p27)
    230
    231/-- `1|chains;pj=1;p-batch|ΣwjCj`: is strongly NP-hard.
    232
    233unknown author (unknown year). see: Parallel Machine Problem. None
    234-/
    235def p28_r0 (R : Reading F) : Prop :=
    236 StronglyNPHard (R.at p28)
    237
    238/-- `1|p-batch;rj|ΣCj`: is strongly NP-hard.
    239
    240unknown author (unknown year). see: Single Machine Problem. None
    241-/
    242def p29_r0 (R : Reading F) : Prop :=
    243 StronglyNPHard (R.at p29)
    244
    245/-- `1|chains;pj=1;p-batch|ΣUj`: is strongly NP-hard.
    246
    247unknown author (unknown year). see: Single Machine Problem. None
    248-/
    249def p30_r0 (R : Reading F) : Prop :=
    250 StronglyNPHard (R.at p30)
    251
    252/-- `1|chains;pj=1;p-batch|ΣTj`: is strongly NP-hard.
    253
    254unknown author (unknown year). see: Single Machine Problem. None
    255-/
    256def p31_r0 (R : Reading F) : Prop :=
    257 StronglyNPHard (R.at p31)
    258
    259/-- `1|p-batch;sizej|ΣCj`: is NP-complete.
    260
    261Uzsoy, Reha (1994). Scheduling a single batch processing machine with non-identical job sizes. https://doi.org/10.1080/00207549408957026
    262
    263Note: membership in NP is not stated.
    264-/
    265def p32_r0 (R : Reading F) : Prop :=
    266 NPHard (R.at p32)
    267
    268end Lax434175.ZooParallelBatchingResults
    269
    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…