Results of The Scheduling Zoo, preemptive shop problems
Lax434175.ZooPreemptiveShopsResults · concepts/Lax434175/ZooPreemptiveShopsResults.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
The 29 results of The Scheduling Zoo on its preemptive shop problems that are stated here, each as a proposition about a reading of the problem (; for a family, at the problem's specification): its words of instances and schedules and what an online scheduler sees. Each names its source; where the proposition is weaker than the wording, a note says what is left out.
Concept map
Lean source view on GitHub
| 1 | import Lax434175.ZooPreemptiveShops |
| 2 | import Lax434175.Results |
| 3 | import Lax434175.ResultParameters |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Results of The Scheduling Zoo, preemptive shop problems |
| 8 | type: definition |
| 9 | --- |
| 10 | The 29 results of The Scheduling Zoo on its preemptive shop problems that are |
| 11 | stated here, each as a proposition about a reading of the problem |
| 12 | (`Results.PReading`; for a family, `Results.Reading` at the problem's |
| 13 | specification): its words of instances and schedules and what an online |
| 14 | scheduler sees. Each names its source; where the proposition is weaker than |
| 15 | the wording, a note says what is left out. |
| 16 | -/ |
| 17 | |
| 18 | namespace Lax434175.ZooPreemptiveShopsResults |
| 19 | open Lax434175 Lax434175.Problems Lax434175.Results Lax434175.ResultParameters Lax434175.ZooPreemptiveShops |
| 20 | |
| 21 | /-- `J|n=k;pmtn|Cmax`, parameter m: is in Ppseudo. |
| 22 | |
| 23 | Brucker, P. and Kravchenko, S.A. and Sotskov, Y.N. (1999). Preemptive job-shop scheduling problems with a fixed number of jobs. https://doi.org/10.1007/pl00020906 |
| 24 | |
| 25 | Note: the problem has k jobs for every fixed k, so the result is read for every fixed number of jobs and of m. |
| 26 | -/ |
| 27 | def p0_r0 (R : Reading F) : Prop := |
| 28 | PseudoPolyFixed (R.at p0) (tplus (lift (Ops.n p0)) (lift (Ops.m p0))) |
| 29 | |
| 30 | /-- `J|n=k;pmtn|ΣCj`, parameter m: is in Ppseudo. |
| 31 | |
| 32 | Brucker, P. and Kravchenko, S.A. and Sotskov, Y.N. (1999). Preemptive job-shop scheduling problems with a fixed number of jobs. https://doi.org/10.1007/pl00020906 |
| 33 | |
| 34 | Note: the problem has k jobs for every fixed k, so the result is read for every fixed number of jobs and of m. |
| 35 | -/ |
| 36 | def p1_r0 (R : Reading F) : Prop := |
| 37 | PseudoPolyFixed (R.at p1) (tplus (lift (Ops.n p1)) (lift (Ops.m p1))) |
| 38 | |
| 39 | /-- `J2|n=3;pmtn|Cmax`: is NP-hard. |
| 40 | |
| 41 | Brucker, P. and Kravchenko, S.A. and Sotskov, Y.N. (1999). Preemptive job-shop scheduling problems with a fixed number of jobs. https://doi.org/10.1007/pl00020906 |
| 42 | -/ |
| 43 | def p2_r0 (R : Reading F) : Prop := |
| 44 | NPHard (R.at p2) |
| 45 | |
| 46 | /-- `J2|n=3;pmtn|ΣCj`: is NP-hard. |
| 47 | |
| 48 | Brucker, P. and Kravchenko, S.A. and Sotskov, Y.N. (1999). Preemptive job-shop scheduling problems with a fixed number of jobs. https://doi.org/10.1007/pl00020906 |
| 49 | -/ |
| 50 | def p3_r0 (R : Reading F) : Prop := |
| 51 | NPHard (R.at p3) |
| 52 | |
| 53 | /-- `O|pmtn;rj|Lmax`: is in P. |
| 54 | |
| 55 | Cho, Y. and Sahni, S. (1981). Preemptive scheduling of independent jobs with release and due times on open, flow and job shops. https://doi.org/10.1287/opre.29.3.511 |
| 56 | -/ |
| 57 | def p4_r0 (R : Reading F) : Prop := |
| 58 | InP (R.at p4) |
| 59 | |
| 60 | /-- `F2|pmtn|Cmax`: is in P. |
| 61 | |
| 62 | Cho, Y. and Sahni, S. (1981). Preemptive scheduling of independent jobs with release and due times on open, flow and job shops. https://doi.org/10.1287/opre.29.3.511 |
| 63 | -/ |
| 64 | def p5_r0 (R : Reading F) : Prop := |
| 65 | InP (R.at p5) |
| 66 | |
| 67 | /-- `F2|pmtn|Cmax`: is in P. |
| 68 | |
| 69 | Gonzalez, T. and Sahni, S. (1978). Flowshop and jobshop schedules: complexity and approximation. https://doi.org/10.1287/opre.26.1.36 |
| 70 | -/ |
| 71 | def p5_r1 (R : Reading F) : Prop := |
| 72 | InP (R.at p5) |
| 73 | |
| 74 | /-- `F2|rj;pmtn|Cmax`: is strongly NP-hard. |
| 75 | |
| 76 | Cho, Y. and Sahni, S. (1981). Preemptive scheduling of independent jobs with release and due times on open, flow and job shops. https://doi.org/10.1287/opre.29.3.511 |
| 77 | -/ |
| 78 | def p6_r0 (R : Reading F) : Prop := |
| 79 | StronglyNPHard (R.at p6) |
| 80 | |
| 81 | /-- `F2|rj;pmtn|Cmax`: is strongly NP-hard. |
| 82 | |
| 83 | Gonzalez, T. and Sahni, S. (1978). Flowshop and jobshop schedules: complexity and approximation. https://doi.org/10.1287/opre.26.1.36 |
| 84 | -/ |
| 85 | def p6_r1 (R : Reading F) : Prop := |
| 86 | StronglyNPHard (R.at p6) |
| 87 | |
| 88 | /-- `F3|pmtn|Cmax`: is strongly NP-hard. |
| 89 | |
| 90 | Cho, Y. and Sahni, S. (1981). Preemptive scheduling of independent jobs with release and due times on open, flow and job shops. https://doi.org/10.1287/opre.29.3.511 |
| 91 | -/ |
| 92 | def p7_r0 (R : Reading F) : Prop := |
| 93 | StronglyNPHard (R.at p7) |
| 94 | |
| 95 | /-- `F3|pmtn|Cmax`: is strongly NP-hard. |
| 96 | |
| 97 | Gonzalez, T. and Sahni, S. (1978). Flowshop and jobshop schedules: complexity and approximation. https://doi.org/10.1287/opre.26.1.36 |
| 98 | -/ |
| 99 | def p7_r1 (R : Reading F) : Prop := |
| 100 | StronglyNPHard (R.at p7) |
| 101 | |
| 102 | /-- `F2|pmtn|Lmax`: is strongly NP-hard. |
| 103 | |
| 104 | Cho, Y. and Sahni, S. (1981). Preemptive scheduling of independent jobs with release and due times on open, flow and job shops. https://doi.org/10.1287/opre.29.3.511 |
| 105 | -/ |
| 106 | def p8_r0 (R : Reading F) : Prop := |
| 107 | StronglyNPHard (R.at p8) |
| 108 | |
| 109 | /-- `F2|pmtn|Lmax`: is strongly NP-hard. |
| 110 | |
| 111 | Gonzalez, T. and Sahni, S. (1978). Flowshop and jobshop schedules: complexity and approximation. https://doi.org/10.1287/opre.26.1.36 |
| 112 | -/ |
| 113 | def p8_r1 (R : Reading F) : Prop := |
| 114 | StronglyNPHard (R.at p8) |
| 115 | |
| 116 | /-- `O2|pmtn|ΣCj`: is NP-hard. |
| 117 | |
| 118 | Du, J. and Leung, J.Y.-T. (1993). Minimizing mean flow time in two-machine open shops and flow shops. https://doi.org/10.1006/jagm.1993.1002 |
| 119 | -/ |
| 120 | def p9_r0 (R : Reading F) : Prop := |
| 121 | NPHard (R.at p9) |
| 122 | |
| 123 | /-- `F2|pmtn|ΣCj`: is strongly NP-hard. |
| 124 | |
| 125 | Du, J. and Leung, J.Y.-T. (1993). Minimizing mean flow time in two-machine open shops and flow shops. https://doi.org/10.1006/jagm.1993.1002 |
| 126 | -/ |
| 127 | def p10_r0 (R : Reading F) : Prop := |
| 128 | StronglyNPHard (R.at p10) |
| 129 | |
| 130 | /-- `O2|chains;pmtn|Cmax`: is strongly NP-hard. |
| 131 | |
| 132 | Lenstra, J.K. (unknown year). unknown title. None |
| 133 | -/ |
| 134 | def p11_r0 (R : Reading F) : Prop := |
| 135 | StronglyNPHard (R.at p11) |
| 136 | |
| 137 | /-- `O2|chains;pmtn|ΣCj`: is strongly NP-hard. |
| 138 | |
| 139 | Lenstra, J.K. (unknown year). unknown title. None |
| 140 | -/ |
| 141 | def p12_r0 (R : Reading F) : Prop := |
| 142 | StronglyNPHard (R.at p12) |
| 143 | |
| 144 | /-- `O2|pmtn|ΣwjCj`: is strongly NP-hard. |
| 145 | |
| 146 | Lenstra, J.K. (unknown year). unknown title. None |
| 147 | -/ |
| 148 | def p13_r0 (R : Reading F) : Prop := |
| 149 | StronglyNPHard (R.at p13) |
| 150 | |
| 151 | /-- `F2|chains;pmtn|Cmax`: is strongly NP-hard. |
| 152 | |
| 153 | Lenstra, J.K. (unknown year). unknown title. None |
| 154 | -/ |
| 155 | def p14_r0 (R : Reading F) : Prop := |
| 156 | StronglyNPHard (R.at p14) |
| 157 | |
| 158 | /-- `J2|pmtn|ΣCj`: is strongly NP-hard. |
| 159 | |
| 160 | Lenstra, J.K. (unknown year). unknown title. None |
| 161 | -/ |
| 162 | def p15_r0 (R : Reading F) : Prop := |
| 163 | StronglyNPHard (R.at p15) |
| 164 | |
| 165 | /-- `O3|pmtn|ΣCj`: is strongly NP-hard. |
| 166 | |
| 167 | Liu, C.Y. and Bulfin, R.L. (1985). On the complexity of preemptive open-shop scheduling problems. https://doi.org/10.1016/0167-6377(85)90035-5 |
| 168 | -/ |
| 169 | def p16_r0 (R : Reading F) : Prop := |
| 170 | StronglyNPHard (R.at p16) |
| 171 | |
| 172 | /-- `O2|pmtn|ΣUj`: is NP-hard. |
| 173 | |
| 174 | Lawler, E.L. and Lenstra, J.K. and Rinnooy Kan, A.H.G. (1981). Minimizing maximum lateness in a two-machine open shop. https://doi.org/10.1287/moor.6.1.153 |
| 175 | -/ |
| 176 | def p17_r0 (R : Reading F) : Prop := |
| 177 | NPHard (R.at p17) |
| 178 | |
| 179 | /-- `O2|pmtn|ΣUj`: is NP-hard. |
| 180 | |
| 181 | Lawler, E.L. and Lenstra, J.K. and Rinnooy Kan, A.H.G. (1982). Erratum: ''Minimizing maximum lateness in a two-machine open shop''\ [Math. Oper. Res. \bf 6 (1981), no. 1, 153-158]. https://doi.org/10.1287/moor.6.1.153 |
| 182 | -/ |
| 183 | def p17_r1 (R : Reading F) : Prop := |
| 184 | NPHard (R.at p17) |
| 185 | |
| 186 | /-- `J2|pmtn|Cmax`: is strongly NP-hard. |
| 187 | |
| 188 | Lenstra, J.K. and Rinnooy Kan, A.H.G. (1979). Computational complexity of discrete optimization problems. https://doi.org/10.1016/s0167-5060(08)70821-5 |
| 189 | -/ |
| 190 | def p18_r0 (R : Reading F) : Prop := |
| 191 | StronglyNPHard (R.at p18) |
| 192 | |
| 193 | /-- `J|prec;rj;n=k;pmtn|ΣwjUj`: is in Ppseudo. |
| 194 | |
| 195 | Middendorf, M. and Timkovsky, V.G. (1999). Transversal graphs for partially ordered sets: sequencing, merging and scheduling problems. https://doi.org/10.1023/a:1009827520712 |
| 196 | |
| 197 | Note: the problem has k jobs for every fixed k, so the result is read for every fixed number of jobs. |
| 198 | -/ |
| 199 | def p19_r0 (R : Reading F) : Prop := |
| 200 | PseudoPolyFixed (R.at p19) (lift (Ops.n p19)) |
| 201 | |
| 202 | /-- `J|prec;rj;n=k;pmtn|ΣwjTj`: is in Ppseudo. |
| 203 | |
| 204 | Middendorf, M. and Timkovsky, V.G. (1999). Transversal graphs for partially ordered sets: sequencing, merging and scheduling problems. https://doi.org/10.1023/a:1009827520712 |
| 205 | |
| 206 | Note: the problem has k jobs for every fixed k, so the result is read for every fixed number of jobs. |
| 207 | -/ |
| 208 | def p20_r0 (R : Reading F) : Prop := |
| 209 | PseudoPolyFixed (R.at p20) (lift (Ops.n p20)) |
| 210 | |
| 211 | /-- `J|prec;rj;n=2;pmtn|ΣwjUj`: is in P. |
| 212 | |
| 213 | Sotskov, Y.N. (1991). The complexity of shop-scheduling problems with two or three jobs. https://doi.org/10.1016/0377-2217(91)90066-5 |
| 214 | -/ |
| 215 | def p21_r0 (R : Reading F) : Prop := |
| 216 | InP (R.at p21) |
| 217 | |
| 218 | /-- `J|prec;rj;n=2;pmtn|ΣwjTj`: is in P. |
| 219 | |
| 220 | Sotskov, Y.N. (1991). The complexity of shop-scheduling problems with two or three jobs. https://doi.org/10.1016/0377-2217(91)90066-5 |
| 221 | -/ |
| 222 | def p22_r0 (R : Reading F) : Prop := |
| 223 | InP (R.at p22) |
| 224 | |
| 225 | /-- `O2|pmtn;rj|ΣCj`: is strongly NP-hard. |
| 226 | |
| 227 | Sriskandarajah, C. and Wagneur, E. (1994). On the complexity of preemptive openshop scheduling problems. https://doi.org/10.1016/0377-2217(94)90406-5 |
| 228 | -/ |
| 229 | def p23_r0 (R : Reading F) : Prop := |
| 230 | StronglyNPHard (R.at p23) |
| 231 | |
| 232 | end Lax434175.ZooPreemptiveShopsResults |
| 233 |
Used by
none
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments