Parameters of the zoo's results
Lax434175.ResultParameters · concepts/Lax434175/ResultParameters.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
The parameters in which the zoo states results, as functions of the instances.
On the operations family and the batching family: the number of jobs, the number of machines, the largest processing time and weight , the numbers , , , of distinct processing times, release dates, weights and due dates, the total weight and the total processing time . The processing time of an operation is its time on the first machine, as in the field of processing times, and that of a job the sum over its operations. A weight is and a due date when the objective has none.
On the operations family also:
- the number of kinds of machines (Knop and Koutecký): machines of one kind have the same processing time for every operation, so this is the number of distinct columns of the matrix ;
- the rank of that matrix over the rationals (Chen, Marx, Ye and Zhang);
- , the largest processing time of the last operation of a job (and the predicate that every job has a last operation of positive length), and , the largest number of jobs whose last operations, ending at their due dates, overlap at one instant — for jobs completed just in time the intervals (Heeger, Hermelin, Itzhaki, Schieber and Shabtay; there);
- the largest communication delay ;
- the speed ratio of uniform machines, the least over the speeds that represent the instance;
- the width of the precedence order, the largest number of pairwise incomparable jobs;
- the number of forbidden times, the instants at which no job may start or end;
- , the largest number of operations of a job;
- the number of batches into which batch setups group the jobs;
- with the threshold : the gap to the optimum of the linear relaxation [CS-LP] of the vertex-cover formulation of Correa and Schulz, as in Ambühl and Mastrolilli (2009). With the transitive closure of the precedence relation and for different jobs related in neither direction, it minimizes over with for , for , , , and for , , . Its optimum equals those of the relaxations of Potts and of Chudak and Hochbaum (their Theorems 2 to 4); the parameter is , and when negative;
- with the threshold : the time window of job runs from its release date to its deadline, and also ends at for the makespan and at for the maximum lateness, since the decision version asks for that. The pathwidth of the interval graph of the windows is the largest number of windows containing one instant, minus one, and the maximum slack is the largest window length minus processing time (Hanen and Munier Kordon). A window without end has length here; it occurs only without deadlines and with another objective.
On the batching family also and the maximum slack, with the same windows.
On single-machine scheduling with rejection: , , , the number of distinct rejection costs, the largest rejection cost , and the number of accepted jobs, read as an instance quantity: the least number of jobs a feasible solution accepts, minus the most jobs whose rejection costs fit the budget. On : and .
Concept map
Lean source view on GitHub
| 1 | import Lax434175.OperationsFamily |
| 2 | import Lax434175.BatchFamily |
| 3 | import Lax434175.ZooParameters |
| 4 | import Lax434175.Parameters |
| 5 | import Lax434175.Results |
| 6 | import Lax434175.Rejection |
| 7 | import Lax434175.MachineCovering |
| 8 | import Mathlib.LinearAlgebra.Matrix.Rank |
| 9 | |
| 10 | /-! |
| 11 | --- |
| 12 | title: Parameters of the zoo's results |
| 13 | type: definition |
| 14 | --- |
| 15 | The parameters in which the zoo states results, as functions of the instances. |
| 16 | |
| 17 | On the operations family and the batching family: the number of jobs, the |
| 18 | number of machines, the largest processing time and weight |
| 19 | , the numbers , , , of distinct processing times, |
| 20 | release dates, weights and due dates, the total weight and the total |
| 21 | processing time . The processing time of an operation is its time on the |
| 22 | first machine, as in the field of processing times, and that of a job the sum |
| 23 | over its operations. A weight is and a due date when the objective has |
| 24 | none. |
| 25 | |
| 26 | On the operations family also: |
| 27 | |
| 28 | - the number of *kinds* of machines (Knop and Koutecký): machines of one kind |
| 29 | have the same processing time for every operation, so this is the number of |
| 30 | distinct columns of the matrix ; |
| 31 | - the *rank* of that matrix over the rationals (Chen, Marx, Ye and Zhang); |
| 32 | - , the largest processing time of the last operation of a job (and the |
| 33 | predicate that every job has a last operation of positive length), and |
| 34 | , the largest number of jobs whose last operations, ending at their due |
| 35 | dates, overlap at one instant — for jobs completed just in time the |
| 36 | intervals (Heeger, Hermelin, Itzhaki, Schieber and |
| 37 | Shabtay; there); |
| 38 | - the largest communication delay ; |
| 39 | - the speed ratio of uniform machines, the least over the |
| 40 | speeds that represent the instance; |
| 41 | - the width of the precedence order, the largest number of pairwise |
| 42 | incomparable jobs; |
| 43 | - the number of forbidden times, the instants at which no job may start |
| 44 | or end; |
| 45 | - , the largest number of operations of a job; |
| 46 | - the number of batches into which batch setups group the jobs; |
| 47 | - with the threshold : the gap to the optimum |
| 48 | of the linear relaxation [CS-LP] of the vertex-cover formulation |
| 49 | of Correa and Schulz, as in Ambühl and Mastrolilli (2009). With the |
| 50 | transitive closure of the precedence relation and for |
| 51 | different jobs related in neither direction, it minimizes |
| 52 | |
| 53 | over with for , |
| 54 | for , , |
| 55 | , and for , |
| 56 | , . Its optimum equals those of the |
| 57 | relaxations of Potts and of Chudak and Hochbaum (their Theorems 2 to 4); the |
| 58 | parameter is , and when negative; |
| 59 | - with the threshold : the time window of job runs from its release date |
| 60 | to its deadline, and also ends at for the makespan and at for the |
| 61 | maximum lateness, since the decision version asks for that. The pathwidth |
| 62 | of the interval graph of the windows is the largest number of |
| 63 | windows containing one instant, minus one, and the maximum slack is the largest |
| 64 | window length minus processing time (Hanen and Munier Kordon). A window without |
| 65 | end has length here; it occurs only without deadlines and with another |
| 66 | objective. |
| 67 | |
| 68 | On the batching family also and the maximum slack, with the |
| 69 | same windows. |
| 70 | |
| 71 | On single-machine scheduling with rejection: , , , the number |
| 72 | of distinct rejection costs, the largest rejection cost , and the |
| 73 | number of accepted jobs, read as an instance quantity: the least number of jobs |
| 74 | a feasible solution accepts, minus the most jobs whose rejection costs fit |
| 75 | the budget. On : and . |
| 76 | -/ |
| 77 | |
| 78 | namespace Lax434175.ResultParameters |
| 79 | open Lax434175 Lax434175.Problems Lax434175.Assembly Lax434175.Parameters |
| 80 | open Lax434175.Results |
| 81 | |
| 82 | /-- The sum of two parameters. -/ |
| 83 | def plus {P : Problem} (κ κ' : Parameter P) : Parameter P := fun x => κ x + κ' x |
| 84 | |
| 85 | /-- The largest number of the intervals `[a i, b i)` that contain one instant. -/ |
| 86 | noncomputable def overlap {n : ℕ} (a b : Fin n → ℕ∞) : ℕ := |
| 87 | sSup {k | ∃ t : ℕ, k = (Finset.univ.filter fun j => a j ≤ t ∧ (t : ℕ∞) < b j).card} |
| 88 | |
| 89 | namespace Ops |
| 90 | |
| 91 | variable (s : Spec OperationsFamily.family) |
| 92 | |
| 93 | /-- The number of jobs. -/ |
| 94 | def n : Parameter (problem _ s) := fun x => x.base.jobs |
| 95 | |
| 96 | /-- The number of machines. -/ |
| 97 | def m : Parameter (problem _ s) := fun x => x.base.machines |
| 98 | |
| 99 | /-- The largest processing time of an operation. -/ |
| 100 | def pmax : Parameter (problem _ s) := fun x => |
| 101 | Finset.univ.sup fun o : Operations.Op x.base => Operations.opTime x.base o |
| 102 | |
| 103 | /-- The number of distinct processing times of operations. -/ |
| 104 | def numP : Parameter (problem _ s) := fun x => |
| 105 | (Finset.univ.image fun o : Operations.Op x.base => Operations.opTime x.base o).card |
| 106 | |
| 107 | /-- The number of distinct release dates. -/ |
| 108 | def numR : Parameter (problem _ s) := fun x => ZooParameters.distinct x.base.r |
| 109 | |
| 110 | /-- The number of distinct weights. -/ |
| 111 | def numW : Parameter (problem _ s) := fun x => |
| 112 | ZooParameters.weights Operations.kernel s.objective x.base x.objectiveData |
| 113 | |
| 114 | /-- The number of distinct due dates. -/ |
| 115 | def numD : Parameter (problem _ s) := fun x => |
| 116 | ZooParameters.dueDates Operations.kernel s.objective x.base x.objectiveData |
| 117 | |
| 118 | /-- The weight of a job. -/ |
| 119 | def weight (x : Inst _ s) (j : Fin x.base.jobs) : ℕ := |
| 120 | Objectives.weight (K := Operations.kernel) s.objective x.objectiveData j |
| 121 | |
| 122 | /-- The due date of a job. -/ |
| 123 | def due (x : Inst _ s) (j : Fin x.base.jobs) : ℕ := |
| 124 | Objectives.dueDate (K := Operations.kernel) s.objective x.objectiveData j |
| 125 | |
| 126 | /-- The largest weight. -/ |
| 127 | def wmax : Parameter (problem _ s) := fun x => Finset.univ.sup (weight s x) |
| 128 | |
| 129 | /-- The total weight. -/ |
| 130 | def totalW : Parameter (problem _ s) := fun x => ∑ j, weight s x j |
| 131 | |
| 132 | /-- The processing time of a job: the sum over its operations. -/ |
| 133 | def ptime (x : Operations.Inst) (j : Fin x.jobs) : ℕ := |
| 134 | ∑ k : Fin (x.ops j), Operations.opTime x ⟨j, k⟩ |
| 135 | |
| 136 | /-- The total processing time. -/ |
| 137 | def totalP : Parameter (problem _ s) := fun x => ∑ j, ptime x.base j |
| 138 | |
| 139 | /-- The number of kinds of machines: distinct columns of the matrix of |
| 140 | processing times. -/ |
| 141 | def kinds : Parameter (problem _ s) := fun x => |
| 142 | (Finset.univ.image fun i : Fin x.base.machines => |
| 143 | fun o : Operations.Op x.base => x.base.p o.1 o.2 i).card |
| 144 | |
| 145 | /-- The rank of the matrix of processing times. -/ |
| 146 | noncomputable def rank : Parameter (problem _ s) := fun x => |
| 147 | (Matrix.of fun (o : Operations.Op x.base) (i : Fin x.base.machines) => |
| 148 | (x.base.p o.1 o.2 i : ℚ)).rank |
| 149 | |
| 150 | /-- The processing time of the last operation of a job, `0` without operations. -/ |
| 151 | def lastTime (x : Operations.Inst) (j : Fin x.jobs) : ℕ := |
| 152 | if h : 0 < x.ops j then Operations.opTime x ⟨j, ⟨x.ops j - 1, by omega⟩⟩ else 0 |
| 153 | |
| 154 | /-- Every job has a last operation of positive length. -/ |
| 155 | def lastPositive (x : (problem _ s).Inst) : Prop := ∀ j, 0 < lastTime x.base j |
| 156 | |
| 157 | /-- `q_max`: the largest processing time of a last operation. -/ |
| 158 | def qmax : Parameter (problem _ s) := fun x => Finset.univ.sup (lastTime x.base) |
| 159 | |
| 160 | /-- `χ`: the largest number of jobs whose last operations, ending at their due |
| 161 | dates, overlap at one instant. -/ |
| 162 | noncomputable def chi : Parameter (problem _ s) := fun x => |
| 163 | overlap (fun j => ((due s x j - lastTime x.base j : ℕ) : ℕ∞)) (fun j => (due s x j : ℕ∞)) |
| 164 | |
| 165 | /-- The largest communication delay. -/ |
| 166 | noncomputable def cmax : Parameter (problem _ s) := fun x => |
| 167 | sSup {c | ∃ i j, CommunicationDelays.view (s.module .communicationDelays) |
| 168 | (x.data .communicationDelays : CommunicationDelays.Data _ x.base.toPar) i j c} |
| 169 | |
| 170 | /-- The speed ratio `s_max / s_min` of uniform machines: the least over the |
| 171 | speeds representing the instance. -/ |
| 172 | noncomputable def speedRatio (x : Inst _ s) : ℝ := |
| 173 | sInf {r | ∃ (q : Operations.Op x.base → ℕ) (sp : Fin x.base.machines → ℕ), |
| 174 | (∀ o i, 0 < sp i ∧ x.base.p o.1 o.2 i * sp i = q o) ∧ |
| 175 | ∀ i i', (sp i : ℝ) ≤ r * sp i'} |
| 176 | |
| 177 | /-- The precedence relation of an instance. -/ |
| 178 | def prec (x : Inst _ s) (i j : Fin x.base.jobs) : Prop := |
| 179 | (s.module .precedence).order.view (x.data .precedence).1 i j |
| 180 | |
| 181 | /-- The width of the precedence order: the largest set of jobs no two of which |
| 182 | are related by the transitive closure. -/ |
| 183 | noncomputable def width : Parameter (problem _ s) := fun x => |
| 184 | sSup {k | ∃ S : Finset (Fin x.base.jobs), S.card = k ∧ |
| 185 | ∀ i ∈ S, ∀ j ∈ S, ¬ Relation.TransGen (prec s x) i j} |
| 186 | |
| 187 | /-- The end of the time window of a job with the threshold `D`: its deadline, |
| 188 | and also `D` for the makespan and `d_j + D` for the maximum lateness. -/ |
| 189 | noncomputable def windowEnd (x : Inst _ s) (D : ℤ) (j : Fin x.base.jobs) : ℕ∞ := |
| 190 | min (Deadlines.view (K := Operations.kernel) (s.module .deadlines) (x.data .deadlines) j) |
| 191 | (match s.objective with |
| 192 | | .makespan => (D.toNat : ℕ∞) |
| 193 | | .lmax => (((due s x j : ℤ) + D).toNat : ℕ∞) |
| 194 | | _ => ⊤) |
| 195 | |
| 196 | /-- `pw(I)`: the largest number of time windows containing one instant, minus |
| 197 | one. -/ |
| 198 | noncomputable def pw : TParameter (problem _ s) := fun x D => |
| 199 | overlap (fun j => (x.base.r j : ℕ∞)) (windowEnd s x D) - 1 |
| 200 | |
| 201 | /-- The maximum slack: the largest window length minus processing time. -/ |
| 202 | noncomputable def slackmax : TParameter (problem _ s) := fun x D => |
| 203 | Finset.univ.sup fun j => (windowEnd s x D j).toNat - ptime x.base j - x.base.r j |
| 204 | |
| 205 | /-- `τ`: the number of forbidden times, the instants at which no job may start or end. -/ |
| 206 | def tau : Parameter (problem _ s) := fun x => |
| 207 | (ForbiddenTimes.view (s.module .forbiddenTimes) (x.data .forbiddenTimes)).dedup.length |
| 208 | |
| 209 | /-- `n_max`: the largest number of operations of a job. -/ |
| 210 | def nmax : Parameter (problem _ s) := fun x => Finset.univ.sup x.base.ops |
| 211 | |
| 212 | /-- `g`: the number of batches into which batch setups group the jobs. -/ |
| 213 | def numBatches : Parameter (problem _ s) := fun x => |
| 214 | (Finset.univ.image fun j => ShopExtras.BatchSetups.batch (x := x.base.toShop) |
| 215 | (s.module .batchSetups) (x.data .batchSetups) j).card |
| 216 | |
| 217 | /-- Two different jobs related in neither direction by the precedence order. -/ |
| 218 | def Incomparable (x : Inst _ s) (i j : Fin x.base.jobs) : Prop := |
| 219 | i ≠ j ∧ ¬ Relation.TransGen (prec s x) i j ∧ ¬ Relation.TransGen (prec s x) j i |
| 220 | |
| 221 | /-- A feasible solution of [CS-LP] (Correa and Schulz; Ambühl and Mastrolilli 2009). -/ |
| 222 | def CSFeasible (x : Inst _ s) (δ : Fin x.base.jobs → Fin x.base.jobs → ℝ) : Prop := |
| 223 | (∀ i j, 0 ≤ δ i j) ∧ |
| 224 | (∀ i j, Incomparable s x i j → 1 ≤ δ i j + δ j i) ∧ |
| 225 | (∀ i j k, Relation.TransGen (prec s x) i j → Incomparable s x j k → Incomparable s x k i → |
| 226 | 1 ≤ δ i k + δ k j) ∧ |
| 227 | (∀ i j k l, Relation.TransGen (prec s x) i j → Incomparable s x j k → |
| 228 | Relation.TransGen (prec s x) k l → Incomparable s x l i → 1 ≤ δ i l + δ k j) |
| 229 | |
| 230 | open Classical in |
| 231 | /-- The objective of [CS-LP]. -/ |
| 232 | noncomputable def csValue (x : Inst _ s) (δ : Fin x.base.jobs → Fin x.base.jobs → ℝ) : ℝ := |
| 233 | ∑ j, (ptime x.base j * weight s x j : ℝ) + |
| 234 | ∑ i, ∑ j, (if Relation.TransGen (prec s x) i j then (ptime x.base i * weight s x j : ℝ) |
| 235 | else if Incomparable s x i j then δ i j * ptime x.base i * weight s x j else 0) |
| 236 | |
| 237 | /-- The optimum of [CS-LP], a lower bound on the total weighted completion time |
| 238 | on one machine. -/ |
| 239 | noncomputable def csLP (x : Inst _ s) : ℝ := |
| 240 | sInf (csValue s x '' {δ | CSFeasible s x δ}) |
| 241 | |
| 242 | /-- `D − LP`: the threshold minus the optimum of [CS-LP], rounded up, and `0` |
| 243 | when negative. -/ |
| 244 | noncomputable def gapLP : TParameter (problem _ s) := fun x D => ⌈(D : ℝ) - csLP s x⌉₊ |
| 245 | |
| 246 | end Ops |
| 247 | |
| 248 | namespace Batch |
| 249 | |
| 250 | variable (s : Spec BatchFamily.family) |
| 251 | |
| 252 | /-- The number of jobs. -/ |
| 253 | def n : Parameter (problem _ s) := fun x => x.base.jobs |
| 254 | |
| 255 | /-- The largest processing time. -/ |
| 256 | def pmax : Parameter (problem _ s) := fun x => Finset.univ.sup x.base.p |
| 257 | |
| 258 | /-- The number of distinct processing times. -/ |
| 259 | def numP : Parameter (problem _ s) := fun x => ZooParameters.distinct x.base.p |
| 260 | |
| 261 | /-- The number of distinct release dates. -/ |
| 262 | def numR : Parameter (problem _ s) := fun x => ZooParameters.distinct x.base.r |
| 263 | |
| 264 | /-- The number of distinct weights. -/ |
| 265 | def numW : Parameter (problem _ s) := fun x => |
| 266 | ZooParameters.weights BatchFamily.kernel s.objective x.base x.objectiveData |
| 267 | |
| 268 | /-- The number of distinct due dates. -/ |
| 269 | def numD : Parameter (problem _ s) := fun x => |
| 270 | ZooParameters.dueDates BatchFamily.kernel s.objective x.base x.objectiveData |
| 271 | |
| 272 | /-- The weight of a job. -/ |
| 273 | def weight (x : Inst _ s) (j : Fin x.base.jobs) : ℕ := |
| 274 | Objectives.weight (K := BatchFamily.kernel) s.objective x.objectiveData j |
| 275 | |
| 276 | /-- The largest weight. -/ |
| 277 | def wmax : Parameter (problem _ s) := fun x => Finset.univ.sup (weight s x) |
| 278 | |
| 279 | /-- The total weight. -/ |
| 280 | def totalW : Parameter (problem _ s) := fun x => ∑ j, weight s x j |
| 281 | |
| 282 | /-- The total processing time. -/ |
| 283 | def totalP : Parameter (problem _ s) := fun x => ∑ j, x.base.p j |
| 284 | |
| 285 | /-- The due date of a job. -/ |
| 286 | def due (x : Inst _ s) (j : Fin x.base.jobs) : ℕ := |
| 287 | Objectives.dueDate (K := BatchFamily.kernel) s.objective x.objectiveData j |
| 288 | |
| 289 | /-- The end of the time window of a job with the threshold `D`, as on the |
| 290 | operations family. -/ |
| 291 | noncomputable def windowEnd (x : Inst _ s) (D : ℤ) (j : Fin x.base.jobs) : ℕ∞ := |
| 292 | min (Deadlines.view (K := BatchFamily.kernel) (s.module (.field .deadlines)) |
| 293 | (x.data (.field .deadlines)) j) |
| 294 | (match s.objective with |
| 295 | | .makespan => (D.toNat : ℕ∞) |
| 296 | | .lmax => (((due s x j : ℤ) + D).toNat : ℕ∞) |
| 297 | | _ => ⊤) |
| 298 | |
| 299 | /-- `pw(I)`: the largest number of time windows containing one instant, minus |
| 300 | one. -/ |
| 301 | noncomputable def pw : TParameter (problem _ s) := fun x D => |
| 302 | overlap (fun j => (x.base.r j : ℕ∞)) (windowEnd s x D) - 1 |
| 303 | |
| 304 | /-- The maximum slack: the largest window length minus processing time. -/ |
| 305 | noncomputable def slackmax : TParameter (problem _ s) := fun x D => |
| 306 | Finset.univ.sup fun j => (windowEnd s x D j).toNat - x.base.p j - x.base.r j |
| 307 | |
| 308 | end Batch |
| 309 | |
| 310 | namespace Reject |
| 311 | |
| 312 | /-- The number of jobs. -/ |
| 313 | def n : Parameter Rejection.problem := fun x => x.jobs |
| 314 | |
| 315 | /-- The number of distinct processing times. -/ |
| 316 | def numP : Parameter Rejection.problem := fun x => ZooParameters.distinct x.p |
| 317 | |
| 318 | /-- The largest processing time. -/ |
| 319 | def pmax : Parameter Rejection.problem := fun x => Finset.univ.sup x.p |
| 320 | |
| 321 | /-- The number of distinct rejection costs. -/ |
| 322 | def numE : Parameter Rejection.problem := fun x => ZooParameters.distinct x.e |
| 323 | |
| 324 | /-- The largest rejection cost. -/ |
| 325 | def emax : Parameter Rejection.problem := fun x => Finset.univ.sup x.e |
| 326 | |
| 327 | /-- The least number of jobs a feasible solution accepts: `n` minus the most |
| 328 | jobs whose rejection costs fit the budget. -/ |
| 329 | noncomputable def accepted : Parameter Rejection.problem := fun x => |
| 330 | x.jobs - sSup {k | ∃ S : Finset (Fin x.jobs), S.card = k ∧ ∑ j ∈ S, x.e j ≤ x.budget} |
| 331 | |
| 332 | end Reject |
| 333 | |
| 334 | namespace Cover |
| 335 | |
| 336 | /-- The number of jobs. -/ |
| 337 | def n : Parameter MachineCovering.problem := fun x => x.jobs |
| 338 | |
| 339 | /-- The number of machines. -/ |
| 340 | def m : Parameter MachineCovering.problem := fun x => x.machines |
| 341 | |
| 342 | end Cover |
| 343 | |
| 344 | end Lax434175.ResultParameters |
| 345 |
Builds on
Used by
Lax434175.DominationLax434175.IsemStandardLax434175.StandardReadingLax434175.ThresholdParamsLax434175.ZooOpenLax434175.ZooOpenParamsLax434175.ZooParallelBatchingResultsLax434175.ZooParallelResultsLax434175.ZooPreemptiveResultsLax434175.ZooPreemptiveShopsResultsLax434175.ZooRestartsResultsLax434175.ZooSerialBatchingResultsLax434175.ZooShopsResultsLax434175.ZooStandaloneResults
From Mathlib
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments