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

Preemption does not help on a single machine

Lax434175.PreemptionUseless · concepts/Lax434175/PreemptionUseless.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

    On a single machine and without release dates, a preemptive schedule can be turned into a non-preemptive one in which no job completes later: process the jobs one after the other from time 00, in the order of their completion times (ties broken by start times and then by the numbering of the jobs). A job then completes at the total processing time of the jobs before it and itself, and the machine has processed these jobs entirely by the original completion time of the job, so this total is at most that time.

    Hence a problem and the same problem with preemption allowed have the same decision versions when there is one operation per job, at most one machine, no release dates, the precedence constraints have zero lags, the objective depends monotonically on the completion times (every objective except the number of jobs not completed just in time), and there are no server, forbidden times, no-idle constraints or batch setups. Deadlines, machine sets, communication delays, no-wait and transportation delays may be present; with one operation per job on one machine the last three impose nothing more on the new schedule.

    A specification ss reduces to tt by dropping preemption if it is of this kind, has no interruption or preemption, and the same specification with the other of the two is field by field a special case of tt.

    Theorem. A specification that reduces to another by dropping preemption describes a problem whose decision version reduces to that of the other.

    Concept map
    38 concepts; 1 descendant hidden
    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.TimeReversal
    2
    3/-!
    4---
    5title: Preemption does not help on a single machine
    6type: theorem
    7---
    8On a single machine and without release dates, a preemptive schedule can be
    9turned into a non-preemptive one in which no job completes later: process the
    10jobs one after the other from time 00, in the order of their completion
    11times (ties broken by start times and then by the numbering of the jobs). A
    12job then completes at the total processing time of the jobs before it and
    13itself, and the machine has processed these jobs entirely by the original
    14completion time of the job, so this total is at most that time.
    15
    16Hence a problem and the same problem with preemption allowed have the same
    17decision versions when there is one operation per job, at most one machine,
    18no release dates, the precedence constraints have zero lags, the objective
    19depends monotonically on the completion times (every objective except the
    20number of jobs not completed just in time), and there are no server,
    21forbidden times, no-idle constraints or batch setups. Deadlines, machine sets,
    22communication delays, no-wait and transportation delays may be present; with
    23one operation per job on one machine the last three impose nothing more on
    24the new schedule.
    25
    26A specification ss reduces to tt by dropping preemption if it is of this
    27kind, has no interruption or preemption, and the same specification with the
    28other of the two is field by field a special case of tt.
    29
    30**Theorem.** A specification that reduces to another by dropping preemption
    31describes a problem whose decision version reduces to that of the other.
    32-/
    33
    34namespace Lax434175.PreemptionUseless
    35open Lax434175.Problems Lax434175.Assembly
    36open Lax434175 Lax434175.Operations Lax434175.OperationsFamily Lax434175.TimeReversal
    37
    38def atMostOne : Counts.Bound → Bool
    39 | .atMost 0 | .atMost 1 => true
    40 | _ => false
    41
    42def zeroLags (v : Precedence.Value) : Bool :=
    43 match v.lags with
    44 | .zero => true
    45 | _ => false
    46
    47def regular : Objectives.Value → Bool
    48 | .sumZ | .sumWZ => false
    49 | _ => true
    50
    51/-- The interruption swapped between none and preemption. -/
    52def swapped : Interruption.Mode → Option Interruption.Mode
    53 | .none => some .pmtn
    54 | .pmtn => some .none
    55 | .restarts | .pmtnNoMigration => none
    56
    57/-- The specification is of the kind for which preemption does not help. -/
    58def Applies (s : Spec family) : Bool :=
    59 isSingle (s.module .jobStructure) && atMostOne (s.module .machineCount) &&
    60 releaseNone (s.module .releaseDates) && zeroLags (s.module .precedence) &&
    61 regular (Thresholds.objectiveOf s) && noServer (s.module .server) &&
    62 noForbidden (s.module .forbiddenTimes) && noIdling (s.module .noIdle) &&
    63 noSetups (s.module .batchSetups)
    64
    65/-- The same specification with another way of interruption. -/
    66def withInterruption (s : Spec family) (m : Interruption.Mode) : Spec family where
    67 module
    68 | .interruption => m
    69 | i => s.module i
    70 objective := s.objective
    71
    72/-- `s` reduces to `t` by dropping or allowing preemption. -/
    73def ReducesByPreemption (s t : Spec family) : Prop :=
    74 Applies s = true ∧ ∃ m, swapped (s.module .interruption) = some m ∧ (withInterruption s m).le t
    75
    76instance (s t : Spec family) : Decidable (ReducesByPreemption s t) := by
    77 unfold ReducesByPreemption
    78 cases h : swapped (s.module .interruption) with
    79 | none => exact isFalse fun ⟨_, m, hm, _⟩ => by simp at hm
    80 | some m =>
    81 exact decidable_of_iff (Applies s = true ∧ (withInterruption s m).le t)
    82 ⟨fun ⟨h1, h2⟩ => ⟨h1, m, rfl, h2⟩, fun ⟨h1, m', hm, h2⟩ => by
    83 cases hm
    84 exact ⟨h1, h2⟩⟩
    85
    86axiom reducible_of_reducesByPreemption {s t : Spec family} :
    87 ReducesByPreemption s t → Reducible (problem family s) (problem family t)
    88
    89end Lax434175.PreemptionUseless
    90
    Show Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…