Lax Lean Archive

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

The Scheduling Zoo, serial batching problems

Lax434175.ZooSerialBatching · concepts/Lax434175/ZooSerialBatching.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 23 serial batching problems of The Scheduling Zoo, each as a specification, and the 16 relations of the zoo among them that are derived here.

    A relation of the zoo states that one problem generalizes another. The 16 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, serial batching problems
    6type: theorem
    7---
    8The 23 serial batching problems of The Scheduling Zoo, each as a
    9specification, and the 16 relations of the zoo among them that are
    10derived here.
    11
    12A relation of the zoo states that one problem generalizes another. The
    1316 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.ZooSerialBatching
    25open Lax434175 Lax434175.Problems Lax434175.Assembly
    26
    27/-- The family of the problems listed here. -/
    28abbrev F := BatchFamily.family
    29
    30/-- `1|prec;pj=p;s-batch|ΣCj` -/
    31def p0 : Spec F :=
    32 BatchFamily.spec .serial (processingTimes := .equal) (capacity := .unbounded)
    33 (precedence := ⟨.prec, .zero⟩) (objective := .sumC)
    34
    35/-- `1|pj=p;s-batch|ΣwjCj` -/
    36def p1 : Spec F :=
    37 BatchFamily.spec .serial (processingTimes := .equal) (capacity := .unbounded)
    38 (objective := .sumWC)
    39
    40/-- `1|chains;s-batch|ΣCj` -/
    41def p2 : Spec F :=
    42 BatchFamily.spec .serial (capacity := .unbounded) (precedence := ⟨.chains, .zero⟩)
    43 (objective := .sumC)
    44
    45/-- `1|chains;pj=1;s-batch|ΣwjCj` -/
    46def p3 : Spec F :=
    47 BatchFamily.spec .serial (processingTimes := .unit) (capacity := .unbounded)
    48 (precedence := ⟨.chains, .zero⟩) (objective := .sumWC)
    49
    50/-- `1|s-batch|ΣwjCj` -/
    51def p4 : Spec F :=
    52 BatchFamily.spec .serial (capacity := .unbounded) (objective := .sumWC)
    53
    54/-- `1|pj=p;s-batch;rj|ΣwjCj` -/
    55def p5 : Spec F :=
    56 BatchFamily.spec .serial (processingTimes := .equal) (release := .releaseDates)
    57 (capacity := .unbounded) (objective := .sumWC)
    58
    59/-- `1|pj=p;s-batch;rj|ΣwjUj` -/
    60def p6 : Spec F :=
    61 BatchFamily.spec .serial (processingTimes := .equal) (release := .releaseDates)
    62 (capacity := .unbounded) (objective := .sumWU)
    63
    64/-- `1|pj=p;s-batch;rj|ΣTj` -/
    65def p7 : Spec F :=
    66 BatchFamily.spec .serial (processingTimes := .equal) (release := .releaseDates)
    67 (capacity := .unbounded) (objective := .sumT)
    68
    69/-- `1|s-batch|ΣTj` -/
    70def p8 : Spec F :=
    71 BatchFamily.spec .serial (capacity := .unbounded) (objective := .sumT)
    72
    73/-- `1|s-batch|ΣUj` -/
    74def p9 : Spec F :=
    75 BatchFamily.spec .serial (capacity := .unbounded) (objective := .sumU)
    76
    77/-- `1|s-batch|ΣwjUj` -/
    78def p10 : Spec F :=
    79 BatchFamily.spec .serial (capacity := .unbounded) (objective := .sumWU)
    80
    81/-- `1|s-batch|ΣCj` -/
    82def p11 : Spec F :=
    83 BatchFamily.spec .serial (capacity := .unbounded) (objective := .sumC)
    84
    85/-- `1|pj=p;s-batch|ΣwjUj` -/
    86def p12 : Spec F :=
    87 BatchFamily.spec .serial (processingTimes := .equal) (capacity := .unbounded)
    88 (objective := .sumWU)
    89
    90/-- `1|prec;s-batch|ΣCj` -/
    91def p13 : Spec F :=
    92 BatchFamily.spec .serial (capacity := .unbounded) (precedence := ⟨.prec, .zero⟩)
    93 (objective := .sumC)
    94
    95/-- `1|chains;pj=1;s-batch|ΣUj` -/
    96def p14 : Spec F :=
    97 BatchFamily.spec .serial (processingTimes := .unit) (capacity := .unbounded)
    98 (precedence := ⟨.chains, .zero⟩) (objective := .sumU)
    99
    100/-- `1|s-batch;rj|Lmax` -/
    101def p15 : Spec F :=
    102 BatchFamily.spec .serial (release := .releaseDates) (capacity := .unbounded)
    103 (objective := .lmax)
    104
    105/-- `1|s-batch;rj|ΣCj` -/
    106def p16 : Spec F :=
    107 BatchFamily.spec .serial (release := .releaseDates) (capacity := .unbounded)
    108 (objective := .sumC)
    109
    110/-- `1|chains;pj=1;s-batch|ΣTj` -/
    111def p17 : Spec F :=
    112 BatchFamily.spec .serial (processingTimes := .unit) (capacity := .unbounded)
    113 (precedence := ⟨.chains, .zero⟩) (objective := .sumT)
    114
    115/-- `1|prec;s-batch|Lmax` -/
    116def p18 : Spec F :=
    117 BatchFamily.spec .serial (capacity := .unbounded) (precedence := ⟨.prec, .zero⟩)
    118 (objective := .lmax)
    119
    120/-- `1|s-batch(∞);rj|ΣwjUj` -/
    121def p19 : Spec F :=
    122 BatchFamily.spec .serial (release := .releaseDates) (capacity := .unbounded)
    123 (objective := .sumWU)
    124
    125/-- `1|s-batch(∞)|ΣwjUj` -/
    126def p20 : Spec F :=
    127 BatchFamily.spec .serial (capacity := .unbounded) (objective := .sumWU)
    128
    129/-- `1|s-batch(b)|ΣwjUj` -/
    130def p21 : Spec F :=
    131 BatchFamily.spec .serial (capacity := .bounded) (objective := .sumWU)
    132
    133/-- `1|s-batch(b);rj|ΣwjUj` -/
    134def p22 : Spec F :=
    135 BatchFamily.spec .serial (release := .releaseDates) (capacity := .bounded) (objective := .sumWU)
    136
    137/-- The problems with their names in three-field notation. -/
    138def problems : List (String × Spec F) := [
    139 ("1|prec;pj=p;s-batch|ΣCj", p0),
    140 ("1|pj=p;s-batch|ΣwjCj", p1),
    141 ("1|chains;s-batch|ΣCj", p2),
    142 ("1|chains;pj=1;s-batch|ΣwjCj", p3),
    143 ("1|s-batch|ΣwjCj", p4),
    144 ("1|pj=p;s-batch;rj|ΣwjCj", p5),
    145 ("1|pj=p;s-batch;rj|ΣwjUj", p6),
    146 ("1|pj=p;s-batch;rj|ΣTj", p7),
    147 ("1|s-batch|ΣTj", p8),
    148 ("1|s-batch|ΣUj", p9),
    149 ("1|s-batch|ΣwjUj", p10),
    150 ("1|s-batch|ΣCj", p11),
    151 ("1|pj=p;s-batch|ΣwjUj", p12),
    152 ("1|prec;s-batch|ΣCj", p13),
    153 ("1|chains;pj=1;s-batch|ΣUj", p14),
    154 ("1|s-batch;rj|Lmax", p15),
    155 ("1|s-batch;rj|ΣCj", p16),
    156 ("1|chains;pj=1;s-batch|ΣTj", p17),
    157 ("1|prec;s-batch|Lmax", p18),
    158 ("1|s-batch(∞);rj|ΣwjUj", p19),
    159 ("1|s-batch(∞)|ΣwjUj", p20),
    160 ("1|s-batch(b)|ΣwjUj", p21),
    161 ("1|s-batch(b);rj|ΣwjUj", p22)]
    162
    163/-- The relations that hold field by field: general problem, special problem. -/
    164def specialCases : List (Spec F × Spec F) := [
    165 (p13, p0), (p4, p1), (p5, p1), (p13, p2), (p10, p9), (p2, p11), (p4, p11), (p8, p11),
    166 (p16, p11), (p6, p12), (p10, p12), (p22, p19), (p10, p20), (p19, p20), (p21, p20), (p22, p21)]
    167
    168/-- The relations that need a threshold step: general problem, special problem. -/
    169def thresholdReductions : List (Spec F × Spec F) := [
    170]
    171
    172axiom specialCases_hold : ∀ e ∈ specialCases,
    173 SpecialCase (problem F e.2) (problem F e.1)
    174
    175axiom thresholdReductions_hold : ∀ e ∈ thresholdReductions,
    176 Reducible (problem F e.2) (problem F e.1)
    177
    178end Lax434175.ZooSerialBatching
    179
    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…