Results of The Scheduling Zoo, serial batching problems
Lax434175.ZooSerialBatchingResults · concepts/Lax434175/ZooSerialBatchingResults.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
The 33 results of The Scheduling Zoo on its serial batching 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.ZooSerialBatching |
| 2 | import Lax434175.Results |
| 3 | import Lax434175.ResultParameters |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Results of The Scheduling Zoo, serial batching problems |
| 8 | type: definition |
| 9 | --- |
| 10 | The 33 results of The Scheduling Zoo on its serial batching 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.ZooSerialBatchingResults |
| 19 | open Lax434175 Lax434175.Problems Lax434175.Results Lax434175.ResultParameters Lax434175.ZooSerialBatching |
| 20 | |
| 21 | /-- `1|prec;pj=p;s-batch|ΣCj`: is in P. |
| 22 | |
| 23 | Albers, S. and Brucker, P. (1993). The complexity of one-machine batching problems. https://doi.org/10.1016/0166-218x(93)90085-3 |
| 24 | -/ |
| 25 | def p0_r0 (R : Reading F) : Prop := |
| 26 | InP (R.at p0) |
| 27 | |
| 28 | /-- `1|pj=p;s-batch|ΣwjCj`: is in P. |
| 29 | |
| 30 | Albers, S. and Brucker, P. (1993). The complexity of one-machine batching problems. https://doi.org/10.1016/0166-218x(93)90085-3 |
| 31 | -/ |
| 32 | def p1_r0 (R : Reading F) : Prop := |
| 33 | InP (R.at p1) |
| 34 | |
| 35 | /-- `1|chains;s-batch|ΣCj`: is NP-hard. |
| 36 | |
| 37 | Albers, S. and Brucker, P. (1993). The complexity of one-machine batching problems. https://doi.org/10.1016/0166-218x(93)90085-3 |
| 38 | -/ |
| 39 | def p2_r0 (R : Reading F) : Prop := |
| 40 | NPHard (R.at p2) |
| 41 | |
| 42 | /-- `1|chains;pj=1;s-batch|ΣwjCj`: is strongly NP-hard. |
| 43 | |
| 44 | Albers, S. and Brucker, P. (1993). The complexity of one-machine batching problems. https://doi.org/10.1016/0166-218x(93)90085-3 |
| 45 | -/ |
| 46 | def p3_r0 (R : Reading F) : Prop := |
| 47 | StronglyNPHard (R.at p3) |
| 48 | |
| 49 | /-- `1|s-batch|ΣwjCj`: is strongly NP-hard. |
| 50 | |
| 51 | Albers, S. and Brucker, P. (1993). The complexity of one-machine batching problems. https://doi.org/10.1016/0166-218x(93)90085-3 |
| 52 | -/ |
| 53 | def p4_r0 (R : Reading F) : Prop := |
| 54 | StronglyNPHard (R.at p4) |
| 55 | |
| 56 | /-- `1|pj=p;s-batch;rj|ΣwjCj`: is in P. |
| 57 | |
| 58 | Baptiste, P. (2000). Batching identical jobs. https://doi.org/10.1007/s001860000088 |
| 59 | -/ |
| 60 | def p5_r0 (R : Reading F) : Prop := |
| 61 | InP (R.at p5) |
| 62 | |
| 63 | /-- `1|pj=p;s-batch;rj|ΣwjUj`: is in P. |
| 64 | |
| 65 | Baptiste, P. (2000). Batching identical jobs. https://doi.org/10.1007/s001860000088 |
| 66 | -/ |
| 67 | def p6_r0 (R : Reading F) : Prop := |
| 68 | InP (R.at p6) |
| 69 | |
| 70 | /-- `1|pj=p;s-batch;rj|ΣTj`: is in P. |
| 71 | |
| 72 | Baptiste, P. (2000). Batching identical jobs. https://doi.org/10.1007/s001860000088 |
| 73 | -/ |
| 74 | def p7_r0 (R : Reading F) : Prop := |
| 75 | InP (R.at p7) |
| 76 | |
| 77 | /-- `1|s-batch|ΣTj`: is in Ppseudo. |
| 78 | |
| 79 | Baptiste, P. and Jouglet, A. (2001). On minimizing total tardiness in a serial batching problem. https://doi.org/10.1051/ro:2001105 |
| 80 | -/ |
| 81 | def p8_r0 (R : Reading F) : Prop := |
| 82 | PseudoPoly (R.at p8) |
| 83 | |
| 84 | /-- `1|s-batch|ΣTj`: is NP-hard. |
| 85 | |
| 86 | Du, J. and Leung, J.Y.-T. (1990). Minimizing total tardiness on one machine is NP-hard. https://doi.org/10.1287/moor.15.3.483 |
| 87 | -/ |
| 88 | def p8_r1 (R : Reading F) : Prop := |
| 89 | NPHard (R.at p8) |
| 90 | |
| 91 | /-- `1|s-batch|ΣUj`: is in P. |
| 92 | |
| 93 | Brucker, P. and Kovalyov, M.Y. (1996). Single machine batch scheduling to minimize the weighted number of late jobs. https://doi.org/10.1007/bf01303431 |
| 94 | -/ |
| 95 | def p9_r0 (R : Reading F) : Prop := |
| 96 | InP (R.at p9) |
| 97 | |
| 98 | /-- `1|s-batch|ΣwjUj`: is in Ppseudo. |
| 99 | |
| 100 | Brucker, P. and Kovalyov, M.Y. (1996). Single machine batch scheduling to minimize the weighted number of late jobs. https://doi.org/10.1007/bf01303431 |
| 101 | -/ |
| 102 | def p10_r0 (R : Reading F) : Prop := |
| 103 | PseudoPoly (R.at p10) |
| 104 | |
| 105 | /-- `1|s-batch|ΣwjUj`: is NP-hard. |
| 106 | |
| 107 | Karp, R.M. (1972). Reducibility among combinatorial problems. https://doi.org/10.1007/978-1-4684-2001-2_9 |
| 108 | -/ |
| 109 | def p10_r1 (R : Reading F) : Prop := |
| 110 | NPHard (R.at p10) |
| 111 | |
| 112 | /-- `1|s-batch|ΣCj`: is in P. |
| 113 | |
| 114 | Coffman, Jr., E.G. and Yannakakis, M. and Magazine, M.J. and Santos, C. (1990). Batch sizing and job sequencing on a single machine. https://doi.org/10.1007/bf02248589 |
| 115 | -/ |
| 116 | def p11_r0 (R : Reading F) : Prop := |
| 117 | InP (R.at p11) |
| 118 | |
| 119 | /-- `1|pj=p;s-batch|ΣwjUj`: is in P. |
| 120 | |
| 121 | Hochbaum, D.S. and Landy, D. (1994). Scheduling with batching: minimizing the weighted number of tardy jobs. https://doi.org/10.1016/0167-6377(94)90063-9 |
| 122 | -/ |
| 123 | def p12_r0 (R : Reading F) : Prop := |
| 124 | InP (R.at p12) |
| 125 | |
| 126 | /-- `1|prec;s-batch|ΣCj`: is strongly NP-hard. |
| 127 | |
| 128 | Lawler, E.L. (1978). Sequencing jobs to minimize total weighted completion time subject to precedence constraints. https://doi.org/10.1016/s0167-5060(08)70323-6 |
| 129 | -/ |
| 130 | def p13_r0 (R : Reading F) : Prop := |
| 131 | StronglyNPHard (R.at p13) |
| 132 | |
| 133 | /-- `1|prec;s-batch|ΣCj`: is strongly NP-hard. |
| 134 | |
| 135 | Lenstra, J.K. and Rinnooy Kan, A.H.G. (1978). Complexity of scheduling under precedence constraints. https://doi.org/10.1287/opre.26.1.22 |
| 136 | -/ |
| 137 | def p13_r1 (R : Reading F) : Prop := |
| 138 | StronglyNPHard (R.at p13) |
| 139 | |
| 140 | /-- `1|chains;pj=1;s-batch|ΣUj`: is strongly NP-hard. |
| 141 | |
| 142 | Lenstra, J.K. and Rinnooy Kan, A.H.G. (1980). Complexity results for scheduling chains on a single machine. https://doi.org/10.1016/0377-2217(80)90111-3 |
| 143 | -/ |
| 144 | def p14_r0 (R : Reading F) : Prop := |
| 145 | StronglyNPHard (R.at p14) |
| 146 | |
| 147 | /-- `1|s-batch;rj|Lmax`: is strongly NP-hard. |
| 148 | |
| 149 | Lenstra, J.K. and Rinnooy Kan, A.H.G. and Brucker, P. (1977). Complexity of machine scheduling problems. https://doi.org/10.1016/s0167-5060(08)70743-x |
| 150 | -/ |
| 151 | def p15_r0 (R : Reading F) : Prop := |
| 152 | StronglyNPHard (R.at p15) |
| 153 | |
| 154 | /-- `1|s-batch;rj|ΣCj`: is strongly NP-hard. |
| 155 | |
| 156 | Lenstra, J.K. and Rinnooy Kan, A.H.G. and Brucker, P. (1977). Complexity of machine scheduling problems. https://doi.org/10.1016/s0167-5060(08)70743-x |
| 157 | -/ |
| 158 | def p16_r0 (R : Reading F) : Prop := |
| 159 | StronglyNPHard (R.at p16) |
| 160 | |
| 161 | /-- `1|chains;pj=1;s-batch|ΣTj`: is strongly NP-hard. |
| 162 | |
| 163 | Leung, J.Y.-T. and Young, G.H. (1990). Minimizing total tardiness on a single machine with precedence constraints. https://doi.org/10.1287/ijoc.2.4.346 |
| 164 | -/ |
| 165 | def p17_r0 (R : Reading F) : Prop := |
| 166 | StronglyNPHard (R.at p17) |
| 167 | |
| 168 | /-- `1|prec;s-batch|Lmax`: is in P. |
| 169 | |
| 170 | Ng, C.T. and Cheng, T.C.E. and Yuan, J.J. (2002). A note on the single machine serial batching scheduling problem to minimize maximum lateness with precedence constraints. https://doi.org/10.1016/s0167-6377(01)00105-5 |
| 171 | -/ |
| 172 | def p18_r0 (R : Reading F) : Prop := |
| 173 | InP (R.at p18) |
| 174 | |
| 175 | /-- `1|s-batch(∞);rj|ΣwjUj`: is NP-hard. |
| 176 | |
| 177 | Hermelin, Danny and Mnich, Matthias and Omlor, Simon (2024). Serial batching to minimize the weighted number of tardy jobs. https://link.springer.com/article/10.1007/s10951-024-00818-9 |
| 178 | -/ |
| 179 | def p19_r0 (R : Reading F) : Prop := |
| 180 | NPHard (R.at p19) |
| 181 | |
| 182 | /-- `1|s-batch(∞);rj|ΣwjUj`, parameter #d+#p: is W[1]-hard. |
| 183 | |
| 184 | Hermelin, Danny and Mnich, Matthias and Omlor, Simon (2024). Serial batching to minimize the weighted number of tardy jobs. https://link.springer.com/article/10.1007/s10951-024-00818-9 |
| 185 | -/ |
| 186 | def p19_r1 (R : Reading F) : Prop := |
| 187 | WHard (R.at p19) 1 (tplus (lift (Batch.numD p19)) (lift (Batch.numP p19))) |
| 188 | |
| 189 | /-- `1|s-batch(∞);rj|ΣwjUj`, parameter #p+#r: is W[1]-hard. |
| 190 | |
| 191 | Hermelin, Danny and Mnich, Matthias and Omlor, Simon (2024). Serial batching to minimize the weighted number of tardy jobs. https://link.springer.com/article/10.1007/s10951-024-00818-9 |
| 192 | -/ |
| 193 | def p19_r2 (R : Reading F) : Prop := |
| 194 | WHard (R.at p19) 1 (tplus (lift (Batch.numP p19)) (lift (Batch.numR p19))) |
| 195 | |
| 196 | /-- `1|s-batch(∞);rj|ΣwjUj`, parameter #d+#p+#w: is in P. |
| 197 | |
| 198 | Hermelin, Danny and Mnich, Matthias and Omlor, Simon (2024). Serial batching to minimize the weighted number of tardy jobs. https://link.springer.com/article/10.1007/s10951-024-00818-9 |
| 199 | |
| 200 | Note: in P for every fixed value. |
| 201 | -/ |
| 202 | def p19_r3 (R : Reading F) : Prop := |
| 203 | InPFixed (R.at p19) (tplus (tplus (lift (Batch.numD p19)) (lift (Batch.numP p19))) (lift (Batch.numW p19))) |
| 204 | |
| 205 | /-- `1|s-batch(∞);rj|ΣwjUj`, parameter #p+#r+#w: is in P. |
| 206 | |
| 207 | Hermelin, Danny and Mnich, Matthias and Omlor, Simon (2024). Serial batching to minimize the weighted number of tardy jobs. https://link.springer.com/article/10.1007/s10951-024-00818-9 |
| 208 | |
| 209 | Note: in P for every fixed value. |
| 210 | -/ |
| 211 | def p19_r4 (R : Reading F) : Prop := |
| 212 | InPFixed (R.at p19) (tplus (tplus (lift (Batch.numP p19)) (lift (Batch.numR p19))) (lift (Batch.numW p19))) |
| 213 | |
| 214 | /-- `1|s-batch(∞)|ΣwjUj`, parameter #p: is in P. |
| 215 | |
| 216 | Hermelin, Danny and Mnich, Matthias and Omlor, Simon (2024). Serial batching to minimize the weighted number of tardy jobs. https://link.springer.com/article/10.1007/s10951-024-00818-9 |
| 217 | |
| 218 | Note: in P for every fixed value. |
| 219 | -/ |
| 220 | def p20_r0 (R : Reading F) : Prop := |
| 221 | InPFixed (R.at p20) (lift (Batch.numP p20)) |
| 222 | |
| 223 | /-- `1|s-batch(∞)|ΣwjUj`, parameter #w: is in P. |
| 224 | |
| 225 | Hermelin, Danny and Mnich, Matthias and Omlor, Simon (2024). Serial batching to minimize the weighted number of tardy jobs. https://link.springer.com/article/10.1007/s10951-024-00818-9 |
| 226 | |
| 227 | Note: in P for every fixed value. |
| 228 | -/ |
| 229 | def p20_r1 (R : Reading F) : Prop := |
| 230 | InPFixed (R.at p20) (lift (Batch.numW p20)) |
| 231 | |
| 232 | /-- `1|s-batch(∞)|ΣwjUj`, parameter #d+#p: is fixed parameter tractable. |
| 233 | |
| 234 | Hermelin, Danny and Mnich, Matthias and Omlor, Simon (2024). Serial batching to minimize the weighted number of tardy jobs. https://link.springer.com/article/10.1007/s10951-024-00818-9 |
| 235 | -/ |
| 236 | def p20_r2 (R : Reading F) : Prop := |
| 237 | IsFPT (R.at p20) (tplus (lift (Batch.numD p20)) (lift (Batch.numP p20))) |
| 238 | |
| 239 | /-- `1|s-batch(∞)|ΣwjUj`, parameter #d+#w: is fixed parameter tractable. |
| 240 | |
| 241 | Hermelin, Danny and Mnich, Matthias and Omlor, Simon (2024). Serial batching to minimize the weighted number of tardy jobs. https://link.springer.com/article/10.1007/s10951-024-00818-9 |
| 242 | -/ |
| 243 | def p20_r3 (R : Reading F) : Prop := |
| 244 | IsFPT (R.at p20) (tplus (lift (Batch.numD p20)) (lift (Batch.numW p20))) |
| 245 | |
| 246 | /-- `1|s-batch(b)|ΣwjUj`, parameter #d+#w: is fixed parameter tractable. |
| 247 | |
| 248 | Hermelin, Danny and Mnich, Matthias and Omlor, Simon (2024). Serial batching to minimize the weighted number of tardy jobs. https://link.springer.com/article/10.1007/s10951-024-00818-9 |
| 249 | -/ |
| 250 | def p21_r0 (R : Reading F) : Prop := |
| 251 | IsFPT (R.at p21) (tplus (lift (Batch.numD p21)) (lift (Batch.numW p21))) |
| 252 | |
| 253 | /-- `1|s-batch(b);rj|ΣwjUj`, parameter #d+#p+#r: is fixed parameter tractable. |
| 254 | |
| 255 | Hermelin, Danny and Mnich, Matthias and Omlor, Simon (2024). Serial batching to minimize the weighted number of tardy jobs. https://link.springer.com/article/10.1007/s10951-024-00818-9 |
| 256 | -/ |
| 257 | def p22_r0 (R : Reading F) : Prop := |
| 258 | IsFPT (R.at p22) (tplus (tplus (lift (Batch.numD p22)) (lift (Batch.numP p22))) (lift (Batch.numR p22))) |
| 259 | |
| 260 | end Lax434175.ZooSerialBatchingResults |
| 261 |
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