Scheduling on one machine as batching
Lax434175.BatchingZeroSetup · concepts/Lax434175/BatchingZeroSetup.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Batching with setup time and batches of at most one job is scheduling on a single machine: the batches are processed one after the other, and a batch with one job takes the processing time of that job, in serial and in parallel batching alike. Conversely, numbering the jobs of a non-preemptive schedule on one machine by start time (ties by completion time and then by number) and putting each job in a batch of its own gives such a batch schedule with the same start and completion times.
In serial batching the capacity may also be unbounded. With setup time , splitting a batch into its jobs, processed one after the other in the order of their numbers from the start of the batch, completes no job later and starts none earlier than the batch. For a regular objective, one that does not decrease when a completion time grows (every objective here except the just-in-time ones), a batch schedule therefore gives a schedule on one machine of no larger cost.
Hence a problem of the family with operations that has one operation per job, one machine, no interruption, no machine-set restriction, processing times unit, equal or arbitrary, a precedence class other than -orders, and none of the server, forbidden times, no-idle constraints and batch setups, reduces to the batching problem with the same number of jobs, processing times, release dates, deadlines, precedence constraints and objective: with bounded capacity, in either mode, and with unbounded capacity in serial mode when the objective is regular.
A specification of the family with operations reduces to a specification of the batching family if is of this kind and the batching specification obtained from it, in a mode and a capacity allowed for it, is field by field a special case of .
Theorem. A specification that reduces to a batching specification describes a problem whose decision version reduces to that of the batching problem.
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
Lean source view on GitHub
| 1 | import Lax434175.PreemptionUseless |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Scheduling on one machine as batching |
| 6 | type: theorem |
| 7 | --- |
| 8 | Batching with setup time and batches of at most one job is scheduling on a |
| 9 | single machine: the batches are processed one after the other, and a batch |
| 10 | with one job takes the processing time of that job, in serial and in parallel |
| 11 | batching alike. Conversely, numbering the jobs of a non-preemptive schedule on |
| 12 | one machine by start time (ties by completion time and then by number) and |
| 13 | putting each job in a batch of its own gives such a batch schedule with the |
| 14 | same start and completion times. |
| 15 | |
| 16 | In serial batching the capacity may also be unbounded. With setup time , |
| 17 | splitting a batch into its jobs, processed one after the other in the order of |
| 18 | their numbers from the start of the batch, completes no job later and starts |
| 19 | none earlier than the batch. For a regular objective, one that does not |
| 20 | decrease when a completion time grows (every objective here except the |
| 21 | just-in-time ones), a batch schedule therefore gives a schedule on one |
| 22 | machine of no larger cost. |
| 23 | |
| 24 | Hence a problem of the family with operations that has one operation per job, |
| 25 | one machine, no interruption, no machine-set restriction, processing times |
| 26 | unit, equal or arbitrary, a precedence class other than -orders, and |
| 27 | none of the server, forbidden times, no-idle constraints and batch setups, |
| 28 | reduces to the batching problem with the same number of jobs, processing |
| 29 | times, release dates, deadlines, precedence constraints and objective: with |
| 30 | bounded capacity, in either mode, and with unbounded capacity in serial mode |
| 31 | when the objective is regular. |
| 32 | |
| 33 | A specification of the family with operations reduces to a specification |
| 34 | of the batching family if is of this kind and the batching |
| 35 | specification obtained from it, in a mode and a capacity allowed for it, is |
| 36 | field by field a special case of . |
| 37 | |
| 38 | **Theorem.** A specification that reduces to a batching specification |
| 39 | describes a problem whose decision version reduces to that of the batching |
| 40 | problem. |
| 41 | -/ |
| 42 | |
| 43 | namespace Lax434175.BatchingZeroSetup |
| 44 | open Lax434175.Problems Lax434175.Assembly |
| 45 | open Lax434175 Lax434175.Operations Lax434175.OperationsFamily Lax434175.TimeReversal |
| 46 | open Lax434175.PreemptionUseless |
| 47 | |
| 48 | def isNoneMode : Interruption.Mode → Bool |
| 49 | | .none => true |
| 50 | | _ => false |
| 51 | |
| 52 | def noSets : Machines → Bool |
| 53 | | .par .none => true |
| 54 | | _ => false |
| 55 | |
| 56 | def notAOrder : Precedence.Order → Bool |
| 57 | | .aOrder => false |
| 58 | | _ => true |
| 59 | |
| 60 | /-- The processing-time value of batching with the same instances. -/ |
| 61 | def batchTimes : ParallelMachines.ProcessingTimes → Option Batching.ProcessingTimes |
| 62 | | .unit => some .unit |
| 63 | | .equal => some .equal |
| 64 | | .arbitrary => some .arbitrary |
| 65 | | .oneOrTwo => none |
| 66 | |
| 67 | /-- The specification is a single-machine problem that batching expresses. -/ |
| 68 | def Applies (s : Spec family) : Bool := |
| 69 | isNoneMode (s.module .interruption) && isSingle (s.module .jobStructure) && |
| 70 | atMostOne (s.module .machineCount) && (batchTimes (s.module .processingTimes)).isSome && |
| 71 | noSets (s.module .machineSets) && notAOrder (s.module .precedence).order && |
| 72 | noServer (s.module .server) && noForbidden (s.module .forbiddenTimes) && |
| 73 | noIdling (s.module .noIdle) && noSetups (s.module .batchSetups) |
| 74 | |
| 75 | /-- The objective does not decrease when a completion time grows: every |
| 76 | objective except the just-in-time ones. -/ |
| 77 | def isRegular (o : Objectives.Value) : Bool := |
| 78 | Objectives.kind o != .notJustInTime |
| 79 | |
| 80 | /-- The capacities a single-machine problem is read in: at most one job per |
| 81 | batch in either mode, and unbounded capacity in serial mode for a regular |
| 82 | objective. -/ |
| 83 | def capacityAllowed : Batching.Mode → Batching.Capacity → Objectives.Value → Bool |
| 84 | | _, .bounded, _ => true |
| 85 | | .serial, .unbounded, o => isRegular o |
| 86 | | _, _, _ => false |
| 87 | |
| 88 | /-- The batching specification of a single-machine specification. -/ |
| 89 | def toBatch (s : Spec family) (mode : Batching.Mode) (times : Batching.ProcessingTimes) |
| 90 | (capacity : Batching.Capacity) : Spec BatchFamily.family where |
| 91 | module |
| 92 | | .mode => mode |
| 93 | | .field .capacity => capacity |
| 94 | | .field .jobCount => s.module .jobCount |
| 95 | | .field .processingTimes => times |
| 96 | | .field .releaseDates => s.module .releaseDates |
| 97 | | .field .deadlines => s.module .deadlines |
| 98 | | .field .precedence => s.module .precedence |
| 99 | objective := s.objective |
| 100 | |
| 101 | /-- `s` reduces to the batching specification `t`. -/ |
| 102 | def ReducesToBatching (s : Spec family) (t : Spec BatchFamily.family) : Prop := |
| 103 | Applies s = true ∧ ∃ mode times capacity, batchTimes (s.module .processingTimes) = some times ∧ |
| 104 | capacityAllowed mode capacity s.objective = true ∧ (toBatch s mode times capacity).le t |
| 105 | |
| 106 | instance (s : Spec family) (t : Spec BatchFamily.family) : Decidable (ReducesToBatching s t) := by |
| 107 | unfold ReducesToBatching |
| 108 | cases h : batchTimes (s.module .processingTimes) with |
| 109 | | none => exact isFalse fun ⟨_, _, _, _, hm, _⟩ => by simp at hm |
| 110 | | some w => |
| 111 | exact decidable_of_iff (Applies s = true ∧ |
| 112 | ∃ mode ∈ [Batching.Mode.serial, .parallel], |
| 113 | ∃ capacity ∈ [Batching.Capacity.unbounded, .bounded, .sizes], |
| 114 | capacityAllowed mode capacity s.objective = true ∧ (toBatch s mode w capacity).le t) |
| 115 | ⟨fun ⟨h1, mode, _, capacity, _, h2, h3⟩ => ⟨h1, mode, w, capacity, rfl, h2, h3⟩, |
| 116 | fun ⟨h1, mode, w', capacity, hw, h2, h3⟩ => by |
| 117 | cases hw |
| 118 | refine ⟨h1, mode, ?_, capacity, ?_, h2, h3⟩ |
| 119 | · cases mode <;> simp |
| 120 | · cases capacity <;> simp⟩ |
| 121 | |
| 122 | axiom reducible_of_reducesToBatching {s : Spec family} {t : Spec BatchFamily.family} : |
| 123 | ReducesToBatching s t → Reducible (problem family s) (problem BatchFamily.family t) |
| 124 | |
| 125 | end Lax434175.BatchingZeroSetup |
| 126 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments