The Scheduling Zoo, non-preemptive problems on parallel machines
Lax434175.ZooParallel · concepts/Lax434175/ZooParallel.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
The 256 non-preemptive problems on parallel machines of The Scheduling Zoo, each as a specification, and the 251 relations of the zoo among them that are derived here.
A relation of the zoo states that one problem generalizes another. The 242 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 9 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. The 0 relations of the third list replace completion time by flow time and likewise give a reduction of decision versions. Each pair lists the more general problem first.
Theorem. Every pair of the first list is a special case, and every pair of the other lists is a reduction of decision versions.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax434175.OperationsFamily |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: The Scheduling Zoo, non-preemptive problems on parallel machines |
| 6 | type: theorem |
| 7 | --- |
| 8 | The 256 non-preemptive problems on parallel machines of The Scheduling Zoo, each as a |
| 9 | specification, and the 251 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 | 242 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 | 9 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. The 0 relations of the third list replace completion |
| 18 | time by flow time and likewise give a reduction of decision versions. 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 other lists is a reduction of decision versions. |
| 22 | -/ |
| 23 | |
| 24 | namespace Lax434175.ZooParallel |
| 25 | open Lax434175 Lax434175.Problems Lax434175.Assembly |
| 26 | |
| 27 | /-- The family of the problems listed here. -/ |
| 28 | abbrev F := OperationsFamily.family |
| 29 | |
| 30 | /-- `P||Cmax` -/ |
| 31 | def p0 : Spec F := |
| 32 | OperationsFamily.spec (objective := .makespan) |
| 33 | |
| 34 | /-- `P|rj|Cmax` -/ |
| 35 | def p1 : Spec F := |
| 36 | OperationsFamily.spec (release := .releaseDates) (objective := .makespan) |
| 37 | |
| 38 | /-- `P||ΣwjCj` -/ |
| 39 | def p2 : Spec F := |
| 40 | OperationsFamily.spec (objective := .sumWC) |
| 41 | |
| 42 | /-- `P||ΣUj` -/ |
| 43 | def p3 : Spec F := |
| 44 | OperationsFamily.spec (objective := .sumU) |
| 45 | |
| 46 | /-- `P||ΣwjUj` -/ |
| 47 | def p4 : Spec F := |
| 48 | OperationsFamily.spec (objective := .sumWU) |
| 49 | |
| 50 | /-- `R||Cmax` -/ |
| 51 | def p5 : Spec F := |
| 52 | OperationsFamily.spec (environment := .unrelated) (objective := .makespan) |
| 53 | |
| 54 | /-- `Q|online-rj|Fmax` -/ |
| 55 | def p6 : Spec F := |
| 56 | OperationsFamily.spec (environment := .uniform) (release := .online) (objective := .fmax) |
| 57 | |
| 58 | /-- `R|online-rj|Fmax` -/ |
| 59 | def p7 : Spec F := |
| 60 | OperationsFamily.spec (environment := .unrelated) (release := .online) (objective := .fmax) |
| 61 | |
| 62 | /-- `R|online-rj|max wjFj` -/ |
| 63 | def p8 : Spec F := |
| 64 | OperationsFamily.spec (environment := .unrelated) (release := .online) (objective := .maxWF) |
| 65 | |
| 66 | /-- `R|rj|ΣwjCj` -/ |
| 67 | def p9 : Spec F := |
| 68 | OperationsFamily.spec (environment := .unrelated) (release := .releaseDates) |
| 69 | (objective := .sumWC) |
| 70 | |
| 71 | /-- `1|online-rj;pj=1;dj≤rj+4|ΣwjUj` -/ |
| 72 | def p10 : Spec F := |
| 73 | OperationsFamily.spec (processingTimes := .unit) (release := .online) |
| 74 | (machineCount := .atMost 1) (objective := .sumWUWindow 4) |
| 75 | |
| 76 | /-- `1|online-rj;pj=1|ΣwjUj` -/ |
| 77 | def p11 : Spec F := |
| 78 | OperationsFamily.spec (processingTimes := .unit) (release := .online) |
| 79 | (machineCount := .atMost 1) (objective := .sumWU) |
| 80 | |
| 81 | /-- `1|online-rj;pj=1;dj≤rj+2|ΣwjUj` -/ |
| 82 | def p12 : Spec F := |
| 83 | OperationsFamily.spec (processingTimes := .unit) (release := .online) |
| 84 | (machineCount := .atMost 1) (objective := .sumWUWindow 2) |
| 85 | |
| 86 | /-- `1|online-rj;pj=1;dj≤rj+3|ΣwjUj` -/ |
| 87 | def p13 : Spec F := |
| 88 | OperationsFamily.spec (processingTimes := .unit) (release := .online) |
| 89 | (machineCount := .atMost 1) (objective := .sumWUWindow 3) |
| 90 | |
| 91 | /-- `Q||Cmax` -/ |
| 92 | def p14 : Spec F := |
| 93 | OperationsFamily.spec (environment := .uniform) (objective := .makespan) |
| 94 | |
| 95 | /-- `1|prec|ΣwjCj` -/ |
| 96 | def p15 : Spec F := |
| 97 | OperationsFamily.spec (precedence := ⟨.prec, .zero⟩) (machineCount := .atMost 1) |
| 98 | (objective := .sumWC) |
| 99 | |
| 100 | /-- `1|rj;prec|ΣwjCj` -/ |
| 101 | def p16 : Spec F := |
| 102 | OperationsFamily.spec (release := .releaseDates) (precedence := ⟨.prec, .zero⟩) |
| 103 | (machineCount := .atMost 1) (objective := .sumWC) |
| 104 | |
| 105 | /-- `P|prec;pj=1|Cmax` -/ |
| 106 | def p17 : Spec F := |
| 107 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.prec, .zero⟩) |
| 108 | (objective := .makespan) |
| 109 | |
| 110 | /-- `P2|prec;pj∈1,2|Cmax` -/ |
| 111 | def p18 : Spec F := |
| 112 | OperationsFamily.spec (processingTimes := .oneOrTwo) (precedence := ⟨.prec, .zero⟩) |
| 113 | (machineCount := .atMost 2) (objective := .makespan) |
| 114 | |
| 115 | /-- `1|rj|ΣwjCj` -/ |
| 116 | def p19 : Spec F := |
| 117 | OperationsFamily.spec (release := .releaseDates) (machineCount := .atMost 1) |
| 118 | (objective := .sumWC) |
| 119 | |
| 120 | /-- `1|pj=p;rj|ΣwjCj` -/ |
| 121 | def p20 : Spec F := |
| 122 | OperationsFamily.spec (processingTimes := .equal) (release := .releaseDates) |
| 123 | (machineCount := .atMost 1) (objective := .sumWC) |
| 124 | |
| 125 | /-- `1|pj=p;rj|ΣTj` -/ |
| 126 | def p21 : Spec F := |
| 127 | OperationsFamily.spec (processingTimes := .equal) (release := .releaseDates) |
| 128 | (machineCount := .atMost 1) (objective := .sumT) |
| 129 | |
| 130 | /-- `P|pj=p;rj|ΣwjCj` -/ |
| 131 | def p22 : Spec F := |
| 132 | OperationsFamily.spec (processingTimes := .equal) (release := .releaseDates) |
| 133 | (objective := .sumWC) |
| 134 | |
| 135 | /-- `P|pj=p;rj|ΣTj` -/ |
| 136 | def p23 : Spec F := |
| 137 | OperationsFamily.spec (processingTimes := .equal) (release := .releaseDates) |
| 138 | (objective := .sumT) |
| 139 | |
| 140 | /-- `P|rj;pj=p;sizej|Cmax` -/ |
| 141 | def p24 : Spec F := |
| 142 | OperationsFamily.spec (processingTimes := .equal) (release := .releaseDates) |
| 143 | (machineSets := .par .size) (objective := .makespan) |
| 144 | |
| 145 | /-- `P|rj;pj=p;sizej|ΣCj` -/ |
| 146 | def p25 : Spec F := |
| 147 | OperationsFamily.spec (processingTimes := .equal) (release := .releaseDates) |
| 148 | (machineSets := .par .size) (objective := .sumC) |
| 149 | |
| 150 | /-- `1|pj=p;rj|ΣwjUj` -/ |
| 151 | def p26 : Spec F := |
| 152 | OperationsFamily.spec (processingTimes := .equal) (release := .releaseDates) |
| 153 | (machineCount := .atMost 1) (objective := .sumWU) |
| 154 | |
| 155 | /-- `P|pj=p;intree|ΣCj` -/ |
| 156 | def p27 : Spec F := |
| 157 | OperationsFamily.spec (processingTimes := .equal) (precedence := ⟨.intree, .zero⟩) |
| 158 | (objective := .sumC) |
| 159 | |
| 160 | /-- `P|pj=p;tree|ΣCj` -/ |
| 161 | def p28 : Spec F := |
| 162 | OperationsFamily.spec (processingTimes := .equal) (precedence := ⟨.tree, .zero⟩) |
| 163 | (objective := .sumC) |
| 164 | |
| 165 | /-- `P|rj;pj=p|ΣwjUj` -/ |
| 166 | def p29 : Spec F := |
| 167 | OperationsFamily.spec (processingTimes := .equal) (release := .releaseDates) |
| 168 | (objective := .sumWU) |
| 169 | |
| 170 | /-- `P|pj=1;chains;rj|Lmax` -/ |
| 171 | def p30 : Spec F := |
| 172 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 173 | (precedence := ⟨.chains, .zero⟩) (objective := .lmax) |
| 174 | |
| 175 | /-- `R||ΣCj` -/ |
| 176 | def p31 : Spec F := |
| 177 | OperationsFamily.spec (environment := .unrelated) (objective := .sumC) |
| 178 | |
| 179 | /-- `P2||ΣwjCj` -/ |
| 180 | def p32 : Spec F := |
| 181 | OperationsFamily.spec (machineCount := .atMost 2) (objective := .sumWC) |
| 182 | |
| 183 | /-- `Q|Mj|ΣCj` -/ |
| 184 | def p33 : Spec F := |
| 185 | OperationsFamily.spec (environment := .uniform) (machineSets := .par .sets) (objective := .sumC) |
| 186 | |
| 187 | /-- `P2|Mj|ΣwjCj` -/ |
| 188 | def p34 : Spec F := |
| 189 | OperationsFamily.spec (machineSets := .par .sets) (machineCount := .atMost 2) |
| 190 | (objective := .sumWC) |
| 191 | |
| 192 | /-- `P;S1|sj=s;pj=p;rj|Cmax` -/ |
| 193 | def p35 : Spec F := |
| 194 | OperationsFamily.spec (processingTimes := .equal) (release := .releaseDates) (server := .equal) |
| 195 | (objective := .makespan) |
| 196 | |
| 197 | /-- `P;S1|sj=s;pj=p;rj|ΣCj` -/ |
| 198 | def p36 : Spec F := |
| 199 | OperationsFamily.spec (processingTimes := .equal) (release := .releaseDates) (server := .equal) |
| 200 | (objective := .sumC) |
| 201 | |
| 202 | /-- `P;S1|sj=s;pj=1;rj|ΣwjCj` -/ |
| 203 | def p37 : Spec F := |
| 204 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) (server := .equal) |
| 205 | (objective := .sumWC) |
| 206 | |
| 207 | /-- `P;S1|sj=s;pj=1;rj|ΣwjUj` -/ |
| 208 | def p38 : Spec F := |
| 209 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) (server := .equal) |
| 210 | (objective := .sumWU) |
| 211 | |
| 212 | /-- `P;S1|sj=s;pj=1;rj|ΣTj` -/ |
| 213 | def p39 : Spec F := |
| 214 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) (server := .equal) |
| 215 | (objective := .sumT) |
| 216 | |
| 217 | /-- `P2;S1|pj=p|Cmax` -/ |
| 218 | def p40 : Spec F := |
| 219 | OperationsFamily.spec (processingTimes := .equal) (server := .arbitrary) |
| 220 | (machineCount := .atMost 2) (objective := .makespan) |
| 221 | |
| 222 | /-- `P2;S1|pj=p|ΣCj` -/ |
| 223 | def p41 : Spec F := |
| 224 | OperationsFamily.spec (processingTimes := .equal) (server := .arbitrary) |
| 225 | (machineCount := .atMost 2) (objective := .sumC) |
| 226 | |
| 227 | /-- `P2;S1|pj=1;rj|Lmax` -/ |
| 228 | def p42 : Spec F := |
| 229 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 230 | (server := .arbitrary) (machineCount := .atMost 2) (objective := .lmax) |
| 231 | |
| 232 | /-- `P2;S1|pj=1;rj|ΣCj` -/ |
| 233 | def p43 : Spec F := |
| 234 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 235 | (server := .arbitrary) (machineCount := .atMost 2) (objective := .sumC) |
| 236 | |
| 237 | /-- `P;S1|sj=1|ΣCj` -/ |
| 238 | def p44 : Spec F := |
| 239 | OperationsFamily.spec (server := .unit) (objective := .sumC) |
| 240 | |
| 241 | /-- `P3|fixj|Cmax` -/ |
| 242 | def p45 : Spec F := |
| 243 | OperationsFamily.spec (machineSets := .par .fix) (machineCount := .atMost 3) |
| 244 | (objective := .makespan) |
| 245 | |
| 246 | /-- `P|pj=p;sizej|Cmax` -/ |
| 247 | def p46 : Spec F := |
| 248 | OperationsFamily.spec (processingTimes := .equal) (machineSets := .par .size) |
| 249 | (objective := .makespan) |
| 250 | |
| 251 | /-- `P|pj=p;outtree;rj|Cmax` -/ |
| 252 | def p47 : Spec F := |
| 253 | OperationsFamily.spec (processingTimes := .equal) (release := .releaseDates) |
| 254 | (precedence := ⟨.outtree, .zero⟩) (objective := .makespan) |
| 255 | |
| 256 | /-- `P|pj=p;intree|Lmax` -/ |
| 257 | def p48 : Spec F := |
| 258 | OperationsFamily.spec (processingTimes := .equal) (precedence := ⟨.intree, .zero⟩) |
| 259 | (objective := .lmax) |
| 260 | |
| 261 | /-- `P|pj=1;intree;rj|Cmax` -/ |
| 262 | def p49 : Spec F := |
| 263 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 264 | (precedence := ⟨.intree, .zero⟩) (objective := .makespan) |
| 265 | |
| 266 | /-- `P|pj=1;outtree|Lmax` -/ |
| 267 | def p50 : Spec F := |
| 268 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.outtree, .zero⟩) |
| 269 | (objective := .lmax) |
| 270 | |
| 271 | /-- `P|Mj;intree;pj=1;rj|Cmax` -/ |
| 272 | def p51 : Spec F := |
| 273 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 274 | (machineSets := .par .sets) (precedence := ⟨.intree, .zero⟩) (objective := .makespan) |
| 275 | |
| 276 | /-- `P|Mj;outtree;pj=1|Lmax` -/ |
| 277 | def p52 : Spec F := |
| 278 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .sets) |
| 279 | (precedence := ⟨.outtree, .zero⟩) (objective := .lmax) |
| 280 | |
| 281 | /-- `P|pj=1;outtree;rj|ΣCj` -/ |
| 282 | def p53 : Spec F := |
| 283 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 284 | (precedence := ⟨.outtree, .zero⟩) (objective := .sumC) |
| 285 | |
| 286 | /-- `Q2|pj=1;chains|Cmax` -/ |
| 287 | def p54 : Spec F := |
| 288 | OperationsFamily.spec (environment := .uniform) (processingTimes := .unit) |
| 289 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .makespan) |
| 290 | |
| 291 | /-- `P|Mj;pj=1;rj|ΣwjUj` -/ |
| 292 | def p55 : Spec F := |
| 293 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 294 | (machineSets := .par .sets) (objective := .sumWU) |
| 295 | |
| 296 | /-- `Q|Mj;pj=1|ΣwjUj` -/ |
| 297 | def p56 : Spec F := |
| 298 | OperationsFamily.spec (environment := .uniform) (processingTimes := .unit) |
| 299 | (machineSets := .par .sets) (objective := .sumWU) |
| 300 | |
| 301 | /-- `P|Mj;pj=1;rj|ΣwjTj` -/ |
| 302 | def p57 : Spec F := |
| 303 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 304 | (machineSets := .par .sets) (objective := .sumWT) |
| 305 | |
| 306 | /-- `Q|Mj;pj=1|ΣwjTj` -/ |
| 307 | def p58 : Spec F := |
| 308 | OperationsFamily.spec (environment := .uniform) (processingTimes := .unit) |
| 309 | (machineSets := .par .sets) (objective := .sumWT) |
| 310 | |
| 311 | /-- `P2|Mj;chains;pj=1|Cmax` -/ |
| 312 | def p59 : Spec F := |
| 313 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .sets) |
| 314 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .makespan) |
| 315 | |
| 316 | /-- `1|outtree;l;pj=1;rj|Cmax` -/ |
| 317 | def p60 : Spec F := |
| 318 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 319 | (precedence := ⟨.outtree, .constant⟩) (machineCount := .atMost 1) (objective := .makespan) |
| 320 | |
| 321 | /-- `1|tree;l;pj=1|Cmax` -/ |
| 322 | def p61 : Spec F := |
| 323 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.tree, .constant⟩) |
| 324 | (machineCount := .atMost 1) (objective := .makespan) |
| 325 | |
| 326 | /-- `1|intree;l;pj=1|Lmax` -/ |
| 327 | def p62 : Spec F := |
| 328 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.intree, .constant⟩) |
| 329 | (machineCount := .atMost 1) (objective := .lmax) |
| 330 | |
| 331 | /-- `1|prec;l=1;pj=1;rj|Lmax` -/ |
| 332 | def p63 : Spec F := |
| 333 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 334 | (precedence := ⟨.prec, .unit⟩) (machineCount := .atMost 1) (objective := .lmax) |
| 335 | |
| 336 | /-- `P|fixj;rj;pj=1|Cmax` -/ |
| 337 | def p64 : Spec F := |
| 338 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 339 | (machineSets := .par .fix) (objective := .makespan) |
| 340 | |
| 341 | /-- `P|fixj;rj;pj=1|ΣCj` -/ |
| 342 | def p65 : Spec F := |
| 343 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 344 | (machineSets := .par .fix) (objective := .sumC) |
| 345 | |
| 346 | /-- `P|fixj;pj=1|ΣwjCj` -/ |
| 347 | def p66 : Spec F := |
| 348 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .fix) |
| 349 | (objective := .sumWC) |
| 350 | |
| 351 | /-- `P|fixj;pj=1|ΣwjUj` -/ |
| 352 | def p67 : Spec F := |
| 353 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .fix) |
| 354 | (objective := .sumWU) |
| 355 | |
| 356 | /-- `P|fixj;pj=1|ΣTj` -/ |
| 357 | def p68 : Spec F := |
| 358 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .fix) (objective := .sumT) |
| 359 | |
| 360 | /-- `1|outtree;l;pj=1;rj|ΣCj` -/ |
| 361 | def p69 : Spec F := |
| 362 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 363 | (precedence := ⟨.outtree, .constant⟩) (machineCount := .atMost 1) (objective := .sumC) |
| 364 | |
| 365 | /-- `1|prec;l=1;pj=1|ΣCj` -/ |
| 366 | def p70 : Spec F := |
| 367 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.prec, .unit⟩) |
| 368 | (machineCount := .atMost 1) (objective := .sumC) |
| 369 | |
| 370 | /-- `1|intree;l;pj=1;rj|Cmax` -/ |
| 371 | def p71 : Spec F := |
| 372 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 373 | (precedence := ⟨.intree, .constant⟩) (machineCount := .atMost 1) (objective := .makespan) |
| 374 | |
| 375 | /-- `1|outtree;l;pj=1|Lmax` -/ |
| 376 | def p72 : Spec F := |
| 377 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.outtree, .constant⟩) |
| 378 | (machineCount := .atMost 1) (objective := .lmax) |
| 379 | |
| 380 | /-- `1|chains;l|ΣCj` -/ |
| 381 | def p73 : Spec F := |
| 382 | OperationsFamily.spec (precedence := ⟨.chains, .constant⟩) (machineCount := .atMost 1) |
| 383 | (objective := .sumC) |
| 384 | |
| 385 | /-- `1|chains;l;pj=p|ΣCj` -/ |
| 386 | def p74 : Spec F := |
| 387 | OperationsFamily.spec (processingTimes := .equal) (precedence := ⟨.chains, .constant⟩) |
| 388 | (machineCount := .atMost 1) (objective := .sumC) |
| 389 | |
| 390 | /-- `P2|rj;pj=1;sizej|ΣCj` -/ |
| 391 | def p75 : Spec F := |
| 392 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 393 | (machineSets := .par .size) (machineCount := .atMost 2) (objective := .sumC) |
| 394 | |
| 395 | /-- `P|pj=p;sizej|ΣwjUj` -/ |
| 396 | def p76 : Spec F := |
| 397 | OperationsFamily.spec (processingTimes := .equal) (machineSets := .par .size) |
| 398 | (objective := .sumWU) |
| 399 | |
| 400 | /-- `P|pj=p;sizej|ΣTj` -/ |
| 401 | def p77 : Spec F := |
| 402 | OperationsFamily.spec (processingTimes := .equal) (machineSets := .par .size) |
| 403 | (objective := .sumT) |
| 404 | |
| 405 | /-- `P2|chains;rj;pj=1;sizej|Cmax` -/ |
| 406 | def p78 : Spec F := |
| 407 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 408 | (machineSets := .par .size) (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) |
| 409 | (objective := .makespan) |
| 410 | |
| 411 | /-- `P2|chains;pj=1;sizej|Lmax` -/ |
| 412 | def p79 : Spec F := |
| 413 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .size) |
| 414 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .lmax) |
| 415 | |
| 416 | /-- `P2|prec;pj=1;sizej|ΣCj` -/ |
| 417 | def p80 : Spec F := |
| 418 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .size) |
| 419 | (precedence := ⟨.prec, .zero⟩) (machineCount := .atMost 2) (objective := .sumC) |
| 420 | |
| 421 | /-- `P|chains;pj=1;sizej|Cmax` -/ |
| 422 | def p81 : Spec F := |
| 423 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .size) |
| 424 | (precedence := ⟨.chains, .zero⟩) (objective := .makespan) |
| 425 | |
| 426 | /-- `P3|chains;pj=1;sizej|Cmax` -/ |
| 427 | def p82 : Spec F := |
| 428 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .size) |
| 429 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 3) (objective := .makespan) |
| 430 | |
| 431 | /-- `P2|fixj;chains;pj=1|Cmax` -/ |
| 432 | def p83 : Spec F := |
| 433 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .fix) |
| 434 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .makespan) |
| 435 | |
| 436 | /-- `P2|fixj;chains;pj=1|ΣCj` -/ |
| 437 | def p84 : Spec F := |
| 438 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .fix) |
| 439 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .sumC) |
| 440 | |
| 441 | /-- `P2|pj=1;prec;rj|ΣCj` -/ |
| 442 | def p85 : Spec F := |
| 443 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 444 | (precedence := ⟨.prec, .zero⟩) (machineCount := .atMost 2) (objective := .sumC) |
| 445 | |
| 446 | /-- `1|prec;l=1;pj=1;rj|ΣCj` -/ |
| 447 | def p86 : Spec F := |
| 448 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 449 | (precedence := ⟨.prec, .unit⟩) (machineCount := .atMost 1) (objective := .sumC) |
| 450 | |
| 451 | /-- `P2|pj=p;prec|Cmax` -/ |
| 452 | def p87 : Spec F := |
| 453 | OperationsFamily.spec (processingTimes := .equal) (precedence := ⟨.prec, .zero⟩) |
| 454 | (machineCount := .atMost 2) (objective := .makespan) |
| 455 | |
| 456 | /-- `P2|pj=p;prec|ΣCj` -/ |
| 457 | def p88 : Spec F := |
| 458 | OperationsFamily.spec (processingTimes := .equal) (precedence := ⟨.prec, .zero⟩) |
| 459 | (machineCount := .atMost 2) (objective := .sumC) |
| 460 | |
| 461 | /-- `P2|fixj|ΣCj` -/ |
| 462 | def p89 : Spec F := |
| 463 | OperationsFamily.spec (machineSets := .par .fix) (machineCount := .atMost 2) |
| 464 | (objective := .sumC) |
| 465 | |
| 466 | /-- `P|pj=p;tree|Cmax` -/ |
| 467 | def p90 : Spec F := |
| 468 | OperationsFamily.spec (processingTimes := .equal) (precedence := ⟨.tree, .zero⟩) |
| 469 | (objective := .makespan) |
| 470 | |
| 471 | /-- `P|pj=p;sizej|ΣwjCj` -/ |
| 472 | def p91 : Spec F := |
| 473 | OperationsFamily.spec (processingTimes := .equal) (machineSets := .par .size) |
| 474 | (objective := .sumWC) |
| 475 | |
| 476 | /-- `P|pj=1;sizej|ΣCj` -/ |
| 477 | def p92 : Spec F := |
| 478 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .size) |
| 479 | (objective := .sumC) |
| 480 | |
| 481 | /-- `P2|sizej|Cmax` -/ |
| 482 | def p93 : Spec F := |
| 483 | OperationsFamily.spec (machineSets := .par .size) (machineCount := .atMost 2) |
| 484 | (objective := .makespan) |
| 485 | |
| 486 | /-- `P3|sizej|Cmax` -/ |
| 487 | def p94 : Spec F := |
| 488 | OperationsFamily.spec (machineSets := .par .size) (machineCount := .atMost 3) |
| 489 | (objective := .makespan) |
| 490 | |
| 491 | /-- `P5|sizej|Cmax` -/ |
| 492 | def p95 : Spec F := |
| 493 | OperationsFamily.spec (machineSets := .par .size) (machineCount := .atMost 5) |
| 494 | (objective := .makespan) |
| 495 | |
| 496 | /-- `P|sizej|Cmax` -/ |
| 497 | def p96 : Spec F := |
| 498 | OperationsFamily.spec (machineSets := .par .size) (objective := .makespan) |
| 499 | |
| 500 | /-- `1||ΣTj` -/ |
| 501 | def p97 : Spec F := |
| 502 | OperationsFamily.spec (machineCount := .atMost 1) (objective := .sumT) |
| 503 | |
| 504 | /-- `Q|pj=1;rj|ΣCj` -/ |
| 505 | def p98 : Spec F := |
| 506 | OperationsFamily.spec (environment := .uniform) (processingTimes := .unit) |
| 507 | (release := .releaseDates) (objective := .sumC) |
| 508 | |
| 509 | /-- `Q|pj=p;rj|ΣCj` -/ |
| 510 | def p99 : Spec F := |
| 511 | OperationsFamily.spec (environment := .uniform) (processingTimes := .equal) |
| 512 | (release := .releaseDates) (objective := .sumC) |
| 513 | |
| 514 | /-- `P2|chains|Cmax` -/ |
| 515 | def p100 : Spec F := |
| 516 | OperationsFamily.spec (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) |
| 517 | (objective := .makespan) |
| 518 | |
| 519 | /-- `P2|chains|ΣCj` -/ |
| 520 | def p101 : Spec F := |
| 521 | OperationsFamily.spec (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) |
| 522 | (objective := .sumC) |
| 523 | |
| 524 | /-- `P2|Mj;chains|Cmax` -/ |
| 525 | def p102 : Spec F := |
| 526 | OperationsFamily.spec (machineSets := .par .sets) (precedence := ⟨.chains, .zero⟩) |
| 527 | (machineCount := .atMost 2) (objective := .makespan) |
| 528 | |
| 529 | /-- `P2|Mj;chains|ΣCj` -/ |
| 530 | def p103 : Spec F := |
| 531 | OperationsFamily.spec (machineSets := .par .sets) (precedence := ⟨.chains, .zero⟩) |
| 532 | (machineCount := .atMost 2) (objective := .sumC) |
| 533 | |
| 534 | /-- `1|prec;l=1|Cmax` -/ |
| 535 | def p104 : Spec F := |
| 536 | OperationsFamily.spec (precedence := ⟨.prec, .unit⟩) (machineCount := .atMost 1) |
| 537 | (objective := .makespan) |
| 538 | |
| 539 | /-- `P2|pj=p;prec|Lmax` -/ |
| 540 | def p105 : Spec F := |
| 541 | OperationsFamily.spec (processingTimes := .equal) (precedence := ⟨.prec, .zero⟩) |
| 542 | (machineCount := .atMost 2) (objective := .lmax) |
| 543 | |
| 544 | /-- `P2|pj=1;prec;rj|Lmax` -/ |
| 545 | def p106 : Spec F := |
| 546 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 547 | (precedence := ⟨.prec, .zero⟩) (machineCount := .atMost 2) (objective := .lmax) |
| 548 | |
| 549 | /-- `P|Mj|Cmax` -/ |
| 550 | def p107 : Spec F := |
| 551 | OperationsFamily.spec (machineSets := .par .sets) (objective := .makespan) |
| 552 | |
| 553 | /-- `P|pj=p;outtree|ΣCj` -/ |
| 554 | def p108 : Spec F := |
| 555 | OperationsFamily.spec (processingTimes := .equal) (precedence := ⟨.outtree, .zero⟩) |
| 556 | (objective := .sumC) |
| 557 | |
| 558 | /-- `P2;S1|sj=1|ΣCj` -/ |
| 559 | def p109 : Spec F := |
| 560 | OperationsFamily.spec (server := .unit) (machineCount := .atMost 2) (objective := .sumC) |
| 561 | |
| 562 | /-- `P;S1|pj=1|ΣwjCj` -/ |
| 563 | def p110 : Spec F := |
| 564 | OperationsFamily.spec (processingTimes := .unit) (server := .arbitrary) (objective := .sumWC) |
| 565 | |
| 566 | /-- `P;S1|pj=1|ΣUj` -/ |
| 567 | def p111 : Spec F := |
| 568 | OperationsFamily.spec (processingTimes := .unit) (server := .arbitrary) (objective := .sumU) |
| 569 | |
| 570 | /-- `P2;S1|sj=1|Cmax` -/ |
| 571 | def p112 : Spec F := |
| 572 | OperationsFamily.spec (server := .unit) (machineCount := .atMost 2) (objective := .makespan) |
| 573 | |
| 574 | /-- `P2;S1|pj=1|ΣwjUj` -/ |
| 575 | def p113 : Spec F := |
| 576 | OperationsFamily.spec (processingTimes := .unit) (server := .arbitrary) |
| 577 | (machineCount := .atMost 2) (objective := .sumWU) |
| 578 | |
| 579 | /-- `P2;S1|pj=1|ΣTj` -/ |
| 580 | def p114 : Spec F := |
| 581 | OperationsFamily.spec (processingTimes := .unit) (server := .arbitrary) |
| 582 | (machineCount := .atMost 2) (objective := .sumT) |
| 583 | |
| 584 | /-- `P2;S1|sj=s|Cmax` -/ |
| 585 | def p115 : Spec F := |
| 586 | OperationsFamily.spec (server := .equal) (machineCount := .atMost 2) (objective := .makespan) |
| 587 | |
| 588 | /-- `P2;S1|sj=1|Lmax` -/ |
| 589 | def p116 : Spec F := |
| 590 | OperationsFamily.spec (server := .unit) (machineCount := .atMost 2) (objective := .lmax) |
| 591 | |
| 592 | /-- `P2;S1|sj=s|ΣCj` -/ |
| 593 | def p117 : Spec F := |
| 594 | OperationsFamily.spec (server := .equal) (machineCount := .atMost 2) (objective := .sumC) |
| 595 | |
| 596 | /-- `P2;S1|pj=1|ΣwjTj` -/ |
| 597 | def p118 : Spec F := |
| 598 | OperationsFamily.spec (processingTimes := .unit) (server := .arbitrary) |
| 599 | (machineCount := .atMost 2) (objective := .sumWT) |
| 600 | |
| 601 | /-- `P2|fixj|Cmax` -/ |
| 602 | def p119 : Spec F := |
| 603 | OperationsFamily.spec (machineSets := .par .fix) (machineCount := .atMost 2) |
| 604 | (objective := .makespan) |
| 605 | |
| 606 | /-- `P|fixj;pj=1|Cmax` -/ |
| 607 | def p120 : Spec F := |
| 608 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .fix) |
| 609 | (objective := .makespan) |
| 610 | |
| 611 | /-- `P2|fixj;rj|Cmax` -/ |
| 612 | def p121 : Spec F := |
| 613 | OperationsFamily.spec (release := .releaseDates) (machineSets := .par .fix) |
| 614 | (machineCount := .atMost 2) (objective := .makespan) |
| 615 | |
| 616 | /-- `P2|fixj|Lmax` -/ |
| 617 | def p122 : Spec F := |
| 618 | OperationsFamily.spec (machineSets := .par .fix) (machineCount := .atMost 2) |
| 619 | (objective := .lmax) |
| 620 | |
| 621 | /-- `P|fixj;pj=1|ΣCj` -/ |
| 622 | def p123 : Spec F := |
| 623 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .fix) (objective := .sumC) |
| 624 | |
| 625 | /-- `1||ΣwjUj` -/ |
| 626 | def p124 : Spec F := |
| 627 | OperationsFamily.spec (machineCount := .atMost 1) (objective := .sumWU) |
| 628 | |
| 629 | /-- `P|fixj|Cmax` -/ |
| 630 | def p125 : Spec F := |
| 631 | OperationsFamily.spec (machineSets := .par .fix) (objective := .makespan) |
| 632 | |
| 633 | /-- `Q|pj=1;chains|Cmax` -/ |
| 634 | def p126 : Spec F := |
| 635 | OperationsFamily.spec (environment := .uniform) (processingTimes := .unit) |
| 636 | (precedence := ⟨.chains, .zero⟩) (objective := .makespan) |
| 637 | |
| 638 | /-- `Q|pj=p;chains|Cmax` -/ |
| 639 | def p127 : Spec F := |
| 640 | OperationsFamily.spec (environment := .uniform) (processingTimes := .equal) |
| 641 | (precedence := ⟨.chains, .zero⟩) (objective := .makespan) |
| 642 | |
| 643 | /-- `Q|Mj;chains;pj=1|Cmax` -/ |
| 644 | def p128 : Spec F := |
| 645 | OperationsFamily.spec (environment := .uniform) (processingTimes := .unit) |
| 646 | (machineSets := .par .sets) (precedence := ⟨.chains, .zero⟩) (objective := .makespan) |
| 647 | |
| 648 | /-- `P|pj=1;intree;rj|ΣCj` -/ |
| 649 | def p129 : Spec F := |
| 650 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 651 | (precedence := ⟨.intree, .zero⟩) (objective := .sumC) |
| 652 | |
| 653 | /-- `P|Mj|ΣwjCj` -/ |
| 654 | def p130 : Spec F := |
| 655 | OperationsFamily.spec (machineSets := .par .sets) (objective := .sumWC) |
| 656 | |
| 657 | /-- `1|prec;rj|Cmax` -/ |
| 658 | def p131 : Spec F := |
| 659 | OperationsFamily.spec (release := .releaseDates) (precedence := ⟨.prec, .zero⟩) |
| 660 | (machineCount := .atMost 1) (objective := .makespan) |
| 661 | |
| 662 | /-- `1|prec|Lmax` -/ |
| 663 | def p132 : Spec F := |
| 664 | OperationsFamily.spec (precedence := ⟨.prec, .zero⟩) (machineCount := .atMost 1) |
| 665 | (objective := .lmax) |
| 666 | |
| 667 | /-- `1||ΣwjTj` -/ |
| 668 | def p133 : Spec F := |
| 669 | OperationsFamily.spec (machineCount := .atMost 1) (objective := .sumWT) |
| 670 | |
| 671 | /-- `1|sp-graph|ΣwjCj` -/ |
| 672 | def p134 : Spec F := |
| 673 | OperationsFamily.spec (precedence := ⟨.seriesParallel, .zero⟩) (machineCount := .atMost 1) |
| 674 | (objective := .sumWC) |
| 675 | |
| 676 | /-- `1|prec|ΣCj` -/ |
| 677 | def p135 : Spec F := |
| 678 | OperationsFamily.spec (precedence := ⟨.prec, .zero⟩) (machineCount := .atMost 1) |
| 679 | (objective := .sumC) |
| 680 | |
| 681 | /-- `1|bounded height;pj=1|ΣwjCj` -/ |
| 682 | def p136 : Spec F := |
| 683 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.boundedHeight, .zero⟩) |
| 684 | (machineCount := .atMost 1) (objective := .sumWC) |
| 685 | |
| 686 | /-- `P2|prec;pj=p;sizej|Cmax` -/ |
| 687 | def p137 : Spec F := |
| 688 | OperationsFamily.spec (processingTimes := .equal) (machineSets := .par .size) |
| 689 | (precedence := ⟨.prec, .zero⟩) (machineCount := .atMost 2) (objective := .makespan) |
| 690 | |
| 691 | /-- `P|pj=1;sizej|Cmax` -/ |
| 692 | def p138 : Spec F := |
| 693 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .size) |
| 694 | (objective := .makespan) |
| 695 | |
| 696 | /-- `P2|rj;pj=p;sizej|Cmax` -/ |
| 697 | def p139 : Spec F := |
| 698 | OperationsFamily.spec (processingTimes := .equal) (release := .releaseDates) |
| 699 | (machineSets := .par .size) (machineCount := .atMost 2) (objective := .makespan) |
| 700 | |
| 701 | /-- `P2|pj=p;sizej|ΣwjCj` -/ |
| 702 | def p140 : Spec F := |
| 703 | OperationsFamily.spec (processingTimes := .equal) (machineSets := .par .size) |
| 704 | (machineCount := .atMost 2) (objective := .sumWC) |
| 705 | |
| 706 | /-- `P2|rj;sizej|Cmax` -/ |
| 707 | def p141 : Spec F := |
| 708 | OperationsFamily.spec (release := .releaseDates) (machineSets := .par .size) |
| 709 | (machineCount := .atMost 2) (objective := .makespan) |
| 710 | |
| 711 | /-- `P2|sizej|Lmax` -/ |
| 712 | def p142 : Spec F := |
| 713 | OperationsFamily.spec (machineSets := .par .size) (machineCount := .atMost 2) |
| 714 | (objective := .lmax) |
| 715 | |
| 716 | /-- `P2|sizej|ΣCj` -/ |
| 717 | def p143 : Spec F := |
| 718 | OperationsFamily.spec (machineSets := .par .size) (machineCount := .atMost 2) |
| 719 | (objective := .sumC) |
| 720 | |
| 721 | /-- `P2|sizej|ΣwjCj` -/ |
| 722 | def p144 : Spec F := |
| 723 | OperationsFamily.spec (machineSets := .par .size) (machineCount := .atMost 2) |
| 724 | (objective := .sumWC) |
| 725 | |
| 726 | /-- `Q|rj|Cmax` -/ |
| 727 | def p145 : Spec F := |
| 728 | OperationsFamily.spec (environment := .uniform) (release := .releaseDates) |
| 729 | (objective := .makespan) |
| 730 | |
| 731 | /-- `Q||ΣwjCj` -/ |
| 732 | def p146 : Spec F := |
| 733 | OperationsFamily.spec (environment := .uniform) (objective := .sumWC) |
| 734 | |
| 735 | /-- `Q||ΣwjUj` -/ |
| 736 | def p147 : Spec F := |
| 737 | OperationsFamily.spec (environment := .uniform) (objective := .sumWU) |
| 738 | |
| 739 | /-- `1|prec;pj=1|ΣwjCj` -/ |
| 740 | def p148 : Spec F := |
| 741 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.prec, .zero⟩) |
| 742 | (machineCount := .atMost 1) (objective := .sumWC) |
| 743 | |
| 744 | /-- `P|pj=1;bounded height|ΣCj` -/ |
| 745 | def p149 : Spec F := |
| 746 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.boundedHeight, .zero⟩) |
| 747 | (objective := .sumC) |
| 748 | |
| 749 | /-- `P|pj=1;bounded height|Cmax` -/ |
| 750 | def p150 : Spec F := |
| 751 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.boundedHeight, .zero⟩) |
| 752 | (objective := .makespan) |
| 753 | |
| 754 | /-- `P|Mj;prec;pj=1|ΣCj` -/ |
| 755 | def p151 : Spec F := |
| 756 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .sets) |
| 757 | (precedence := ⟨.prec, .zero⟩) (objective := .sumC) |
| 758 | |
| 759 | /-- `1|chains;pj=1;rj|ΣwjCj` -/ |
| 760 | def p152 : Spec F := |
| 761 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 762 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 1) (objective := .sumWC) |
| 763 | |
| 764 | /-- `1|chains;pj=1|ΣUj` -/ |
| 765 | def p153 : Spec F := |
| 766 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.chains, .zero⟩) |
| 767 | (machineCount := .atMost 1) (objective := .sumU) |
| 768 | |
| 769 | /-- `P2|pj=1;intree|ΣwjCj` -/ |
| 770 | def p154 : Spec F := |
| 771 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.intree, .zero⟩) |
| 772 | (machineCount := .atMost 2) (objective := .sumWC) |
| 773 | |
| 774 | /-- `P2|pj=1;outtree|ΣwjCj` -/ |
| 775 | def p155 : Spec F := |
| 776 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.outtree, .zero⟩) |
| 777 | (machineCount := .atMost 2) (objective := .sumWC) |
| 778 | |
| 779 | /-- `P2|Mj;intree;pj=1|ΣwjCj` -/ |
| 780 | def p156 : Spec F := |
| 781 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .sets) |
| 782 | (precedence := ⟨.intree, .zero⟩) (machineCount := .atMost 2) (objective := .sumWC) |
| 783 | |
| 784 | /-- `P2|Mj;outtree;pj=1|ΣwjCj` -/ |
| 785 | def p157 : Spec F := |
| 786 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .sets) |
| 787 | (precedence := ⟨.outtree, .zero⟩) (machineCount := .atMost 2) (objective := .sumWC) |
| 788 | |
| 789 | /-- `1|rj|Lmax` -/ |
| 790 | def p158 : Spec F := |
| 791 | OperationsFamily.spec (release := .releaseDates) (machineCount := .atMost 1) |
| 792 | (objective := .lmax) |
| 793 | |
| 794 | /-- `1|rj|ΣCj` -/ |
| 795 | def p159 : Spec F := |
| 796 | OperationsFamily.spec (release := .releaseDates) (machineCount := .atMost 1) |
| 797 | (objective := .sumC) |
| 798 | |
| 799 | /-- `P2||Cmax` -/ |
| 800 | def p160 : Spec F := |
| 801 | OperationsFamily.spec (machineCount := .atMost 2) (objective := .makespan) |
| 802 | |
| 803 | /-- `P2|Mj|Cmax` -/ |
| 804 | def p161 : Spec F := |
| 805 | OperationsFamily.spec (machineSets := .par .sets) (machineCount := .atMost 2) |
| 806 | (objective := .makespan) |
| 807 | |
| 808 | /-- `1|prec;l;pj=1|Cmax` -/ |
| 809 | def p162 : Spec F := |
| 810 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.prec, .constant⟩) |
| 811 | (machineCount := .atMost 1) (objective := .makespan) |
| 812 | |
| 813 | /-- `1|chains;pj=1|ΣTj` -/ |
| 814 | def p163 : Spec F := |
| 815 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.chains, .zero⟩) |
| 816 | (machineCount := .atMost 1) (objective := .sumT) |
| 817 | |
| 818 | /-- `1||ΣUj` -/ |
| 819 | def p164 : Spec F := |
| 820 | OperationsFamily.spec (machineCount := .atMost 1) (objective := .sumU) |
| 821 | |
| 822 | /-- `P|pj=1;intree|Lmax` -/ |
| 823 | def p165 : Spec F := |
| 824 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.intree, .zero⟩) |
| 825 | (objective := .lmax) |
| 826 | |
| 827 | /-- `1|chains;l;pj=p|Cmax` -/ |
| 828 | def p166 : Spec F := |
| 829 | OperationsFamily.spec (processingTimes := .equal) (precedence := ⟨.chains, .constant⟩) |
| 830 | (machineCount := .atMost 1) (objective := .makespan) |
| 831 | |
| 832 | /-- `1|chains;l=1;pj=p|ΣCj` -/ |
| 833 | def p167 : Spec F := |
| 834 | OperationsFamily.spec (processingTimes := .equal) (precedence := ⟨.chains, .unit⟩) |
| 835 | (machineCount := .atMost 1) (objective := .sumC) |
| 836 | |
| 837 | /-- `1|prec;pj=p;rj|Lmax` -/ |
| 838 | def p168 : Spec F := |
| 839 | OperationsFamily.spec (processingTimes := .equal) (release := .releaseDates) |
| 840 | (precedence := ⟨.prec, .zero⟩) (machineCount := .atMost 1) (objective := .lmax) |
| 841 | |
| 842 | /-- `1|prec;pj=p;rj|ΣCj` -/ |
| 843 | def p169 : Spec F := |
| 844 | OperationsFamily.spec (processingTimes := .equal) (release := .releaseDates) |
| 845 | (precedence := ⟨.prec, .zero⟩) (machineCount := .atMost 1) (objective := .sumC) |
| 846 | |
| 847 | /-- `P|pj=p;rj|Lmax` -/ |
| 848 | def p170 : Spec F := |
| 849 | OperationsFamily.spec (processingTimes := .equal) (release := .releaseDates) |
| 850 | (objective := .lmax) |
| 851 | |
| 852 | /-- `P|pj=p;rj|ΣCj` -/ |
| 853 | def p171 : Spec F := |
| 854 | OperationsFamily.spec (processingTimes := .equal) (release := .releaseDates) |
| 855 | (objective := .sumC) |
| 856 | |
| 857 | /-- `P2|chains;pj=1|ΣwjCj` -/ |
| 858 | def p172 : Spec F := |
| 859 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.chains, .zero⟩) |
| 860 | (machineCount := .atMost 2) (objective := .sumWC) |
| 861 | |
| 862 | /-- `P2|Mj;chains;pj=1|ΣwjCj` -/ |
| 863 | def p173 : Spec F := |
| 864 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .sets) |
| 865 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .sumWC) |
| 866 | |
| 867 | /-- `1|chains;l=1;pj=1|ΣwjCj` -/ |
| 868 | def p174 : Spec F := |
| 869 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.chains, .unit⟩) |
| 870 | (machineCount := .atMost 1) (objective := .sumWC) |
| 871 | |
| 872 | /-- `P|Mj;prec;pj=1|Cmax` -/ |
| 873 | def p175 : Spec F := |
| 874 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .sets) |
| 875 | (precedence := ⟨.prec, .zero⟩) (objective := .makespan) |
| 876 | |
| 877 | /-- `1|chains;l|Cmax` -/ |
| 878 | def p176 : Spec F := |
| 879 | OperationsFamily.spec (precedence := ⟨.chains, .constant⟩) (machineCount := .atMost 1) |
| 880 | (objective := .makespan) |
| 881 | |
| 882 | /-- `1|chains;lij;pj=1|Cmax` -/ |
| 883 | def p177 : Spec F := |
| 884 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.chains, .arbitrary⟩) |
| 885 | (machineCount := .atMost 1) (objective := .makespan) |
| 886 | |
| 887 | /-- `P2|outtree;pj=1;sizej|ΣCj` -/ |
| 888 | def p178 : Spec F := |
| 889 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .size) |
| 890 | (precedence := ⟨.outtree, .zero⟩) (machineCount := .atMost 2) (objective := .sumC) |
| 891 | |
| 892 | /-- `P2|intree;pj=1;sizej|ΣCj` -/ |
| 893 | def p179 : Spec F := |
| 894 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .size) |
| 895 | (precedence := ⟨.intree, .zero⟩) (machineCount := .atMost 2) (objective := .sumC) |
| 896 | |
| 897 | /-- `1|pj=1;rj|ΣwjTj` -/ |
| 898 | def p180 : Spec F := |
| 899 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 900 | (machineCount := .atMost 1) (objective := .sumWT) |
| 901 | |
| 902 | /-- `1|pj=p|ΣwjTj` -/ |
| 903 | def p181 : Spec F := |
| 904 | OperationsFamily.spec (processingTimes := .equal) (machineCount := .atMost 1) |
| 905 | (objective := .sumWT) |
| 906 | |
| 907 | /-- `P|pj=p|ΣwjUj` -/ |
| 908 | def p182 : Spec F := |
| 909 | OperationsFamily.spec (processingTimes := .equal) (objective := .sumWU) |
| 910 | |
| 911 | /-- `P|pj=p|ΣwjTj` -/ |
| 912 | def p183 : Spec F := |
| 913 | OperationsFamily.spec (processingTimes := .equal) (objective := .sumWT) |
| 914 | |
| 915 | /-- `P;S1|sj=s;pj=p|ΣwjUj` -/ |
| 916 | def p184 : Spec F := |
| 917 | OperationsFamily.spec (processingTimes := .equal) (server := .equal) (objective := .sumWU) |
| 918 | |
| 919 | /-- `P;S1|sj=1;pj=1;rj|ΣwjTj` -/ |
| 920 | def p185 : Spec F := |
| 921 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) (server := .unit) |
| 922 | (objective := .sumWT) |
| 923 | |
| 924 | /-- `P;S1|sj=s;pj=p|ΣwjTj` -/ |
| 925 | def p186 : Spec F := |
| 926 | OperationsFamily.spec (processingTimes := .equal) (server := .equal) (objective := .sumWT) |
| 927 | |
| 928 | /-- `Q|pj=p;rj|Cmax` -/ |
| 929 | def p187 : Spec F := |
| 930 | OperationsFamily.spec (environment := .uniform) (processingTimes := .equal) |
| 931 | (release := .releaseDates) (objective := .makespan) |
| 932 | |
| 933 | /-- `Q|pj=p|ΣwjUj` -/ |
| 934 | def p188 : Spec F := |
| 935 | OperationsFamily.spec (environment := .uniform) (processingTimes := .equal) |
| 936 | (objective := .sumWU) |
| 937 | |
| 938 | /-- `Q|pj=p|ΣwjTj` -/ |
| 939 | def p189 : Spec F := |
| 940 | OperationsFamily.spec (environment := .uniform) (processingTimes := .equal) |
| 941 | (objective := .sumWT) |
| 942 | |
| 943 | /-- `P|pj=1;rj|ΣwjUj` -/ |
| 944 | def p190 : Spec F := |
| 945 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 946 | (objective := .sumWU) |
| 947 | |
| 948 | /-- `P|pj=1;rj|ΣwjTj` -/ |
| 949 | def p191 : Spec F := |
| 950 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 951 | (objective := .sumWT) |
| 952 | |
| 953 | /-- `P2|rj|ΣCj` -/ |
| 954 | def p192 : Spec F := |
| 955 | OperationsFamily.spec (release := .releaseDates) (machineCount := .atMost 2) |
| 956 | (objective := .sumC) |
| 957 | |
| 958 | /-- `P2|pj=1;chains;rj|ΣwjCj` -/ |
| 959 | def p193 : Spec F := |
| 960 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 961 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .sumWC) |
| 962 | |
| 963 | /-- `P2|pj=1;chains|ΣUj` -/ |
| 964 | def p194 : Spec F := |
| 965 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.chains, .zero⟩) |
| 966 | (machineCount := .atMost 2) (objective := .sumU) |
| 967 | |
| 968 | /-- `P2|pj=1;chains|ΣTj` -/ |
| 969 | def p195 : Spec F := |
| 970 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.chains, .zero⟩) |
| 971 | (machineCount := .atMost 2) (objective := .sumT) |
| 972 | |
| 973 | /-- `P2|Mj;rj|ΣCj` -/ |
| 974 | def p196 : Spec F := |
| 975 | OperationsFamily.spec (release := .releaseDates) (machineSets := .par .sets) |
| 976 | (machineCount := .atMost 2) (objective := .sumC) |
| 977 | |
| 978 | /-- `P2|Mj;chains;pj=1;rj|ΣwjCj` -/ |
| 979 | def p197 : Spec F := |
| 980 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 981 | (machineSets := .par .sets) (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) |
| 982 | (objective := .sumWC) |
| 983 | |
| 984 | /-- `P2|Mj;chains;pj=1|ΣUj` -/ |
| 985 | def p198 : Spec F := |
| 986 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .sets) |
| 987 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .sumU) |
| 988 | |
| 989 | /-- `P2|Mj;chains;pj=1|ΣTj` -/ |
| 990 | def p199 : Spec F := |
| 991 | OperationsFamily.spec (processingTimes := .unit) (machineSets := .par .sets) |
| 992 | (precedence := ⟨.chains, .zero⟩) (machineCount := .atMost 2) (objective := .sumT) |
| 993 | |
| 994 | /-- `P|Mj|ΣwjZj` -/ |
| 995 | def p200 : Spec F := |
| 996 | OperationsFamily.spec (machineSets := .par .sets) (objective := .sumWZ) |
| 997 | |
| 998 | /-- `P|Mj|ΣZj` -/ |
| 999 | def p201 : Spec F := |
| 1000 | OperationsFamily.spec (machineSets := .par .sets) (objective := .sumZ) |
| 1001 | |
| 1002 | /-- `P||ΣwjZj` -/ |
| 1003 | def p202 : Spec F := |
| 1004 | OperationsFamily.spec (objective := .sumWZ) |
| 1005 | |
| 1006 | /-- `P|Mj;pj=p|ΣZj` -/ |
| 1007 | def p203 : Spec F := |
| 1008 | OperationsFamily.spec (processingTimes := .equal) (machineSets := .par .sets) |
| 1009 | (objective := .sumZ) |
| 1010 | |
| 1011 | /-- `P|Mj;pj=p|ΣwjZj` -/ |
| 1012 | def p204 : Spec F := |
| 1013 | OperationsFamily.spec (processingTimes := .equal) (machineSets := .par .sets) |
| 1014 | (objective := .sumWZ) |
| 1015 | |
| 1016 | /-- `1||ΣZj` -/ |
| 1017 | def p205 : Spec F := |
| 1018 | OperationsFamily.spec (machineCount := .atMost 1) (objective := .sumZ) |
| 1019 | |
| 1020 | /-- `P||ΣZj` -/ |
| 1021 | def p206 : Spec F := |
| 1022 | OperationsFamily.spec (objective := .sumZ) |
| 1023 | |
| 1024 | /-- `1||ΣwjZj` -/ |
| 1025 | def p207 : Spec F := |
| 1026 | OperationsFamily.spec (machineCount := .atMost 1) (objective := .sumWZ) |
| 1027 | |
| 1028 | /-- `R||ΣwjZj` -/ |
| 1029 | def p208 : Spec F := |
| 1030 | OperationsFamily.spec (environment := .unrelated) (objective := .sumWZ) |
| 1031 | |
| 1032 | /-- `1|2-dim partial order|ΣwjCj` -/ |
| 1033 | def p209 : Spec F := |
| 1034 | OperationsFamily.spec (precedence := ⟨.dimensionTwo, .zero⟩) (machineCount := .atMost 1) |
| 1035 | (objective := .sumWC) |
| 1036 | |
| 1037 | /-- `1|interval order|ΣwjCj` -/ |
| 1038 | def p210 : Spec F := |
| 1039 | OperationsFamily.spec (precedence := ⟨.intervalOrder, .zero⟩) (machineCount := .atMost 1) |
| 1040 | (objective := .sumWC) |
| 1041 | |
| 1042 | /-- `P|opposing forest;pj=p|Cmax` -/ |
| 1043 | def p211 : Spec F := |
| 1044 | OperationsFamily.spec (processingTimes := .equal) (precedence := ⟨.opposingForest, .zero⟩) |
| 1045 | (objective := .makespan) |
| 1046 | |
| 1047 | /-- `P|opposing forest;pj=1|Cmax` -/ |
| 1048 | def p212 : Spec F := |
| 1049 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.opposingForest, .zero⟩) |
| 1050 | (objective := .makespan) |
| 1051 | |
| 1052 | /-- `P|bounded height;pj=p|Cmax` -/ |
| 1053 | def p213 : Spec F := |
| 1054 | OperationsFamily.spec (processingTimes := .equal) (precedence := ⟨.boundedHeight, .zero⟩) |
| 1055 | (objective := .makespan) |
| 1056 | |
| 1057 | /-- `P|level order;pj=p|Cmax` -/ |
| 1058 | def p214 : Spec F := |
| 1059 | OperationsFamily.spec (processingTimes := .equal) (precedence := ⟨.levelOrder, .zero⟩) |
| 1060 | (objective := .makespan) |
| 1061 | |
| 1062 | /-- `P|interval order;pj=p|Cmax` -/ |
| 1063 | def p215 : Spec F := |
| 1064 | OperationsFamily.spec (processingTimes := .equal) (precedence := ⟨.intervalOrder, .zero⟩) |
| 1065 | (objective := .makespan) |
| 1066 | |
| 1067 | /-- `P|interval order;pj=p|ΣCj` -/ |
| 1068 | def p216 : Spec F := |
| 1069 | OperationsFamily.spec (processingTimes := .equal) (precedence := ⟨.intervalOrder, .zero⟩) |
| 1070 | (objective := .sumC) |
| 1071 | |
| 1072 | /-- `P|quasi-interval order;pj=p|Cmax` -/ |
| 1073 | def p217 : Spec F := |
| 1074 | OperationsFamily.spec (processingTimes := .equal) (precedence := ⟨.quasiInterval, .zero⟩) |
| 1075 | (objective := .makespan) |
| 1076 | |
| 1077 | /-- `P|over-interval order;pj=p|Cmax` -/ |
| 1078 | def p218 : Spec F := |
| 1079 | OperationsFamily.spec (processingTimes := .equal) (precedence := ⟨.overInterval, .zero⟩) |
| 1080 | (objective := .makespan) |
| 1081 | |
| 1082 | /-- `P|DC-graph;pj=p|Cmax` -/ |
| 1083 | def p219 : Spec F := |
| 1084 | OperationsFamily.spec (processingTimes := .equal) (precedence := ⟨.divideAndConquer, .zero⟩) |
| 1085 | (objective := .makespan) |
| 1086 | |
| 1087 | /-- `P|prec;l=1;pj=1|Cmax` -/ |
| 1088 | def p220 : Spec F := |
| 1089 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.prec, .unit⟩) |
| 1090 | (objective := .makespan) |
| 1091 | |
| 1092 | /-- `R|rj|ΣCj` -/ |
| 1093 | def p221 : Spec F := |
| 1094 | OperationsFamily.spec (environment := .unrelated) (release := .releaseDates) |
| 1095 | (objective := .sumC) |
| 1096 | |
| 1097 | /-- `R||ΣwjCj` -/ |
| 1098 | def p222 : Spec F := |
| 1099 | OperationsFamily.spec (environment := .unrelated) (objective := .sumWC) |
| 1100 | |
| 1101 | /-- `P|prec;pj=1|ΣCj` -/ |
| 1102 | def p223 : Spec F := |
| 1103 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.prec, .zero⟩) |
| 1104 | (objective := .sumC) |
| 1105 | |
| 1106 | /-- `P|prec;l=1;pj=1|ΣCj` -/ |
| 1107 | def p224 : Spec F := |
| 1108 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.prec, .unit⟩) |
| 1109 | (objective := .sumC) |
| 1110 | |
| 1111 | /-- `P|rj|ΣwjCj` -/ |
| 1112 | def p225 : Spec F := |
| 1113 | OperationsFamily.spec (release := .releaseDates) (objective := .sumWC) |
| 1114 | |
| 1115 | /-- `1|online-rj|ΣwjCj` -/ |
| 1116 | def p226 : Spec F := |
| 1117 | OperationsFamily.spec (release := .online) (machineCount := .atMost 1) (objective := .sumWC) |
| 1118 | |
| 1119 | /-- `1|dj=d|ΣwjTj` -/ |
| 1120 | def p227 : Spec F := |
| 1121 | OperationsFamily.spec (machineCount := .atMost 1) (objective := .sumWTCommon) |
| 1122 | |
| 1123 | /-- `1|pj=1;prec;lij≤0|Lmax` -/ |
| 1124 | def p228 : Spec F := |
| 1125 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.prec, .arbitraryNonpositive⟩) |
| 1126 | (machineCount := .atMost 1) (objective := .lmax) |
| 1127 | |
| 1128 | /-- `P|rj;pj=1;sizej∈1,m|Lmax` -/ |
| 1129 | def p229 : Spec F := |
| 1130 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 1131 | (machineSets := .par .sizeOneOrAll) (objective := .lmax) |
| 1132 | |
| 1133 | /-- `1|rj;pj=p|ΣUj` -/ |
| 1134 | def p230 : Spec F := |
| 1135 | OperationsFamily.spec (processingTimes := .equal) (release := .releaseDates) |
| 1136 | (machineCount := .atMost 1) (objective := .sumU) |
| 1137 | |
| 1138 | /-- `P2|rj;pj=1;sizej|Lmax` -/ |
| 1139 | def p231 : Spec F := |
| 1140 | OperationsFamily.spec (processingTimes := .unit) (release := .releaseDates) |
| 1141 | (machineSets := .par .size) (machineCount := .atMost 2) (objective := .lmax) |
| 1142 | |
| 1143 | /-- `P2|rj|Lmax` -/ |
| 1144 | def p232 : Spec F := |
| 1145 | OperationsFamily.spec (release := .releaseDates) (machineCount := .atMost 2) |
| 1146 | (objective := .lmax) |
| 1147 | |
| 1148 | /-- `P|Mj;prec;rj|Lmax` -/ |
| 1149 | def p233 : Spec F := |
| 1150 | OperationsFamily.spec (release := .releaseDates) (machineSets := .par .sets) |
| 1151 | (precedence := ⟨.prec, .zero⟩) (objective := .lmax) |
| 1152 | |
| 1153 | /-- `P|Mj;prec;rj;l|Cmax` -/ |
| 1154 | def p234 : Spec F := |
| 1155 | OperationsFamily.spec (release := .releaseDates) (machineSets := .par .sets) |
| 1156 | (precedence := ⟨.prec, .constant⟩) (objective := .makespan) |
| 1157 | |
| 1158 | /-- `P|Mj;prec;rj;l|Lmax` -/ |
| 1159 | def p235 : Spec F := |
| 1160 | OperationsFamily.spec (release := .releaseDates) (machineSets := .par .sets) |
| 1161 | (precedence := ⟨.prec, .constant⟩) (objective := .lmax) |
| 1162 | |
| 1163 | /-- `P|Mj;prec;rj;d̄j=d̄|Cmax` -/ |
| 1164 | def p236 : Spec F := |
| 1165 | OperationsFamily.spec (release := .releaseDates) (deadline := .common) |
| 1166 | (machineSets := .par .sets) (precedence := ⟨.prec, .zero⟩) (objective := .makespan) |
| 1167 | |
| 1168 | /-- `1|rj|ΣwjUj` -/ |
| 1169 | def p237 : Spec F := |
| 1170 | OperationsFamily.spec (release := .releaseDates) (machineCount := .atMost 1) |
| 1171 | (objective := .sumWU) |
| 1172 | |
| 1173 | /-- `P|rj;pj=p|ΣUj` -/ |
| 1174 | def p238 : Spec F := |
| 1175 | OperationsFamily.spec (processingTimes := .equal) (release := .releaseDates) |
| 1176 | (objective := .sumU) |
| 1177 | |
| 1178 | /-- `P|rj;prec|ΣwjCj` -/ |
| 1179 | def p239 : Spec F := |
| 1180 | OperationsFamily.spec (release := .releaseDates) (precedence := ⟨.prec, .zero⟩) |
| 1181 | (objective := .sumWC) |
| 1182 | |
| 1183 | /-- `P|prec|ΣwjCj` -/ |
| 1184 | def p240 : Spec F := |
| 1185 | OperationsFamily.spec (precedence := ⟨.prec, .zero⟩) (objective := .sumWC) |
| 1186 | |
| 1187 | /-- `P|prec;pj=1|ΣwjCj` -/ |
| 1188 | def p241 : Spec F := |
| 1189 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.prec, .zero⟩) |
| 1190 | (objective := .sumWC) |
| 1191 | |
| 1192 | /-- `Q|prec|ΣwjCj` -/ |
| 1193 | def p242 : Spec F := |
| 1194 | OperationsFamily.spec (environment := .uniform) (precedence := ⟨.prec, .zero⟩) |
| 1195 | (objective := .sumWC) |
| 1196 | |
| 1197 | /-- `1|pj=p;online-rj|ΣUj` -/ |
| 1198 | def p243 : Spec F := |
| 1199 | OperationsFamily.spec (processingTimes := .equal) (release := .online) |
| 1200 | (machineCount := .atMost 1) (objective := .sumU) |
| 1201 | |
| 1202 | /-- `P∞|pj=1;prec;c=1|Cmax` -/ |
| 1203 | def p244 : Spec F := |
| 1204 | OperationsFamily.spec (processingTimes := .unit) (communicationDelays := .unit) |
| 1205 | (precedence := ⟨.prec, .zero⟩) (machineCount := .unlimited) (objective := .makespan) |
| 1206 | |
| 1207 | /-- `P|pj=1;prec;c=1|Cmax` -/ |
| 1208 | def p245 : Spec F := |
| 1209 | OperationsFamily.spec (processingTimes := .unit) (communicationDelays := .unit) |
| 1210 | (precedence := ⟨.prec, .zero⟩) (objective := .makespan) |
| 1211 | |
| 1212 | /-- `P∞|pj=1;prec;c|Cmax` -/ |
| 1213 | def p246 : Spec F := |
| 1214 | OperationsFamily.spec (processingTimes := .unit) (communicationDelays := .general) |
| 1215 | (precedence := ⟨.prec, .zero⟩) (machineCount := .unlimited) (objective := .makespan) |
| 1216 | |
| 1217 | /-- `P|pj=1;prec;c|Cmax` -/ |
| 1218 | def p247 : Spec F := |
| 1219 | OperationsFamily.spec (processingTimes := .unit) (communicationDelays := .general) |
| 1220 | (precedence := ⟨.prec, .zero⟩) (objective := .makespan) |
| 1221 | |
| 1222 | /-- `P|prec;c|Cmax` -/ |
| 1223 | def p248 : Spec F := |
| 1224 | OperationsFamily.spec (communicationDelays := .general) (precedence := ⟨.prec, .zero⟩) |
| 1225 | (objective := .makespan) |
| 1226 | |
| 1227 | /-- `P∞|prec;c|Cmax` -/ |
| 1228 | def p249 : Spec F := |
| 1229 | OperationsFamily.spec (communicationDelays := .general) (precedence := ⟨.prec, .zero⟩) |
| 1230 | (machineCount := .unlimited) (objective := .makespan) |
| 1231 | |
| 1232 | /-- `Q|prec;c|ΣwjCj` -/ |
| 1233 | def p250 : Spec F := |
| 1234 | OperationsFamily.spec (environment := .uniform) (communicationDelays := .general) |
| 1235 | (precedence := ⟨.prec, .zero⟩) (objective := .sumWC) |
| 1236 | |
| 1237 | /-- `Q|prec;c;pj=1|ΣwjCj` -/ |
| 1238 | def p251 : Spec F := |
| 1239 | OperationsFamily.spec (environment := .uniform) (processingTimes := .unit) |
| 1240 | (communicationDelays := .general) (precedence := ⟨.prec, .zero⟩) (objective := .sumWC) |
| 1241 | |
| 1242 | /-- `1|rj|ΣUj` -/ |
| 1243 | def p252 : Spec F := |
| 1244 | OperationsFamily.spec (release := .releaseDates) (machineCount := .atMost 1) |
| 1245 | (objective := .sumU) |
| 1246 | |
| 1247 | /-- `1|forbidden-times|Cmax` -/ |
| 1248 | def p253 : Spec F := |
| 1249 | OperationsFamily.spec (forbiddenTimes := .forbidden) (machineCount := .atMost 1) |
| 1250 | (objective := .makespan) |
| 1251 | |
| 1252 | /-- `P|HM|Cmax` -/ |
| 1253 | def p254 : Spec F := |
| 1254 | OperationsFamily.spec (encoding := .highMultiplicity) (objective := .makespan) |
| 1255 | |
| 1256 | /-- `P3|prec;pj=1|Cmax` -/ |
| 1257 | def p255 : Spec F := |
| 1258 | OperationsFamily.spec (processingTimes := .unit) (precedence := ⟨.prec, .zero⟩) |
| 1259 | (machineCount := .atMost 3) (objective := .makespan) |
| 1260 | |
| 1261 | /-- The problems with their names in three-field notation. -/ |
| 1262 | def problems : List (String × Spec F) := [ |
| 1263 | ("P||Cmax", p0), |
| 1264 | ("P|rj|Cmax", p1), |
| 1265 | ("P||ΣwjCj", p2), |
| 1266 | ("P||ΣUj", p3), |
| 1267 | ("P||ΣwjUj", p4), |
| 1268 | ("R||Cmax", p5), |
| 1269 | ("Q|online-rj|Fmax", p6), |
| 1270 | ("R|online-rj|Fmax", p7), |
| 1271 | ("R|online-rj|max wjFj", p8), |
| 1272 | ("R|rj|ΣwjCj", p9), |
| 1273 | ("1|online-rj;pj=1;dj≤rj+4|ΣwjUj", p10), |
| 1274 | ("1|online-rj;pj=1|ΣwjUj", p11), |
| 1275 | ("1|online-rj;pj=1;dj≤rj+2|ΣwjUj", p12), |
| 1276 | ("1|online-rj;pj=1;dj≤rj+3|ΣwjUj", p13), |
| 1277 | ("Q||Cmax", p14), |
| 1278 | ("1|prec|ΣwjCj", p15), |
| 1279 | ("1|rj;prec|ΣwjCj", p16), |
| 1280 | ("P|prec;pj=1|Cmax", p17), |
| 1281 | ("P2|prec;pj∈1,2|Cmax", p18), |
| 1282 | ("1|rj|ΣwjCj", p19), |
| 1283 | ("1|pj=p;rj|ΣwjCj", p20), |
| 1284 | ("1|pj=p;rj|ΣTj", p21), |
| 1285 | ("P|pj=p;rj|ΣwjCj", p22), |
| 1286 | ("P|pj=p;rj|ΣTj", p23), |
| 1287 | ("P|rj;pj=p;sizej|Cmax", p24), |
| 1288 | ("P|rj;pj=p;sizej|ΣCj", p25), |
| 1289 | ("1|pj=p;rj|ΣwjUj", p26), |
| 1290 | ("P|pj=p;intree|ΣCj", p27), |
| 1291 | ("P|pj=p;tree|ΣCj", p28), |
| 1292 | ("P|rj;pj=p|ΣwjUj", p29), |
| 1293 | ("P|pj=1;chains;rj|Lmax", p30), |
| 1294 | ("R||ΣCj", p31), |
| 1295 | ("P2||ΣwjCj", p32), |
| 1296 | ("Q|Mj|ΣCj", p33), |
| 1297 | ("P2|Mj|ΣwjCj", p34), |
| 1298 | ("P;S1|sj=s;pj=p;rj|Cmax", p35), |
| 1299 | ("P;S1|sj=s;pj=p;rj|ΣCj", p36), |
| 1300 | ("P;S1|sj=s;pj=1;rj|ΣwjCj", p37), |
| 1301 | ("P;S1|sj=s;pj=1;rj|ΣwjUj", p38), |
| 1302 | ("P;S1|sj=s;pj=1;rj|ΣTj", p39), |
| 1303 | ("P2;S1|pj=p|Cmax", p40), |
| 1304 | ("P2;S1|pj=p|ΣCj", p41), |
| 1305 | ("P2;S1|pj=1;rj|Lmax", p42), |
| 1306 | ("P2;S1|pj=1;rj|ΣCj", p43), |
| 1307 | ("P;S1|sj=1|ΣCj", p44), |
| 1308 | ("P3|fixj|Cmax", p45), |
| 1309 | ("P|pj=p;sizej|Cmax", p46), |
| 1310 | ("P|pj=p;outtree;rj|Cmax", p47), |
| 1311 | ("P|pj=p;intree|Lmax", p48), |
| 1312 | ("P|pj=1;intree;rj|Cmax", p49), |
| 1313 | ("P|pj=1;outtree|Lmax", p50), |
| 1314 | ("P|Mj;intree;pj=1;rj|Cmax", p51), |
| 1315 | ("P|Mj;outtree;pj=1|Lmax", p52), |
| 1316 | ("P|pj=1;outtree;rj|ΣCj", p53), |
| 1317 | ("Q2|pj=1;chains|Cmax", p54), |
| 1318 | ("P|Mj;pj=1;rj|ΣwjUj", p55), |
| 1319 | ("Q|Mj;pj=1|ΣwjUj", p56), |
| 1320 | ("P|Mj;pj=1;rj|ΣwjTj", p57), |
| 1321 | ("Q|Mj;pj=1|ΣwjTj", p58), |
| 1322 | ("P2|Mj;chains;pj=1|Cmax", p59), |
| 1323 | ("1|outtree;l;pj=1;rj|Cmax", p60), |
| 1324 | ("1|tree;l;pj=1|Cmax", p61), |
| 1325 | ("1|intree;l;pj=1|Lmax", p62), |
| 1326 | ("1|prec;l=1;pj=1;rj|Lmax", p63), |
| 1327 | ("P|fixj;rj;pj=1|Cmax", p64), |
| 1328 | ("P|fixj;rj;pj=1|ΣCj", p65), |
| 1329 | ("P|fixj;pj=1|ΣwjCj", p66), |
| 1330 | ("P|fixj;pj=1|ΣwjUj", p67), |
| 1331 | ("P|fixj;pj=1|ΣTj", p68), |
| 1332 | ("1|outtree;l;pj=1;rj|ΣCj", p69), |
| 1333 | ("1|prec;l=1;pj=1|ΣCj", p70), |
| 1334 | ("1|intree;l;pj=1;rj|Cmax", p71), |
| 1335 | ("1|outtree;l;pj=1|Lmax", p72), |
| 1336 | ("1|chains;l|ΣCj", p73), |
| 1337 | ("1|chains;l;pj=p|ΣCj", p74), |
| 1338 | ("P2|rj;pj=1;sizej|ΣCj", p75), |
| 1339 | ("P|pj=p;sizej|ΣwjUj", p76), |
| 1340 | ("P|pj=p;sizej|ΣTj", p77), |
| 1341 | ("P2|chains;rj;pj=1;sizej|Cmax", p78), |
| 1342 | ("P2|chains;pj=1;sizej|Lmax", p79), |
| 1343 | ("P2|prec;pj=1;sizej|ΣCj", p80), |
| 1344 | ("P|chains;pj=1;sizej|Cmax", p81), |
| 1345 | ("P3|chains;pj=1;sizej|Cmax", p82), |
| 1346 | ("P2|fixj;chains;pj=1|Cmax", p83), |
| 1347 | ("P2|fixj;chains;pj=1|ΣCj", p84), |
| 1348 | ("P2|pj=1;prec;rj|ΣCj", p85), |
| 1349 | ("1|prec;l=1;pj=1;rj|ΣCj", p86), |
| 1350 | ("P2|pj=p;prec|Cmax", p87), |
| 1351 | ("P2|pj=p;prec|ΣCj", p88), |
| 1352 | ("P2|fixj|ΣCj", p89), |
| 1353 | ("P|pj=p;tree|Cmax", p90), |
| 1354 | ("P|pj=p;sizej|ΣwjCj", p91), |
| 1355 | ("P|pj=1;sizej|ΣCj", p92), |
| 1356 | ("P2|sizej|Cmax", p93), |
| 1357 | ("P3|sizej|Cmax", p94), |
| 1358 | ("P5|sizej|Cmax", p95), |
| 1359 | ("P|sizej|Cmax", p96), |
| 1360 | ("1||ΣTj", p97), |
| 1361 | ("Q|pj=1;rj|ΣCj", p98), |
| 1362 | ("Q|pj=p;rj|ΣCj", p99), |
| 1363 | ("P2|chains|Cmax", p100), |
| 1364 | ("P2|chains|ΣCj", p101), |
| 1365 | ("P2|Mj;chains|Cmax", p102), |
| 1366 | ("P2|Mj;chains|ΣCj", p103), |
| 1367 | ("1|prec;l=1|Cmax", p104), |
| 1368 | ("P2|pj=p;prec|Lmax", p105), |
| 1369 | ("P2|pj=1;prec;rj|Lmax", p106), |
| 1370 | ("P|Mj|Cmax", p107), |
| 1371 | ("P|pj=p;outtree|ΣCj", p108), |
| 1372 | ("P2;S1|sj=1|ΣCj", p109), |
| 1373 | ("P;S1|pj=1|ΣwjCj", p110), |
| 1374 | ("P;S1|pj=1|ΣUj", p111), |
| 1375 | ("P2;S1|sj=1|Cmax", p112), |
| 1376 | ("P2;S1|pj=1|ΣwjUj", p113), |
| 1377 | ("P2;S1|pj=1|ΣTj", p114), |
| 1378 | ("P2;S1|sj=s|Cmax", p115), |
| 1379 | ("P2;S1|sj=1|Lmax", p116), |
| 1380 | ("P2;S1|sj=s|ΣCj", p117), |
| 1381 | ("P2;S1|pj=1|ΣwjTj", p118), |
| 1382 | ("P2|fixj|Cmax", p119), |
| 1383 | ("P|fixj;pj=1|Cmax", p120), |
| 1384 | ("P2|fixj;rj|Cmax", p121), |
| 1385 | ("P2|fixj|Lmax", p122), |
| 1386 | ("P|fixj;pj=1|ΣCj", p123), |
| 1387 | ("1||ΣwjUj", p124), |
| 1388 | ("P|fixj|Cmax", p125), |
| 1389 | ("Q|pj=1;chains|Cmax", p126), |
| 1390 | ("Q|pj=p;chains|Cmax", p127), |
| 1391 | ("Q|Mj;chains;pj=1|Cmax", p128), |
| 1392 | ("P|pj=1;intree;rj|ΣCj", p129), |
| 1393 | ("P|Mj|ΣwjCj", p130), |
| 1394 | ("1|prec;rj|Cmax", p131), |
| 1395 | ("1|prec|Lmax", p132), |
| 1396 | ("1||ΣwjTj", p133), |
| 1397 | ("1|sp-graph|ΣwjCj", p134), |
| 1398 | ("1|prec|ΣCj", p135), |
| 1399 | ("1|bounded height;pj=1|ΣwjCj", p136), |
| 1400 | ("P2|prec;pj=p;sizej|Cmax", p137), |
| 1401 | ("P|pj=1;sizej|Cmax", p138), |
| 1402 | ("P2|rj;pj=p;sizej|Cmax", p139), |
| 1403 | ("P2|pj=p;sizej|ΣwjCj", p140), |
| 1404 | ("P2|rj;sizej|Cmax", p141), |
| 1405 | ("P2|sizej|Lmax", p142), |
| 1406 | ("P2|sizej|ΣCj", p143), |
| 1407 | ("P2|sizej|ΣwjCj", p144), |
| 1408 | ("Q|rj|Cmax", p145), |
| 1409 | ("Q||ΣwjCj", p146), |
| 1410 | ("Q||ΣwjUj", p147), |
| 1411 | ("1|prec;pj=1|ΣwjCj", p148), |
| 1412 | ("P|pj=1;bounded height|ΣCj", p149), |
| 1413 | ("P|pj=1;bounded height|Cmax", p150), |
| 1414 | ("P|Mj;prec;pj=1|ΣCj", p151), |
| 1415 | ("1|chains;pj=1;rj|ΣwjCj", p152), |
| 1416 | ("1|chains;pj=1|ΣUj", p153), |
| 1417 | ("P2|pj=1;intree|ΣwjCj", p154), |
| 1418 | ("P2|pj=1;outtree|ΣwjCj", p155), |
| 1419 | ("P2|Mj;intree;pj=1|ΣwjCj", p156), |
| 1420 | ("P2|Mj;outtree;pj=1|ΣwjCj", p157), |
| 1421 | ("1|rj|Lmax", p158), |
| 1422 | ("1|rj|ΣCj", p159), |
| 1423 | ("P2||Cmax", p160), |
| 1424 | ("P2|Mj|Cmax", p161), |
| 1425 | ("1|prec;l;pj=1|Cmax", p162), |
| 1426 | ("1|chains;pj=1|ΣTj", p163), |
| 1427 | ("1||ΣUj", p164), |
| 1428 | ("P|pj=1;intree|Lmax", p165), |
| 1429 | ("1|chains;l;pj=p|Cmax", p166), |
| 1430 | ("1|chains;l=1;pj=p|ΣCj", p167), |
| 1431 | ("1|prec;pj=p;rj|Lmax", p168), |
| 1432 | ("1|prec;pj=p;rj|ΣCj", p169), |
| 1433 | ("P|pj=p;rj|Lmax", p170), |
| 1434 | ("P|pj=p;rj|ΣCj", p171), |
| 1435 | ("P2|chains;pj=1|ΣwjCj", p172), |
| 1436 | ("P2|Mj;chains;pj=1|ΣwjCj", p173), |
| 1437 | ("1|chains;l=1;pj=1|ΣwjCj", p174), |
| 1438 | ("P|Mj;prec;pj=1|Cmax", p175), |
| 1439 | ("1|chains;l|Cmax", p176), |
| 1440 | ("1|chains;lij;pj=1|Cmax", p177), |
| 1441 | ("P2|outtree;pj=1;sizej|ΣCj", p178), |
| 1442 | ("P2|intree;pj=1;sizej|ΣCj", p179), |
| 1443 | ("1|pj=1;rj|ΣwjTj", p180), |
| 1444 | ("1|pj=p|ΣwjTj", p181), |
| 1445 | ("P|pj=p|ΣwjUj", p182), |
| 1446 | ("P|pj=p|ΣwjTj", p183), |
| 1447 | ("P;S1|sj=s;pj=p|ΣwjUj", p184), |
| 1448 | ("P;S1|sj=1;pj=1;rj|ΣwjTj", p185), |
| 1449 | ("P;S1|sj=s;pj=p|ΣwjTj", p186), |
| 1450 | ("Q|pj=p;rj|Cmax", p187), |
| 1451 | ("Q|pj=p|ΣwjUj", p188), |
| 1452 | ("Q|pj=p|ΣwjTj", p189), |
| 1453 | ("P|pj=1;rj|ΣwjUj", p190), |
| 1454 | ("P|pj=1;rj|ΣwjTj", p191), |
| 1455 | ("P2|rj|ΣCj", p192), |
| 1456 | ("P2|pj=1;chains;rj|ΣwjCj", p193), |
| 1457 | ("P2|pj=1;chains|ΣUj", p194), |
| 1458 | ("P2|pj=1;chains|ΣTj", p195), |
| 1459 | ("P2|Mj;rj|ΣCj", p196), |
| 1460 | ("P2|Mj;chains;pj=1;rj|ΣwjCj", p197), |
| 1461 | ("P2|Mj;chains;pj=1|ΣUj", p198), |
| 1462 | ("P2|Mj;chains;pj=1|ΣTj", p199), |
| 1463 | ("P|Mj|ΣwjZj", p200), |
| 1464 | ("P|Mj|ΣZj", p201), |
| 1465 | ("P||ΣwjZj", p202), |
| 1466 | ("P|Mj;pj=p|ΣZj", p203), |
| 1467 | ("P|Mj;pj=p|ΣwjZj", p204), |
| 1468 | ("1||ΣZj", p205), |
| 1469 | ("P||ΣZj", p206), |
| 1470 | ("1||ΣwjZj", p207), |
| 1471 | ("R||ΣwjZj", p208), |
| 1472 | ("1|2-dim partial order|ΣwjCj", p209), |
| 1473 | ("1|interval order|ΣwjCj", p210), |
| 1474 | ("P|opposing forest;pj=p|Cmax", p211), |
| 1475 | ("P|opposing forest;pj=1|Cmax", p212), |
| 1476 | ("P|bounded height;pj=p|Cmax", p213), |
| 1477 | ("P|level order;pj=p|Cmax", p214), |
| 1478 | ("P|interval order;pj=p|Cmax", p215), |
| 1479 | ("P|interval order;pj=p|ΣCj", p216), |
| 1480 | ("P|quasi-interval order;pj=p|Cmax", p217), |
| 1481 | ("P|over-interval order;pj=p|Cmax", p218), |
| 1482 | ("P|DC-graph;pj=p|Cmax", p219), |
| 1483 | ("P|prec;l=1;pj=1|Cmax", p220), |
| 1484 | ("R|rj|ΣCj", p221), |
| 1485 | ("R||ΣwjCj", p222), |
| 1486 | ("P|prec;pj=1|ΣCj", p223), |
| 1487 | ("P|prec;l=1;pj=1|ΣCj", p224), |
| 1488 | ("P|rj|ΣwjCj", p225), |
| 1489 | ("1|online-rj|ΣwjCj", p226), |
| 1490 | ("1|dj=d|ΣwjTj", p227), |
| 1491 | ("1|pj=1;prec;lij≤0|Lmax", p228), |
| 1492 | ("P|rj;pj=1;sizej∈1,m|Lmax", p229), |
| 1493 | ("1|rj;pj=p|ΣUj", p230), |
| 1494 | ("P2|rj;pj=1;sizej|Lmax", p231), |
| 1495 | ("P2|rj|Lmax", p232), |
| 1496 | ("P|Mj;prec;rj|Lmax", p233), |
| 1497 | ("P|Mj;prec;rj;l|Cmax", p234), |
| 1498 | ("P|Mj;prec;rj;l|Lmax", p235), |
| 1499 | ("P|Mj;prec;rj;d̄j=d̄|Cmax", p236), |
| 1500 | ("1|rj|ΣwjUj", p237), |
| 1501 | ("P|rj;pj=p|ΣUj", p238), |
| 1502 | ("P|rj;prec|ΣwjCj", p239), |
| 1503 | ("P|prec|ΣwjCj", p240), |
| 1504 | ("P|prec;pj=1|ΣwjCj", p241), |
| 1505 | ("Q|prec|ΣwjCj", p242), |
| 1506 | ("1|pj=p;online-rj|ΣUj", p243), |
| 1507 | ("P∞|pj=1;prec;c=1|Cmax", p244), |
| 1508 | ("P|pj=1;prec;c=1|Cmax", p245), |
| 1509 | ("P∞|pj=1;prec;c|Cmax", p246), |
| 1510 | ("P|pj=1;prec;c|Cmax", p247), |
| 1511 | ("P|prec;c|Cmax", p248), |
| 1512 | ("P∞|prec;c|Cmax", p249), |
| 1513 | ("Q|prec;c|ΣwjCj", p250), |
| 1514 | ("Q|prec;c;pj=1|ΣwjCj", p251), |
| 1515 | ("1|rj|ΣUj", p252), |
| 1516 | ("1|forbidden-times|Cmax", p253), |
| 1517 | ("P|HM|Cmax", p254), |
| 1518 | ("P3|prec;pj=1|Cmax", p255)] |
| 1519 | |
| 1520 | /-- The relations that hold field by field: general problem, special problem. -/ |
| 1521 | def specialCases : List (Spec F × Spec F) := [ |
| 1522 | (p1, p0), (p14, p0), (p96, p0), (p107, p0), (p248, p0), (p145, p1), (p233, p1), (p234, p1), |
| 1523 | (p236, p1), (p130, p2), (p146, p2), (p225, p2), (p240, p2), (p4, p3), (p147, p4), (p7, p6), |
| 1524 | (p8, p7), (p11, p10), (p13, p12), (p10, p13), (p5, p14), (p145, p14), (p16, p15), (p240, p15), |
| 1525 | (p239, p16), (p175, p17), (p245, p17), (p16, p19), (p225, p19), (p19, p20), (p22, p20), (p23, p21), |
| 1526 | (p225, p22), (p29, p26), (p237, p26), (p28, p27), (p240, p28), (p233, p30), (p221, p31), (p222, p31), |
| 1527 | (p2, p32), (p34, p32), (p144, p32), (p130, p34), (p125, p45), (p24, p46), (p96, p46), (p233, p47), |
| 1528 | (p234, p47), (p236, p47), (p233, p48), (p51, p49), (p52, p50), (p233, p51), (p234, p51), (p236, p51), |
| 1529 | (p233, p52), (p239, p53), (p126, p54), (p102, p59), (p162, p61), (p86, p70), (p224, p70), (p73, p74), |
| 1530 | (p81, p82), (p105, p87), (p137, p87), (p211, p90), (p25, p92), (p77, p92), (p91, p92), (p94, p93), |
| 1531 | (p141, p93), (p142, p93), (p95, p94), (p96, p95), (p133, p97), (p99, p98), (p221, p99), (p102, p100), |
| 1532 | (p103, p101), (p233, p107), (p234, p107), (p236, p107), (p28, p108), (p44, p109), (p117, p109), (p115, p112), |
| 1533 | (p116, p112), (p118, p114), (p45, p119), (p121, p119), (p122, p119), (p64, p120), (p125, p120), (p65, p123), |
| 1534 | (p66, p123), (p68, p123), (p4, p124), (p237, p124), (p127, p126), (p128, p126), (p239, p129), (p209, p134), |
| 1535 | (p15, p135), (p148, p136), (p46, p138), (p81, p138), (p24, p139), (p141, p139), (p91, p140), (p144, p140), |
| 1536 | (p144, p143), (p222, p146), (p242, p146), (p15, p148), (p241, p148), (p223, p149), (p17, p150), (p213, p150), |
| 1537 | (p16, p152), (p193, p152), (p194, p153), (p156, p154), (p157, p155), (p232, p158), (p19, p159), (p192, p159), |
| 1538 | (p0, p160), (p93, p160), (p100, p160), (p161, p160), (p232, p160), (p102, p161), (p107, p161), (p195, p163), |
| 1539 | (p3, p164), (p124, p164), (p252, p164), (p48, p165), (p176, p166), (p74, p167), (p16, p169), (p233, p170), |
| 1540 | (p22, p171), (p23, p171), (p25, p171), (p99, p171), (p154, p172), (p155, p172), (p173, p172), (p193, p172), |
| 1541 | (p156, p173), (p157, p173), (p197, p173), (p233, p175), (p234, p175), (p236, p175), (p80, p178), (p80, p179), |
| 1542 | (p191, p180), (p133, p181), (p183, p181), (p4, p182), (p29, p182), (p76, p182), (p188, p182), (p189, p183), |
| 1543 | (p145, p187), (p147, p188), (p29, p190), (p55, p190), (p57, p191), (p196, p192), (p197, p193), (p198, p194), |
| 1544 | (p199, p195), (p200, p201), (p200, p202), (p201, p203), (p204, p203), (p200, p204), (p206, p205), (p207, p205), |
| 1545 | (p201, p206), (p202, p206), (p202, p207), (p15, p209), (p15, p210), (p233, p211), (p234, p211), (p236, p211), |
| 1546 | (p248, p211), (p17, p212), (p211, p212), (p233, p213), (p234, p213), (p236, p213), (p248, p213), (p233, p214), |
| 1547 | (p234, p214), (p236, p214), (p248, p214), (p217, p215), (p240, p216), (p218, p217), (p233, p218), (p234, p218), |
| 1548 | (p236, p218), (p248, p218), (p233, p219), (p234, p219), (p236, p219), (p248, p219), (p234, p220), (p9, p221), |
| 1549 | (p9, p222), (p151, p223), (p241, p223), (p9, p225), (p239, p225), (p133, p227), (p26, p230), (p238, p230), |
| 1550 | (p252, p230), (p235, p233), (p235, p234), (p29, p238), (p239, p240), (p242, p240), (p240, p241), (p251, p241), |
| 1551 | (p250, p242), (p246, p244), (p247, p245), (p249, p246), (p248, p247), (p248, p249), (p250, p251), (p237, p252), |
| 1552 | (p17, p255), (p254, p0)] |
| 1553 | |
| 1554 | /-- The relations that need a threshold step: general problem, special problem. -/ |
| 1555 | def thresholdReductions : List (Spec F × Spec F) := [ |
| 1556 | (p3, p0), (p147, p14), (p76, p46), (p77, p46), (p198, p59), (p199, p59), (p67, p120), (p68, p120), |
| 1557 | (p23, p170)] |
| 1558 | |
| 1559 | axiom specialCases_hold : ∀ e ∈ specialCases, |
| 1560 | SpecialCase (problem F e.2) (problem F e.1) |
| 1561 | |
| 1562 | axiom thresholdReductions_hold : ∀ e ∈ thresholdReductions, |
| 1563 | Reducible (problem F e.2) (problem F e.1) |
| 1564 | |
| 1565 | /-- The relations through flow time: general problem, special problem. -/ |
| 1566 | def flowReductions : List (Spec F × Spec F) := [ |
| 1567 | ] |
| 1568 | |
| 1569 | axiom flowReductions_hold : ∀ e ∈ flowReductions, |
| 1570 | Reducible (problem F e.2) (problem F e.1) |
| 1571 | |
| 1572 | end Lax434175.ZooParallel |
| 1573 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments