The Scheduling Zoo, preemptive shop problems
Lax434175.ZooPreemptiveShops · concepts/Lax434175/ZooPreemptiveShops.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
The 24 preemptive shop problems of The Scheduling Zoo, each as a specification, and the 17 relations of the zoo among them that are derived here.
A relation of the zoo states that one problem generalizes another. The 15 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 2 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
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
| 1 | import Lax434175.OperationsFamily |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: The Scheduling Zoo, preemptive shop problems |
| 6 | type: theorem |
| 7 | --- |
| 8 | The 24 preemptive shop problems of The Scheduling Zoo, each as a |
| 9 | specification, and the 17 relations of the zoo among them that are |
| 10 | derived here. |
| 11 | |
| 12 | A relation of the zoo states that one problem generalizes another. The |
| 13 | 15 relations of the first list hold field by field, so that the more |
| 14 | special problem is a special case of the more general one. The |
| 15 | 2 relations of the second list need a threshold step, so that the |
| 16 | decision version of the more special problem reduces to that of the more |
| 17 | general one. |
| 18 | Each pair lists the more general problem first. |
| 19 | |
| 20 | **Theorem.** Every pair of the first list is a special case, and every pair |
| 21 | of the second list is a reduction of decision versions. |
| 22 | -/ |
| 23 | |
| 24 | namespace Lax434175.ZooPreemptiveShops |
| 25 | open Lax434175 Lax434175.Problems Lax434175.Assembly |
| 26 | |
| 27 | /-- The family of the problems listed here. -/ |
| 28 | abbrev F := OperationsFamily.family |
| 29 | |
| 30 | /-- `J|n=k;pmtn|Cmax` -/ |
| 31 | def p0 : Spec F := |
| 32 | OperationsFamily.spec (interruption := .pmtn) (shopType := .job) (jobCount := .constant) |
| 33 | (machineSets := .shop .dedicated) (objective := .makespan) |
| 34 | |
| 35 | /-- `J|n=k;pmtn|ΣCj` -/ |
| 36 | def p1 : Spec F := |
| 37 | OperationsFamily.spec (interruption := .pmtn) (shopType := .job) (jobCount := .constant) |
| 38 | (machineSets := .shop .dedicated) (objective := .sumC) |
| 39 | |
| 40 | /-- `J2|n=3;pmtn|Cmax` -/ |
| 41 | def p2 : Spec F := |
| 42 | OperationsFamily.spec (interruption := .pmtn) (shopType := .job) (jobCount := .atMost 3) |
| 43 | (machineSets := .shop .dedicated) (machineCount := .atMost 2) (objective := .makespan) |
| 44 | |
| 45 | /-- `J2|n=3;pmtn|ΣCj` -/ |
| 46 | def p3 : Spec F := |
| 47 | OperationsFamily.spec (interruption := .pmtn) (shopType := .job) (jobCount := .atMost 3) |
| 48 | (machineSets := .shop .dedicated) (machineCount := .atMost 2) (objective := .sumC) |
| 49 | |
| 50 | /-- `O|pmtn;rj|Lmax` -/ |
| 51 | def p4 : Spec F := |
| 52 | OperationsFamily.spec (interruption := .pmtn) (shopType := .open) (release := .releaseDates) |
| 53 | (machineSets := .shop .byPosition) (objective := .lmax) |
| 54 | |
| 55 | /-- `F2|pmtn|Cmax` -/ |
| 56 | def p5 : Spec F := |
| 57 | OperationsFamily.spec (interruption := .pmtn) (shopType := .flow) |
| 58 | (machineSets := .shop .byPosition) (machineCount := .atMost 2) (objective := .makespan) |
| 59 | |
| 60 | /-- `F2|rj;pmtn|Cmax` -/ |
| 61 | def p6 : Spec F := |
| 62 | OperationsFamily.spec (interruption := .pmtn) (shopType := .flow) (release := .releaseDates) |
| 63 | (machineSets := .shop .byPosition) (machineCount := .atMost 2) (objective := .makespan) |
| 64 | |
| 65 | /-- `F3|pmtn|Cmax` -/ |
| 66 | def p7 : Spec F := |
| 67 | OperationsFamily.spec (interruption := .pmtn) (shopType := .flow) |
| 68 | (machineSets := .shop .byPosition) (machineCount := .atMost 3) (objective := .makespan) |
| 69 | |
| 70 | /-- `F2|pmtn|Lmax` -/ |
| 71 | def p8 : Spec F := |
| 72 | OperationsFamily.spec (interruption := .pmtn) (shopType := .flow) |
| 73 | (machineSets := .shop .byPosition) (machineCount := .atMost 2) (objective := .lmax) |
| 74 | |
| 75 | /-- `O2|pmtn|ΣCj` -/ |
| 76 | def p9 : Spec F := |
| 77 | OperationsFamily.spec (interruption := .pmtn) (shopType := .open) |
| 78 | (machineSets := .shop .byPosition) (machineCount := .atMost 2) (objective := .sumC) |
| 79 | |
| 80 | /-- `F2|pmtn|ΣCj` -/ |
| 81 | def p10 : Spec F := |
| 82 | OperationsFamily.spec (interruption := .pmtn) (shopType := .flow) |
| 83 | (machineSets := .shop .byPosition) (machineCount := .atMost 2) (objective := .sumC) |
| 84 | |
| 85 | /-- `O2|chains;pmtn|Cmax` -/ |
| 86 | def p11 : Spec F := |
| 87 | OperationsFamily.spec (interruption := .pmtn) (shopType := .open) |
| 88 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 89 | (machineCount := .atMost 2) (objective := .makespan) |
| 90 | |
| 91 | /-- `O2|chains;pmtn|ΣCj` -/ |
| 92 | def p12 : Spec F := |
| 93 | OperationsFamily.spec (interruption := .pmtn) (shopType := .open) |
| 94 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 95 | (machineCount := .atMost 2) (objective := .sumC) |
| 96 | |
| 97 | /-- `O2|pmtn|ΣwjCj` -/ |
| 98 | def p13 : Spec F := |
| 99 | OperationsFamily.spec (interruption := .pmtn) (shopType := .open) |
| 100 | (machineSets := .shop .byPosition) (machineCount := .atMost 2) (objective := .sumWC) |
| 101 | |
| 102 | /-- `F2|chains;pmtn|Cmax` -/ |
| 103 | def p14 : Spec F := |
| 104 | OperationsFamily.spec (interruption := .pmtn) (shopType := .flow) |
| 105 | (machineSets := .shop .byPosition) (precedence := ⟨.chains, .zero⟩) |
| 106 | (machineCount := .atMost 2) (objective := .makespan) |
| 107 | |
| 108 | /-- `J2|pmtn|ΣCj` -/ |
| 109 | def p15 : Spec F := |
| 110 | OperationsFamily.spec (interruption := .pmtn) (shopType := .job) |
| 111 | (machineSets := .shop .dedicated) (machineCount := .atMost 2) (objective := .sumC) |
| 112 | |
| 113 | /-- `O3|pmtn|ΣCj` -/ |
| 114 | def p16 : Spec F := |
| 115 | OperationsFamily.spec (interruption := .pmtn) (shopType := .open) |
| 116 | (machineSets := .shop .byPosition) (machineCount := .atMost 3) (objective := .sumC) |
| 117 | |
| 118 | /-- `O2|pmtn|ΣUj` -/ |
| 119 | def p17 : Spec F := |
| 120 | OperationsFamily.spec (interruption := .pmtn) (shopType := .open) |
| 121 | (machineSets := .shop .byPosition) (machineCount := .atMost 2) (objective := .sumU) |
| 122 | |
| 123 | /-- `J2|pmtn|Cmax` -/ |
| 124 | def p18 : Spec F := |
| 125 | OperationsFamily.spec (interruption := .pmtn) (shopType := .job) |
| 126 | (machineSets := .shop .dedicated) (machineCount := .atMost 2) (objective := .makespan) |
| 127 | |
| 128 | /-- `J|prec;rj;n=k;pmtn|ΣwjUj` -/ |
| 129 | def p19 : Spec F := |
| 130 | OperationsFamily.spec (interruption := .pmtn) (shopType := .job) (jobCount := .constant) |
| 131 | (release := .releaseDates) (machineSets := .shop .dedicated) (precedence := ⟨.prec, .zero⟩) |
| 132 | (objective := .sumWU) |
| 133 | |
| 134 | /-- `J|prec;rj;n=k;pmtn|ΣwjTj` -/ |
| 135 | def p20 : Spec F := |
| 136 | OperationsFamily.spec (interruption := .pmtn) (shopType := .job) (jobCount := .constant) |
| 137 | (release := .releaseDates) (machineSets := .shop .dedicated) (precedence := ⟨.prec, .zero⟩) |
| 138 | (objective := .sumWT) |
| 139 | |
| 140 | /-- `J|prec;rj;n=2;pmtn|ΣwjUj` -/ |
| 141 | def p21 : Spec F := |
| 142 | OperationsFamily.spec (interruption := .pmtn) (shopType := .job) (jobCount := .atMost 2) |
| 143 | (release := .releaseDates) (machineSets := .shop .dedicated) (precedence := ⟨.prec, .zero⟩) |
| 144 | (objective := .sumWU) |
| 145 | |
| 146 | /-- `J|prec;rj;n=2;pmtn|ΣwjTj` -/ |
| 147 | def p22 : Spec F := |
| 148 | OperationsFamily.spec (interruption := .pmtn) (shopType := .job) (jobCount := .atMost 2) |
| 149 | (release := .releaseDates) (machineSets := .shop .dedicated) (precedence := ⟨.prec, .zero⟩) |
| 150 | (objective := .sumWT) |
| 151 | |
| 152 | /-- `O2|pmtn;rj|ΣCj` -/ |
| 153 | def p23 : Spec F := |
| 154 | OperationsFamily.spec (interruption := .pmtn) (shopType := .open) (release := .releaseDates) |
| 155 | (machineSets := .shop .byPosition) (machineCount := .atMost 2) (objective := .sumC) |
| 156 | |
| 157 | /-- The problems with their names in three-field notation. -/ |
| 158 | def problems : List (String × Spec F) := [ |
| 159 | ("J|n=k;pmtn|Cmax", p0), |
| 160 | ("J|n=k;pmtn|ΣCj", p1), |
| 161 | ("J2|n=3;pmtn|Cmax", p2), |
| 162 | ("J2|n=3;pmtn|ΣCj", p3), |
| 163 | ("O|pmtn;rj|Lmax", p4), |
| 164 | ("F2|pmtn|Cmax", p5), |
| 165 | ("F2|rj;pmtn|Cmax", p6), |
| 166 | ("F3|pmtn|Cmax", p7), |
| 167 | ("F2|pmtn|Lmax", p8), |
| 168 | ("O2|pmtn|ΣCj", p9), |
| 169 | ("F2|pmtn|ΣCj", p10), |
| 170 | ("O2|chains;pmtn|Cmax", p11), |
| 171 | ("O2|chains;pmtn|ΣCj", p12), |
| 172 | ("O2|pmtn|ΣwjCj", p13), |
| 173 | ("F2|chains;pmtn|Cmax", p14), |
| 174 | ("J2|pmtn|ΣCj", p15), |
| 175 | ("O3|pmtn|ΣCj", p16), |
| 176 | ("O2|pmtn|ΣUj", p17), |
| 177 | ("J2|pmtn|Cmax", p18), |
| 178 | ("J|prec;rj;n=k;pmtn|ΣwjUj", p19), |
| 179 | ("J|prec;rj;n=k;pmtn|ΣwjTj", p20), |
| 180 | ("J|prec;rj;n=2;pmtn|ΣwjUj", p21), |
| 181 | ("J|prec;rj;n=2;pmtn|ΣwjTj", p22), |
| 182 | ("O2|pmtn;rj|ΣCj", p23)] |
| 183 | |
| 184 | /-- The relations that hold field by field: general problem, special problem. -/ |
| 185 | def specialCases : List (Spec F × Spec F) := [ |
| 186 | (p20, p1), (p18, p2), (p15, p3), (p6, p5), (p7, p5), (p8, p5), (p14, p5), (p18, p5), |
| 187 | (p12, p9), (p13, p9), (p16, p9), (p23, p9), (p15, p10), (p19, p21), (p20, p22)] |
| 188 | |
| 189 | /-- The relations that need a threshold step: general problem, special problem. -/ |
| 190 | def thresholdReductions : List (Spec F × Spec F) := [ |
| 191 | (p19, p0), (p20, p0)] |
| 192 | |
| 193 | axiom specialCases_hold : ∀ e ∈ specialCases, |
| 194 | SpecialCase (problem F e.2) (problem F e.1) |
| 195 | |
| 196 | axiom thresholdReductions_hold : ∀ e ∈ thresholdReductions, |
| 197 | Reducible (problem F e.2) (problem F e.1) |
| 198 | |
| 199 | end Lax434175.ZooPreemptiveShops |
| 200 |
Builds on
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments