Just-in-Time Scheduling in a Two-Stage Flexible Flow Shop

Lax496464.FlowShop · concepts/Lax496464/FlowShop.lean · lax-496464

definition

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    An instance consists of nn jobs and mm identical second-stage machines. Job jj has a preprocessing time pj∈Np_j \in \mathbb{N}, a processing time qj∈Nq_j \in \mathbb{N}, a due date dj∈Nd_j \in \mathbb{N} and a weight wj∈Nw_j \in \mathbb{N}. It is run in two operations, in this order and without preemption: a preprocessing operation of length pjp_j on the single first-stage machine, and a processing operation of length qjq_j on one of the mm identical second-stage machines. Job jj is completed just in time when its second operation finishes exactly at djd_j, and the objective is to maximize the total weight of the just-in-time jobs. In the three-field notation the problem is FF(1,m)∣∣∑jwjZjFF(1,m) \mid\mid \sum_j w_j Z_j.

    Just-in-time completion pins the second operation of jj to the interval [sj,dj)[s_j, d_j), where sj=dj−qjs_j = d_j - q_j; the first operation must therefore be finished by sjs_j, 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 ZZ of jobs completed just in time, and ZZ is feasible when its jobs — and no others — admit a schedule completing every one of them exactly at its due date.

    Concept map
    1 concept; 31 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 2 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Algebra.Order.BigOperators.Group.Finset
    2import Mathlib.Data.Fintype.BigOperators
    3import Mathlib.Data.Fintype.Powerset
    4
    5/-!
    6---
    7title: Just-in-Time Scheduling in a Two-Stage Flexible Flow Shop
    8type: definition
    9---
    10An instance consists of nn jobs and mm identical second-stage machines. Job jj has a
    11preprocessing time pj∈Np_j \in \mathbb{N}, a processing time qj∈Nq_j \in \mathbb{N}, a due
    12date dj∈Nd_j \in \mathbb{N} and a weight wj∈Nw_j \in \mathbb{N}. It is run in two operations,
    13in this order and without preemption: a *preprocessing* operation of length pjp_j on the
    14single first-stage machine, and a *processing* operation of length qjq_j on one of the
    15mm identical second-stage machines. Job jj is completed *just in time* when its second
    16operation finishes exactly at djd_j, and the objective is to maximize the total weight of
    17the just-in-time jobs. In the three-field notation the problem is
    18FF(1,m)∣∣∑jwjZjFF(1,m) \mid\mid \sum_j w_j Z_j.
    19
    20Just-in-time completion pins the second operation of jj to the interval [sj,dj)[s_j, d_j),
    21where sj=dj−qjs_j = d_j - q_j; the first operation must therefore be finished by sjs_j, which
    22acts as a deadline for it. Two jobs *conflict* when those two intervals overlap, and
    23conflicting jobs cannot share a second-stage machine.
    24
    25Since the objective counts only the just-in-time jobs, a *solution* is the set ZZ of
    26jobs completed just in time, and ZZ is *feasible* when its jobs — and no others — admit
    27a schedule completing every one of them exactly at its due date.
    28
    29# Formalization Notes
    30
    31Jobs are `Fin n` rather than an abstract finite type: an instance is something a machine
    32is handed as a word, and a word presents its jobs in an order.
    33
    34Start times are integers while the data are naturals, so that sj=dj−qjs_j = d_j - q_j is a
    35genuine subtraction rather than a truncated one. A job with qj>djq_j > d_j can never be
    36completed just in time, since its second operation would have to begin before time 00;
    37the model excludes it by itself, and no side condition qj≤djq_j \le d_j appears anywhere.
    38
    39The 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 m=0m = 0, which is
    41wrong: scheduling nothing is always possible.
    42
    43A schedule assigns a start time and a machine to every job, and its conditions are
    44imposed on the jobs of ZZ only. What the jobs outside ZZ are assigned is immaterial and
    45unconstrained, which is what the paper's convention — only the jobs of ZZ are scheduled
    46— amounts to.
    47-/
    48
    49namespace Lax496464.FlowShop
    50
    51/-- An instance of the two-stage flexible flow shop: `jobs` jobs, `machines` identical
    52second-stage machines, and for each job a preprocessing time, a processing time, a due
    53date and a weight. -/
    54structure 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
    68namespace Instance
    69
    70variable (I : Instance)
    71
    72/-- A job of the instance. -/
    73abbrev Job : Type := Fin I.jobs
    74
    75variable {I}
    76
    77/-- `s j = d j - q j`: the time at which job `j`'s second operation must start if `j` is
    78to be completed just in time, and hence a deadline for its first operation. -/
    79def 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
    82their second operations overlap. Conflicting jobs cannot share a second-stage machine. -/
    83def 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
    86it can be run on a single second-stage machine. -/
    87def 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
    91one of them exactly at its due date. `pre j` is the start time of `j`'s first operation
    92and `mach j` the second-stage machine running its second operation; the second operation
    93needs no start time, because just-in-time completion pins it to `[s j, d j)`. -/
    94structure 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
    111variable (I)
    112
    113/-- `Z` is **feasible**: its jobs can all be completed just in time. -/
    114def Feasible (Z : Finset I.Job) : Prop := Nonempty (JITSchedule Z)
    115
    116/-- The objective value `w(Z) = ∑_{j ∈ Z} w j` of the solution `Z`. -/
    117def weight (Z : Finset I.Job) : ℕ := ∑ j ∈ Z, I.w j
    118
    119/-- The decision version: some feasible set has weight at least `W`. -/
    120def HasWeight (W : ℕ) : Prop := ∃ Z : Finset I.Job, Feasible I Z ∧ W ≤ weight I Z
    121
    122open Classical in
    123/-- The optimum: the largest weight of a feasible set. -/
    124noncomputable 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`. -/
    128def running (Z : Finset I.Job) (t : ℤ) : Finset I.Job :=
    129 Z.filter fun i => s i ≤ t ∧ t < (I.d i : ℤ)
    130
    131end Instance
    132
    133end Lax496464.FlowShop
    134
    Formalization Notes

    Jobs are FinnFin n 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 sj=dj−qjs_j = d_j - q_j is a genuine subtraction rather than a truncated one. A job with qj>djq_j > d_j can never be completed just in time, since its second operation would have to begin before time 00; the model excludes it by itself, and no side condition qj≤djq_j \le d_j appears anywhere.

    The machine of a schedule is a number with a bound, rather than an element of FinmFin m. The latter would make even the empty set unschedulable when m=0m = 0, 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 ZZ only. What the jobs outside ZZ are assigned is immaterial and unconstrained, which is what the paper's convention — only the jobs of ZZ are scheduled — amounts to.

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…