While this submission is a draft, it cannot be used by other submissions.

Scheduling on one machine as batching

Lax434175.BatchingZeroSetup · concepts/Lax434175/BatchingZeroSetup.lean · lax-434175

proven

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

    Theorem

    Batching with setup time 00 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 00, 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 AmA_m-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 ss of the family with operations reduces to a specification tt of the batching family if ss 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 tt.

    Theorem. A specification that reduces to a batching specification describes a problem whose decision version reduces to that of the batching problem.

    Concept map
    39 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax434175.PreemptionUseless
    2
    3/-!
    4---
    5title: Scheduling on one machine as batching
    6type: theorem
    7---
    8Batching with setup time 00 and batches of at most one job is scheduling on a
    9single machine: the batches are processed one after the other, and a batch
    10with one job takes the processing time of that job, in serial and in parallel
    11batching alike. Conversely, numbering the jobs of a non-preemptive schedule on
    12one machine by start time (ties by completion time and then by number) and
    13putting each job in a batch of its own gives such a batch schedule with the
    14same start and completion times.
    15
    16In serial batching the capacity may also be unbounded. With setup time 00,
    17splitting a batch into its jobs, processed one after the other in the order of
    18their numbers from the start of the batch, completes no job later and starts
    19none earlier than the batch. For a regular objective, one that does not
    20decrease when a completion time grows (every objective here except the
    21just-in-time ones), a batch schedule therefore gives a schedule on one
    22machine of no larger cost.
    23
    24Hence a problem of the family with operations that has one operation per job,
    25one machine, no interruption, no machine-set restriction, processing times
    26unit, equal or arbitrary, a precedence class other than AmA_m-orders, and
    27none of the server, forbidden times, no-idle constraints and batch setups,
    28reduces to the batching problem with the same number of jobs, processing
    29times, release dates, deadlines, precedence constraints and objective: with
    30bounded capacity, in either mode, and with unbounded capacity in serial mode
    31when the objective is regular.
    32
    33A specification ss of the family with operations reduces to a specification
    34tt of the batching family if ss is of this kind and the batching
    35specification obtained from it, in a mode and a capacity allowed for it, is
    36field by field a special case of tt.
    37
    38**Theorem.** A specification that reduces to a batching specification
    39describes a problem whose decision version reduces to that of the batching
    40problem.
    41-/
    42
    43namespace Lax434175.BatchingZeroSetup
    44open Lax434175.Problems Lax434175.Assembly
    45open Lax434175 Lax434175.Operations Lax434175.OperationsFamily Lax434175.TimeReversal
    46open Lax434175.PreemptionUseless
    47
    48def isNoneMode : Interruption.Mode → Bool
    49 | .none => true
    50 | _ => false
    51
    52def noSets : Machines → Bool
    53 | .par .none => true
    54 | _ => false
    55
    56def notAOrder : Precedence.Order → Bool
    57 | .aOrder => false
    58 | _ => true
    59
    60/-- The processing-time value of batching with the same instances. -/
    61def 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. -/
    68def 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
    76objective except the just-in-time ones. -/
    77def 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
    81batch in either mode, and unbounded capacity in serial mode for a regular
    82objective. -/
    83def 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. -/
    89def 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`. -/
    102def 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
    106instance (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
    122axiom reducible_of_reducesToBatching {s : Spec family} {t : Spec BatchFamily.family} :
    123 ReducesToBatching s t → Reducible (problem family s) (problem BatchFamily.family t)
    124
    125end Lax434175.BatchingZeroSetup
    126
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…