Shop scheduling
Lax434175.Shops · concepts/Lax434175/Shops.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
An instance of a shop has jobs and machines. Every job consists of a sequence of operations, each with a processing time. A schedule assigns to every operation a nonempty set of machines and an integral start time; the operation occupies these machines without interruption for its processing time. A schedule is feasible for the kernel if two different operations of the same job, or sharing a machine, do not overlap. A job starts when its first operation starts and completes when its last operation completes.
The shop-type field has the values
- open shop: every job has exactly operations, which may be processed in any order;
- flow shop: every job has exactly operations, which must be processed in their given order;
- job shop: the operations of a job must be processed in their given order;
- two-stage flexible flow shop: every job has exactly two operations, which must be processed in their given order.
A flow shop and a two-stage flexible flow shop are special cases of a job shop.
The machine field determines which sets of machines an operation may occupy. Its values are
- by position: the -th operation of every job occupies machine , as in the classical open shop and flow shop;
- dedicated: every operation occupies a given machine, and no two operations of a job are given the same machine, as in the classical job shop;
- recirculation: every operation occupies a given machine;
- stages: the first operation of every job occupies the first machine, and every later operation occupies any one of the other machines, as in the two-stage flexible flow shop;
- machine sets: every operation occupies one machine of a given set;
- fixed sets: every operation occupies all machines of a given set simultaneously;
- general: the admissible sets of machines of every operation are given explicitly.
Each of the first three values is a special case of the next and of all later ones: an operation with a given machine has a machine set, and a fixed set, consisting of that machine alone. Machine sets and fixed sets are special cases of the general value and incomparable with each other. Stages are a special case of machine sets.
The processing-time field restricts the instances to unit operations, , or to equal operations, .
The no-wait field has the values "none" and "no-wait". With no-wait, every job is processed without interruption between its first start and its completion: the time between them is the sum of its processing times. Its two values are incomparable.
Theorem. The shop-type, machine, processing-time and no-wait fields are sound.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Mathlib.Algebra.BigOperators.Group.Finset.Basic |
| 2 | import Mathlib.Data.Fintype.BigOperators |
| 3 | import Mathlib.Data.NNRat.Defs |
| 4 | import Mathlib.Data.Finset.Card |
| 5 | import Mathlib.Data.Fintype.Basic |
| 6 | import Lax434175.Modules |
| 7 | |
| 8 | /-! |
| 9 | --- |
| 10 | title: Shop scheduling |
| 11 | type: theorem |
| 12 | --- |
| 13 | An instance of a shop has jobs and machines. Every job consists of a |
| 14 | sequence of operations, each with a processing time. A schedule assigns to |
| 15 | every operation a nonempty set of machines and an integral start time; the |
| 16 | operation occupies these machines without interruption for its processing |
| 17 | time. A schedule is feasible for the kernel if two different operations of |
| 18 | the same job, or sharing a machine, do not overlap. A job starts when its |
| 19 | first operation starts and completes when its last operation completes. |
| 20 | |
| 21 | The shop-type field has the values |
| 22 | |
| 23 | - open shop: every job has exactly operations, which may be processed in |
| 24 | any order; |
| 25 | - flow shop: every job has exactly operations, which must be processed |
| 26 | in their given order; |
| 27 | - job shop: the operations of a job must be processed in their given order; |
| 28 | - two-stage flexible flow shop: every job has exactly two operations, which |
| 29 | must be processed in their given order. |
| 30 | |
| 31 | A flow shop and a two-stage flexible flow shop are special cases of a job |
| 32 | shop. |
| 33 | |
| 34 | The machine field determines which sets of machines an operation may |
| 35 | occupy. Its values are |
| 36 | |
| 37 | - by position: the -th operation of every job occupies machine , as in |
| 38 | the classical open shop and flow shop; |
| 39 | - dedicated: every operation occupies a given machine, and no two operations |
| 40 | of a job are given the same machine, as in the classical job shop; |
| 41 | - recirculation: every operation occupies a given machine; |
| 42 | - stages: the first operation of every job occupies the first machine, and |
| 43 | every later operation occupies any one of the other machines, as in the |
| 44 | two-stage flexible flow shop; |
| 45 | - machine sets: every operation occupies one machine of a given set; |
| 46 | - fixed sets: every operation occupies all machines of a given set |
| 47 | simultaneously; |
| 48 | - general: the admissible sets of machines of every operation are given |
| 49 | explicitly. |
| 50 | |
| 51 | Each of the first three values is a special case of the next and of all |
| 52 | later ones: an operation with a given machine has a machine set, and a fixed |
| 53 | set, consisting of that machine alone. Machine sets and fixed sets are |
| 54 | special cases of the general value and incomparable with each other. Stages |
| 55 | are a special case of machine sets. |
| 56 | |
| 57 | The processing-time field restricts the instances to unit operations, |
| 58 | , or to equal operations, . |
| 59 | |
| 60 | The no-wait field has the values "none" and "no-wait". With no-wait, every |
| 61 | job is processed without interruption between its first start and its |
| 62 | completion: the time between them is the sum of its processing times. Its |
| 63 | two values are incomparable. |
| 64 | |
| 65 | **Theorem.** The shop-type, machine, processing-time and no-wait fields are |
| 66 | sound. |
| 67 | -/ |
| 68 | |
| 69 | namespace Lax434175.Shops |
| 70 | open Lax434175.Kernels Lax434175.Modules |
| 71 | |
| 72 | structure Inst where |
| 73 | jobs : ℕ |
| 74 | machines : ℕ |
| 75 | /-- The number of operations of a job. -/ |
| 76 | ops : Fin jobs → ℕ |
| 77 | /-- The processing time of an operation. -/ |
| 78 | p : (j : Fin jobs) → Fin (ops j) → ℕ |
| 79 | /-- The release date of a job. -/ |
| 80 | r : Fin jobs → ℕ |
| 81 | |
| 82 | /-- An operation: a job and a position in its sequence. -/ |
| 83 | abbrev Op (x : Inst) := (j : Fin x.jobs) × Fin (x.ops j) |
| 84 | |
| 85 | structure Sched (x : Inst) where |
| 86 | machines : (j : Fin x.jobs) → Fin (x.ops j) → Finset (Fin x.machines) |
| 87 | start : (j : Fin x.jobs) → Fin (x.ops j) → ℕ |
| 88 | |
| 89 | /-- The time at which an operation completes. -/ |
| 90 | def finish (x : Inst) (σ : Sched x) (o : Op x) : ℕ := |
| 91 | σ.start o.1 o.2 + x.p o.1 o.2 |
| 92 | |
| 93 | /-- Every operation occupies some machine, and two different operations of |
| 94 | the same job or sharing a machine do not overlap. -/ |
| 95 | def feasible (x : Inst) (σ : Sched x) : Prop := |
| 96 | (∀ o : Op x, (σ.machines o.1 o.2).Nonempty) ∧ |
| 97 | ∀ a b : Op x, a ≠ b → |
| 98 | (a.1 = b.1 ∨ ¬ Disjoint (σ.machines a.1 a.2) (σ.machines b.1 b.2)) → |
| 99 | finish x σ a ≤ σ.start b.1 b.2 ∨ finish x σ b ≤ σ.start a.1 a.2 |
| 100 | |
| 101 | /-- The start of the first operation of a job. -/ |
| 102 | def jobStart (x : Inst) (σ : Sched x) (j : Fin x.jobs) : ℕ := |
| 103 | ((List.ofFn (σ.start j)).min?).getD 0 |
| 104 | |
| 105 | /-- The completion of the last operation of a job. -/ |
| 106 | def jobCompletion (x : Inst) (σ : Sched x) (j : Fin x.jobs) : ℕ := |
| 107 | ((List.ofFn (fun k => finish x σ ⟨j, k⟩)).max?).getD 0 |
| 108 | |
| 109 | /-- The kernel of non-preemptive shop scheduling. -/ |
| 110 | def kernel : Kernel where |
| 111 | Inst := Inst |
| 112 | jobs := Inst.jobs |
| 113 | release := Inst.r |
| 114 | Sched := Sched |
| 115 | feasible := feasible |
| 116 | start x σ j := (jobStart x σ j : NNRat) |
| 117 | completion x σ j := (jobCompletion x σ j : NNRat) |
| 118 | |
| 119 | /-- The number of machines, a parameter of the kernel. -/ |
| 120 | def machines : kernel.Inst → ℕ := Inst.machines |
| 121 | |
| 122 | /-- Every job has exactly one operation per machine. -/ |
| 123 | def OnePerMachine (x : Inst) : Prop := |
| 124 | ∀ j, x.ops j = x.machines |
| 125 | |
| 126 | /-- The operations of every job are processed in their given order. -/ |
| 127 | def InOrder (x : Inst) (σ : Sched x) : Prop := |
| 128 | ∀ j (k k' : Fin (x.ops j)), k < k' → finish x σ ⟨j, k⟩ ≤ σ.start j k' |
| 129 | |
| 130 | inductive ShopType |
| 131 | | open |
| 132 | | flow |
| 133 | | job |
| 134 | | flexibleFlow |
| 135 | deriving DecidableEq |
| 136 | |
| 137 | /-- The instances of a shop type. -/ |
| 138 | def ShopType.holds : ShopType → Inst → Prop |
| 139 | | .open, x => OnePerMachine x |
| 140 | | .flow, x => OnePerMachine x |
| 141 | | .job, _ => True |
| 142 | | .flexibleFlow, x => ∀ j, x.ops j = 2 |
| 143 | |
| 144 | /-- The order a shop type imposes on the operations of a job. -/ |
| 145 | def ShopType.ordered : ShopType → (x : Inst) → Sched x → Prop |
| 146 | | .open, _, _ => True |
| 147 | | .flow, x, σ => InOrder x σ |
| 148 | | .job, x, σ => InOrder x σ |
| 149 | | .flexibleFlow, x, σ => InOrder x σ |
| 150 | |
| 151 | def ShopType.le : ShopType → ShopType → Bool |
| 152 | | .flow, .job | .flexibleFlow, .job => true |
| 153 | | v, w => decide (v = w) |
| 154 | |
| 155 | /-- The shop-type field. -/ |
| 156 | def shopType : Module kernel where |
| 157 | Value := ShopType |
| 158 | Data _ _ := Unit |
| 159 | admits v x _ := v.holds x |
| 160 | constraint v x _ σ := v.ordered x σ |
| 161 | le := ShopType.le |
| 162 | embed _ _ _ := () |
| 163 | |
| 164 | inductive Machines |
| 165 | | byPosition |
| 166 | | dedicated |
| 167 | | recirculation |
| 168 | | stages |
| 169 | | sets |
| 170 | | fix |
| 171 | | general |
| 172 | |
| 173 | /-- The data of a value of the machine field. -/ |
| 174 | def Machines.Data : Machines → Inst → Type |
| 175 | | .byPosition, _ | .stages, _ => Unit |
| 176 | | .dedicated, x | .recirculation, x => (j : Fin x.jobs) → Fin (x.ops j) → ℕ |
| 177 | | .sets, x => (j : Fin x.jobs) → Fin (x.ops j) → Fin x.machines → Prop |
| 178 | | .fix, x => (j : Fin x.jobs) → Fin (x.ops j) → Finset (Fin x.machines) |
| 179 | | .general, x => (j : Fin x.jobs) → Fin (x.ops j) → Finset (Fin x.machines) → Prop |
| 180 | |
| 181 | /-- The set consisting of the machine with a given number. Machines are |
| 182 | numbered from `0`. -/ |
| 183 | def machineNumbered (x : Inst) (i : ℕ) : Finset (Fin x.machines) := |
| 184 | Finset.univ.filter (fun i' => i'.val = i) |
| 185 | |
| 186 | /-- Whether an operation may occupy a set of machines. -/ |
| 187 | def Machines.view {x : Inst} : (v : Machines) → v.Data x → |
| 188 | (j : Fin x.jobs) → Fin (x.ops j) → Finset (Fin x.machines) → Prop |
| 189 | | .byPosition, _ => fun _ k S => S = machineNumbered x k.val |
| 190 | | .dedicated, μ | .recirculation, μ => fun j k S => S = machineNumbered x (μ j k) |
| 191 | | .stages, _ => fun _ k S => |
| 192 | (k.val = 0 → S = machineNumbered x 0) ∧ (k.val ≠ 0 → S.card = 1 ∧ ∀ i ∈ S, i.val ≠ 0) |
| 193 | | .sets, M => fun j k S => S.card = 1 ∧ ∀ i ∈ S, M j k i |
| 194 | | .fix, F => fun j k S => S = F j k |
| 195 | | .general, allowed => allowed |
| 196 | |
| 197 | /-- The condition on the data: a given machine number is the number of a |
| 198 | machine, and with dedicated machines no two operations of a job are given |
| 199 | the same machine. -/ |
| 200 | def Machines.admits {x : Inst} : (v : Machines) → v.Data x → Prop |
| 201 | | .byPosition, _ => ∀ j (k : Fin (x.ops j)), k.val < x.machines |
| 202 | | .dedicated, μ => (∀ j k, μ j k < x.machines) ∧ ∀ j k k', μ j k = μ j k' → k = k' |
| 203 | | .recirculation, μ => ∀ j k, μ j k < x.machines |
| 204 | | .stages, _ => 0 < x.machines |
| 205 | | _, _ => True |
| 206 | |
| 207 | def Machines.le : Machines → Machines → Bool |
| 208 | | .byPosition, .stages | .dedicated, .stages | .recirculation, .stages => false |
| 209 | | .byPosition, _ => true |
| 210 | | .dedicated, .byPosition => false |
| 211 | | .dedicated, _ => true |
| 212 | | .recirculation, .byPosition | .recirculation, .dedicated => false |
| 213 | | .recirculation, _ => true |
| 214 | | .stages, .stages | .stages, .sets | .stages, .general => true |
| 215 | | .sets, .sets | .sets, .general => true |
| 216 | | .fix, .fix | .fix, .general => true |
| 217 | | .general, .general => true |
| 218 | | _, _ => false |
| 219 | |
| 220 | def Machines.embed : {v w : Machines} → Machines.le v w = true → (x : Inst) → |
| 221 | v.Data x → w.Data x |
| 222 | | .byPosition, .byPosition, _, _, _ => () |
| 223 | | .byPosition, .dedicated, _, _, _ | .byPosition, .recirculation, _, _, _ => |
| 224 | fun _ k => k.val |
| 225 | | .byPosition, .sets, _, _, _ => fun _ k i => i.val = k.val |
| 226 | | .byPosition, .fix, _, x, _ => fun _ k => machineNumbered x k.val |
| 227 | | .dedicated, .dedicated, _, _, μ | .dedicated, .recirculation, _, _, μ |
| 228 | | .recirculation, .recirculation, _, _, μ => μ |
| 229 | | .dedicated, .sets, _, _, μ | .recirculation, .sets, _, _, μ => fun j k i => i.val = μ j k |
| 230 | | .dedicated, .fix, _, x, μ | .recirculation, .fix, _, x, μ => |
| 231 | fun j k => machineNumbered x (μ j k) |
| 232 | | .stages, .stages, _, _, _ => () |
| 233 | | .stages, .sets, _, _, _ => fun _ k i => (k.val = 0 ∧ i.val = 0) ∨ (k.val ≠ 0 ∧ i.val ≠ 0) |
| 234 | | .sets, .sets, _, _, d => d |
| 235 | | .fix, .fix, _, _, d => d |
| 236 | | v, .general, _, _, d => v.view d |
| 237 | | .byPosition, .stages, h, _, _ | .dedicated, .stages, h, _, _ |
| 238 | | .recirculation, .stages, h, _, _ | .sets, .stages, h, _, _ | .fix, .stages, h, _, _ |
| 239 | | .general, .stages, h, _, _ | .stages, .byPosition, h, _, _ | .stages, .dedicated, h, _, _ |
| 240 | | .stages, .recirculation, h, _, _ | .stages, .fix, h, _, _ |
| 241 | | .dedicated, .byPosition, h, _, _ |
| 242 | | .recirculation, .byPosition, h, _, _ | .recirculation, .dedicated, h, _, _ |
| 243 | | .sets, .byPosition, h, _, _ | .sets, .dedicated, h, _, _ |
| 244 | | .sets, .recirculation, h, _, _ | .sets, .fix, h, _, _ | .fix, .byPosition, h, _, _ |
| 245 | | .fix, .dedicated, h, _, _ | .fix, .recirculation, h, _, _ | .fix, .sets, h, _, _ |
| 246 | | .general, .byPosition, h, _, _ | .general, .dedicated, h, _, _ |
| 247 | | .general, .recirculation, h, _, _ | .general, .sets, h, _, _ | .general, .fix, h, _, _ => |
| 248 | absurd h Bool.false_ne_true |
| 249 | |
| 250 | /-- The machine field. -/ |
| 251 | def machineSets : Module kernel where |
| 252 | Value := Machines |
| 253 | Data := Machines.Data |
| 254 | admits v _ d := v.admits d |
| 255 | constraint v _ d σ := ∀ j k, v.view d j k (Sched.machines σ j k) |
| 256 | le := Machines.le |
| 257 | embed := Machines.embed |
| 258 | |
| 259 | inductive ProcessingTimes |
| 260 | | unit |
| 261 | | equal |
| 262 | | arbitrary |
| 263 | |
| 264 | /-- The instances of a processing-time restriction. -/ |
| 265 | def ProcessingTimes.holds : ProcessingTimes → Inst → Prop |
| 266 | | .unit, x => ∀ j k, x.p j k = 1 |
| 267 | | .equal, x => ∃ p, ∀ j k, x.p j k = p |
| 268 | | .arbitrary, _ => True |
| 269 | |
| 270 | /-- The position of a value in the chain unit, equal, arbitrary. -/ |
| 271 | def ProcessingTimes.rank : ProcessingTimes → ℕ |
| 272 | | .unit => 0 |
| 273 | | .equal => 1 |
| 274 | | .arbitrary => 2 |
| 275 | |
| 276 | /-- The processing-time field. -/ |
| 277 | def processingTimes : Module kernel := |
| 278 | Module.ofRestriction ProcessingTimes ProcessingTimes.holds |
| 279 | (fun v w => decide (v.rank ≤ w.rank)) |
| 280 | |
| 281 | inductive NoWait |
| 282 | | none |
| 283 | | noWait |
| 284 | deriving DecidableEq |
| 285 | |
| 286 | /-- Every job is processed without interruption. -/ |
| 287 | def NoWait.constraint : NoWait → (x : Inst) → Sched x → Prop |
| 288 | | .none, _, _ => True |
| 289 | | .noWait, x, σ => ∀ j, jobCompletion x σ j = jobStart x σ j + ∑ k, x.p j k |
| 290 | |
| 291 | /-- The no-wait field. -/ |
| 292 | def noWait : Module kernel where |
| 293 | Value := NoWait |
| 294 | Data _ _ := Unit |
| 295 | admits _ _ _ := True |
| 296 | constraint v x _ σ := v.constraint x σ |
| 297 | le v w := decide (v = w) |
| 298 | embed _ _ _ := () |
| 299 | |
| 300 | axiom shopType_sound : shopType.Sound |
| 301 | |
| 302 | axiom machineSets_sound : machineSets.Sound |
| 303 | |
| 304 | axiom processingTimes_sound : processingTimes.Sound |
| 305 | |
| 306 | axiom noWait_sound : noWait.Sound |
| 307 | |
| 308 | end Lax434175.Shops |
| 309 |
Builds on
Used by
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments