Just-in-Time Scheduling in a Two-Stage Flexible Flow Shop
Lax496464.FlowShop · concepts/Lax496464/FlowShop.lean · lax-496464
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
An instance consists of jobs and identical second-stage machines. Job has a preprocessing time , a processing time , a due date and a weight . It is run in two operations, in this order and without preemption: a preprocessing operation of length on the single first-stage machine, and a processing operation of length on one of the identical second-stage machines. Job is completed just in time when its second operation finishes exactly at , and the objective is to maximize the total weight of the just-in-time jobs. In the three-field notation the problem is .
Just-in-time completion pins the second operation of to the interval , where ; the first operation must therefore be finished by , which acts as a deadline for it. Two jobs conflict when those two intervals overlap, and conflicting jobs cannot share a second-stage machine.
Since the objective counts only the just-in-time jobs, a solution is the set of jobs completed just in time, and is feasible when its jobs — and no others — admit a schedule completing every one of them exactly at its due date.
Concept map
In the paper
- page 2 of this submission's paper
Lean source view on GitHub
| 1 | import Mathlib.Algebra.Order.BigOperators.Group.Finset |
| 2 | import Mathlib.Data.Fintype.BigOperators |
| 3 | import Mathlib.Data.Fintype.Powerset |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Just-in-Time Scheduling in a Two-Stage Flexible Flow Shop |
| 8 | type: definition |
| 9 | --- |
| 10 | An instance consists of jobs and identical second-stage machines. Job has a |
| 11 | preprocessing time , a processing time , a due |
| 12 | date and a weight . It is run in two operations, |
| 13 | in this order and without preemption: a *preprocessing* operation of length on the |
| 14 | single first-stage machine, and a *processing* operation of length on one of the |
| 15 | identical second-stage machines. Job is completed *just in time* when its second |
| 16 | operation finishes exactly at , and the objective is to maximize the total weight of |
| 17 | the just-in-time jobs. In the three-field notation the problem is |
| 18 | . |
| 19 | |
| 20 | Just-in-time completion pins the second operation of to the interval , |
| 21 | where ; the first operation must therefore be finished by , which |
| 22 | acts as a deadline for it. Two jobs *conflict* when those two intervals overlap, and |
| 23 | conflicting jobs cannot share a second-stage machine. |
| 24 | |
| 25 | Since the objective counts only the just-in-time jobs, a *solution* is the set of |
| 26 | jobs completed just in time, and is *feasible* when its jobs — and no others — admit |
| 27 | a schedule completing every one of them exactly at its due date. |
| 28 | |
| 29 | # Formalization Notes |
| 30 | |
| 31 | Jobs are `Fin n` rather than an abstract finite type: an instance is something a machine |
| 32 | is handed as a word, and a word presents its jobs in an order. |
| 33 | |
| 34 | Start times are integers while the data are naturals, so that is a |
| 35 | genuine subtraction rather than a truncated one. A job with can never be |
| 36 | completed just in time, since its second operation would have to begin before time ; |
| 37 | the model excludes it by itself, and no side condition appears anywhere. |
| 38 | |
| 39 | The machine of a schedule is a number with a bound, rather than an element of |
| 40 | `Fin m`. The latter would make even the empty set unschedulable when , which is |
| 41 | wrong: scheduling nothing is always possible. |
| 42 | |
| 43 | A schedule assigns a start time and a machine to every job, and its conditions are |
| 44 | imposed on the jobs of only. What the jobs outside are assigned is immaterial and |
| 45 | unconstrained, which is what the paper's convention — only the jobs of are scheduled |
| 46 | — amounts to. |
| 47 | -/ |
| 48 | |
| 49 | namespace Lax496464.FlowShop |
| 50 | |
| 51 | /-- An instance of the two-stage flexible flow shop: `jobs` jobs, `machines` identical |
| 52 | second-stage machines, and for each job a preprocessing time, a processing time, a due |
| 53 | date and a weight. -/ |
| 54 | structure Instance where |
| 55 | /-- The number `n` of jobs. -/ |
| 56 | jobs : ℕ |
| 57 | /-- The number `m` of identical second-stage machines. -/ |
| 58 | machines : ℕ |
| 59 | /-- The first-stage (preprocessing) time `p j` of job `j`. -/ |
| 60 | p : Fin jobs → ℕ |
| 61 | /-- The second-stage (processing) time `q j` of job `j`. -/ |
| 62 | q : Fin jobs → ℕ |
| 63 | /-- The due date `d j` of job `j`. -/ |
| 64 | d : Fin jobs → ℕ |
| 65 | /-- The weight `w j` of job `j`. -/ |
| 66 | w : Fin jobs → ℕ |
| 67 | |
| 68 | namespace Instance |
| 69 | |
| 70 | variable (I : Instance) |
| 71 | |
| 72 | /-- A job of the instance. -/ |
| 73 | abbrev Job : Type := Fin I.jobs |
| 74 | |
| 75 | variable {I} |
| 76 | |
| 77 | /-- `s j = d j - q j`: the time at which job `j`'s second operation must start if `j` is |
| 78 | to be completed just in time, and hence a deadline for its first operation. -/ |
| 79 | def s (j : I.Job) : ℤ := (I.d j : ℤ) - I.q j |
| 80 | |
| 81 | /-- Jobs `i` and `j` **conflict** when the intervals `[s i, d i)` and `[s j, d j)` of |
| 82 | their second operations overlap. Conflicting jobs cannot share a second-stage machine. -/ |
| 83 | def Conflict (i j : I.Job) : Prop := s i < (I.d j : ℤ) ∧ s j < (I.d i : ℤ) |
| 84 | |
| 85 | /-- A set of jobs is **independent** when no two of its members conflict, that is, when |
| 86 | it can be run on a single second-stage machine. -/ |
| 87 | def Independent (Y : Finset I.Job) : Prop := |
| 88 | ∀ i ∈ Y, ∀ j ∈ Y, i ≠ j → ¬ Conflict i j |
| 89 | |
| 90 | /-- A **just-in-time schedule of `Z`**: a schedule of the jobs in `Z` completing every |
| 91 | one of them exactly at its due date. `pre j` is the start time of `j`'s first operation |
| 92 | and `mach j` the second-stage machine running its second operation; the second operation |
| 93 | needs no start time, because just-in-time completion pins it to `[s j, d j)`. -/ |
| 94 | structure JITSchedule (Z : Finset I.Job) where |
| 95 | /-- The start time of the first operation of job `j`. -/ |
| 96 | pre : I.Job → ℤ |
| 97 | /-- The second-stage machine of job `j`. -/ |
| 98 | mach : I.Job → ℕ |
| 99 | /-- No operation starts before time `0`. -/ |
| 100 | pre_nonneg : ∀ j ∈ Z, 0 ≤ pre j |
| 101 | /-- The preprocessing of `j` is finished by the time its second operation must start. -/ |
| 102 | pre_le_s : ∀ j ∈ Z, pre j + I.p j ≤ s j |
| 103 | /-- The first stage is a single machine: its operations do not overlap. -/ |
| 104 | pre_disjoint : ∀ i ∈ Z, ∀ j ∈ Z, i ≠ j → |
| 105 | pre i + I.p i ≤ pre j ∨ pre j + I.p j ≤ pre i |
| 106 | /-- Only the `m` machines of the instance are used. -/ |
| 107 | mach_lt : ∀ j ∈ Z, mach j < I.machines |
| 108 | /-- Conflicting jobs do not share a second-stage machine. -/ |
| 109 | mach_indep : ∀ i ∈ Z, ∀ j ∈ Z, i ≠ j → mach i = mach j → ¬ Conflict i j |
| 110 | |
| 111 | variable (I) |
| 112 | |
| 113 | /-- `Z` is **feasible**: its jobs can all be completed just in time. -/ |
| 114 | def Feasible (Z : Finset I.Job) : Prop := Nonempty (JITSchedule Z) |
| 115 | |
| 116 | /-- The objective value `w(Z) = ∑_{j ∈ Z} w j` of the solution `Z`. -/ |
| 117 | def weight (Z : Finset I.Job) : ℕ := ∑ j ∈ Z, I.w j |
| 118 | |
| 119 | /-- The decision version: some feasible set has weight at least `W`. -/ |
| 120 | def HasWeight (W : ℕ) : Prop := ∃ Z : Finset I.Job, Feasible I Z ∧ W ≤ weight I Z |
| 121 | |
| 122 | open Classical in |
| 123 | /-- The optimum: the largest weight of a feasible set. -/ |
| 124 | noncomputable def optimum : ℕ := |
| 125 | (Finset.univ.filter fun Z : Finset I.Job => Feasible I Z).sup (weight I) |
| 126 | |
| 127 | /-- The jobs of `Z` whose second operation is running at time `t`. -/ |
| 128 | def running (Z : Finset I.Job) (t : ℤ) : Finset I.Job := |
| 129 | Z.filter fun i => s i ≤ t ∧ t < (I.d i : ℤ) |
| 130 | |
| 131 | end Instance |
| 132 | |
| 133 | end Lax496464.FlowShop |
| 134 |
Formalization Notes
Jobs are rather than an abstract finite type: an instance is something a machine is handed as a word, and a word presents its jobs in an order.
Start times are integers while the data are naturals, so that is a genuine subtraction rather than a truncated one. A job with can never be completed just in time, since its second operation would have to begin before time ; the model excludes it by itself, and no side condition appears anywhere.
The machine of a schedule is a number with a bound, rather than an element of . The latter would make even the empty set unschedulable when , which is wrong: scheduling nothing is always possible.
A schedule assigns a start time and a machine to every job, and its conditions are imposed on the jobs of only. What the jobs outside are assigned is immaterial and unconstrained, which is what the paper's convention — only the jobs of are scheduled — amounts to.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments