Lax Lean Archive

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

The Scheduling Zoo, parallel batching problems

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

proven

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

    Theorem

    The 35 parallel batching problems of The Scheduling Zoo, each as a specification, and the 10 relations of the zoo among them that are derived here.

    A relation of the zoo states that one problem generalizes another. The 10 relations of the first list hold field by field, so that the more special problem is a special case of the more general one. The 0 relations of the second list need a threshold step, so that the decision version of the more special problem reduces to that of the more general one. Each pair lists the more general problem first.

    Theorem. Every pair of the first list is a special case, and every pair of the second list is a reduction of decision versions.

    Concept map
    15 concepts; 3 descendants hidden
    100%
    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.

    1 specialCases_hold proven

    2 thresholdReductions_hold proven

    Lean source view on GitHub

    1import Lax434175.BatchFamily
    2
    3/-!
    4---
    5title: The Scheduling Zoo, parallel batching problems
    6type: theorem
    7---
    8The 35 parallel batching problems of The Scheduling Zoo, each as a
    9specification, and the 10 relations of the zoo among them that are
    10derived here.
    11
    12A relation of the zoo states that one problem generalizes another. The
    1310 relations of the first list hold field by field, so that the more
    14special problem is a special case of the more general one. The
    150 relations of the second list need a threshold step, so that the
    16decision version of the more special problem reduces to that of the more
    17general one.
    18Each pair lists the more general problem first.
    19
    20**Theorem.** Every pair of the first list is a special case, and every pair
    21of the second list is a reduction of decision versions.
    22-/
    23
    24namespace Lax434175.ZooParallelBatching
    25open Lax434175 Lax434175.Problems Lax434175.Assembly
    26
    27/-- The family of the problems listed here. -/
    28abbrev F := BatchFamily.family
    29
    30/-- `1|pj=p;p-batch;rj|ΣwjCj` -/
    31def p0 : Spec F :=
    32 BatchFamily.spec .parallel (processingTimes := .equal) (release := .releaseDates)
    33 (capacity := .bounded) (objective := .sumWC)
    34
    35/-- `1|pj=p;p-batch;rj|ΣwjUj` -/
    36def p1 : Spec F :=
    37 BatchFamily.spec .parallel (processingTimes := .equal) (release := .releaseDates)
    38 (capacity := .bounded) (objective := .sumWU)
    39
    40/-- `1|pj=p;p-batch;rj|ΣTj` -/
    41def p2 : Spec F :=
    42 BatchFamily.spec .parallel (processingTimes := .equal) (release := .releaseDates)
    43 (capacity := .bounded) (objective := .sumT)
    44
    45/-- `1|pj=p;p-batch(∞);rj|ΣwjTj` -/
    46def p3 : Spec F :=
    47 BatchFamily.spec .parallel (processingTimes := .equal) (release := .releaseDates)
    48 (capacity := .unbounded) (objective := .sumWT)
    49
    50/-- `1|p-batch(∞);rj|ΣwjTj` -/
    51def p4 : Spec F :=
    52 BatchFamily.spec .parallel (release := .releaseDates) (capacity := .unbounded)
    53 (objective := .sumWT)
    54
    55/-- `1|p-batch(∞);rj|ΣwjUj` -/
    56def p5 : Spec F :=
    57 BatchFamily.spec .parallel (release := .releaseDates) (capacity := .unbounded)
    58 (objective := .sumWU)
    59
    60/-- `1|p-batch|Cmax` -/
    61def p6 : Spec F :=
    62 BatchFamily.spec .parallel (capacity := .bounded) (objective := .makespan)
    63
    64/-- `1|p-batch(∞)|ΣwjCj` -/
    65def p7 : Spec F :=
    66 BatchFamily.spec .parallel (capacity := .unbounded) (objective := .sumWC)
    67
    68/-- `1|p-batch(∞)|ΣUj` -/
    69def p8 : Spec F :=
    70 BatchFamily.spec .parallel (capacity := .unbounded) (objective := .sumU)
    71
    72/-- `1|p-batch(∞)|ΣwjUj` -/
    73def p9 : Spec F :=
    74 BatchFamily.spec .parallel (capacity := .unbounded) (objective := .sumWU)
    75
    76/-- `1|p-batch(∞)|ΣwjTj` -/
    77def p10 : Spec F :=
    78 BatchFamily.spec .parallel (capacity := .unbounded) (objective := .sumWT)
    79
    80/-- `1|p-batch;rj|Cmax` -/
    81def p11 : Spec F :=
    82 BatchFamily.spec .parallel (release := .releaseDates) (capacity := .bounded)
    83 (objective := .makespan)
    84
    85/-- `1|p-batch|Lmax` -/
    86def p12 : Spec F :=
    87 BatchFamily.spec .parallel (capacity := .bounded) (objective := .lmax)
    88
    89/-- `1|prec;pj=p;p-batch(∞)|ΣwjUj` -/
    90def p13 : Spec F :=
    91 BatchFamily.spec .parallel (processingTimes := .equal) (capacity := .unbounded)
    92 (precedence := ⟨.prec, .zero⟩) (objective := .sumWU)
    93
    94/-- `1|prec;pj=p;p-batch(∞)|ΣwjTj` -/
    95def p14 : Spec F :=
    96 BatchFamily.spec .parallel (processingTimes := .equal) (capacity := .unbounded)
    97 (precedence := ⟨.prec, .zero⟩) (objective := .sumWT)
    98
    99/-- `1|tree;pj=p;p-batch|Cmax` -/
    100def p15 : Spec F :=
    101 BatchFamily.spec .parallel (processingTimes := .equal) (capacity := .bounded)
    102 (precedence := ⟨.tree, .zero⟩) (objective := .makespan)
    103
    104/-- `1|outtree;pj=p;p-batch;rj|Cmax` -/
    105def p16 : Spec F :=
    106 BatchFamily.spec .parallel (processingTimes := .equal) (release := .releaseDates)
    107 (capacity := .bounded) (precedence := ⟨.outtree, .zero⟩) (objective := .makespan)
    108
    109/-- `1|intree;pj=p;p-batch|Lmax` -/
    110def p17 : Spec F :=
    111 BatchFamily.spec .parallel (processingTimes := .equal) (capacity := .bounded)
    112 (precedence := ⟨.intree, .zero⟩) (objective := .lmax)
    113
    114/-- `1|pj=1;p-batch;chains;rj|Lmax` -/
    115def p18 : Spec F :=
    116 BatchFamily.spec .parallel (processingTimes := .unit) (release := .releaseDates)
    117 (capacity := .bounded) (precedence := ⟨.chains, .zero⟩) (objective := .lmax)
    118
    119/-- `1|pj=1;p-batch;outtree;rj|ΣCj` -/
    120def p19 : Spec F :=
    121 BatchFamily.spec .parallel (processingTimes := .unit) (release := .releaseDates)
    122 (capacity := .bounded) (precedence := ⟨.outtree, .zero⟩) (objective := .sumC)
    123
    124/-- `1|pj=p;p-batch;tree|ΣCj` -/
    125def p20 : Spec F :=
    126 BatchFamily.spec .parallel (processingTimes := .equal) (capacity := .bounded)
    127 (precedence := ⟨.tree, .zero⟩) (objective := .sumC)
    128
    129/-- `1|pj=p;p-batch|ΣwjTj` -/
    130def p21 : Spec F :=
    131 BatchFamily.spec .parallel (processingTimes := .equal) (capacity := .bounded)
    132 (objective := .sumWT)
    133
    134/-- `1|pj=1;p-batch;rj|ΣwjTj` -/
    135def p22 : Spec F :=
    136 BatchFamily.spec .parallel (processingTimes := .unit) (release := .releaseDates)
    137 (capacity := .bounded) (objective := .sumWT)
    138
    139/-- `1|intree;pj=1;p-batch;rj|Cmax` -/
    140def p23 : Spec F :=
    141 BatchFamily.spec .parallel (processingTimes := .unit) (release := .releaseDates)
    142 (capacity := .bounded) (precedence := ⟨.intree, .zero⟩) (objective := .makespan)
    143
    144/-- `1|prec;pj=1;p-batch|Cmax` -/
    145def p24 : Spec F :=
    146 BatchFamily.spec .parallel (processingTimes := .unit) (capacity := .bounded)
    147 (precedence := ⟨.prec, .zero⟩) (objective := .makespan)
    148
    149/-- `1|outtree;pj=1;p-batch|Lmax` -/
    150def p25 : Spec F :=
    151 BatchFamily.spec .parallel (processingTimes := .unit) (capacity := .bounded)
    152 (precedence := ⟨.outtree, .zero⟩) (objective := .lmax)
    153
    154/-- `1|prec;pj=1;p-batch|ΣCj` -/
    155def p26 : Spec F :=
    156 BatchFamily.spec .parallel (processingTimes := .unit) (capacity := .bounded)
    157 (precedence := ⟨.prec, .zero⟩) (objective := .sumC)
    158
    159/-- `1|intree;pj=1;p-batch;rj|ΣCj` -/
    160def p27 : Spec F :=
    161 BatchFamily.spec .parallel (processingTimes := .unit) (release := .releaseDates)
    162 (capacity := .bounded) (precedence := ⟨.intree, .zero⟩) (objective := .sumC)
    163
    164/-- `1|chains;pj=1;p-batch|ΣwjCj` -/
    165def p28 : Spec F :=
    166 BatchFamily.spec .parallel (processingTimes := .unit) (capacity := .bounded)
    167 (precedence := ⟨.chains, .zero⟩) (objective := .sumWC)
    168
    169/-- `1|p-batch;rj|ΣCj` -/
    170def p29 : Spec F :=
    171 BatchFamily.spec .parallel (release := .releaseDates) (capacity := .bounded)
    172 (objective := .sumC)
    173
    174/-- `1|chains;pj=1;p-batch|ΣUj` -/
    175def p30 : Spec F :=
    176 BatchFamily.spec .parallel (processingTimes := .unit) (capacity := .bounded)
    177 (precedence := ⟨.chains, .zero⟩) (objective := .sumU)
    178
    179/-- `1|chains;pj=1;p-batch|ΣTj` -/
    180def p31 : Spec F :=
    181 BatchFamily.spec .parallel (processingTimes := .unit) (capacity := .bounded)
    182 (precedence := ⟨.chains, .zero⟩) (objective := .sumT)
    183
    184/-- `1|p-batch;sizej|ΣCj` -/
    185def p32 : Spec F :=
    186 BatchFamily.spec .parallel (capacity := .sizes) (objective := .sumC)
    187
    188/-- `1|p-batch;sizej|ΣwjCj` -/
    189def p33 : Spec F :=
    190 BatchFamily.spec .parallel (capacity := .sizes) (objective := .sumWC)
    191
    192/-- `1|p-batch;sizej|Cmax` -/
    193def p34 : Spec F :=
    194 BatchFamily.spec .parallel (capacity := .sizes) (objective := .makespan)
    195
    196/-- The problems with their names in three-field notation. -/
    197def problems : List (String × Spec F) := [
    198 ("1|pj=p;p-batch;rj|ΣwjCj", p0),
    199 ("1|pj=p;p-batch;rj|ΣwjUj", p1),
    200 ("1|pj=p;p-batch;rj|ΣTj", p2),
    201 ("1|pj=p;p-batch(∞);rj|ΣwjTj", p3),
    202 ("1|p-batch(∞);rj|ΣwjTj", p4),
    203 ("1|p-batch(∞);rj|ΣwjUj", p5),
    204 ("1|p-batch|Cmax", p6),
    205 ("1|p-batch(∞)|ΣwjCj", p7),
    206 ("1|p-batch(∞)|ΣUj", p8),
    207 ("1|p-batch(∞)|ΣwjUj", p9),
    208 ("1|p-batch(∞)|ΣwjTj", p10),
    209 ("1|p-batch;rj|Cmax", p11),
    210 ("1|p-batch|Lmax", p12),
    211 ("1|prec;pj=p;p-batch(∞)|ΣwjUj", p13),
    212 ("1|prec;pj=p;p-batch(∞)|ΣwjTj", p14),
    213 ("1|tree;pj=p;p-batch|Cmax", p15),
    214 ("1|outtree;pj=p;p-batch;rj|Cmax", p16),
    215 ("1|intree;pj=p;p-batch|Lmax", p17),
    216 ("1|pj=1;p-batch;chains;rj|Lmax", p18),
    217 ("1|pj=1;p-batch;outtree;rj|ΣCj", p19),
    218 ("1|pj=p;p-batch;tree|ΣCj", p20),
    219 ("1|pj=p;p-batch|ΣwjTj", p21),
    220 ("1|pj=1;p-batch;rj|ΣwjTj", p22),
    221 ("1|intree;pj=1;p-batch;rj|Cmax", p23),
    222 ("1|prec;pj=1;p-batch|Cmax", p24),
    223 ("1|outtree;pj=1;p-batch|Lmax", p25),
    224 ("1|prec;pj=1;p-batch|ΣCj", p26),
    225 ("1|intree;pj=1;p-batch;rj|ΣCj", p27),
    226 ("1|chains;pj=1;p-batch|ΣwjCj", p28),
    227 ("1|p-batch;rj|ΣCj", p29),
    228 ("1|chains;pj=1;p-batch|ΣUj", p30),
    229 ("1|chains;pj=1;p-batch|ΣTj", p31),
    230 ("1|p-batch;sizej|ΣCj", p32),
    231 ("1|p-batch;sizej|ΣwjCj", p33),
    232 ("1|p-batch;sizej|Cmax", p34)]
    233
    234/-- The relations that hold field by field: general problem, special problem. -/
    235def specialCases : List (Spec F × Spec F) := [
    236 (p4, p3), (p11, p6), (p12, p6), (p34, p6), (p10, p7), (p33, p7), (p9, p8), (p5, p9),
    237 (p4, p10), (p33, p32)]
    238
    239/-- The relations that need a threshold step: general problem, special problem. -/
    240def thresholdReductions : List (Spec F × Spec F) := [
    241]
    242
    243axiom specialCases_hold : ∀ e ∈ specialCases,
    244 SpecialCase (problem F e.2) (problem F e.1)
    245
    246axiom thresholdReductions_hold : ∀ e ∈ thresholdReductions,
    247 Reducible (problem F e.2) (problem F e.1)
    248
    249end Lax434175.ZooParallelBatching
    250
    Show ProofShow Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…