Preemption does not help on a single machine
Lax434175.PreemptionUseless · concepts/Lax434175/PreemptionUseless.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural 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 , 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 reduces to 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 .
Theorem. A specification that reduces to another by dropping preemption describes a problem whose decision version reduces to that of the other.
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
Lean source view on GitHub
| 1 | import Lax434175.TimeReversal |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Preemption does not help on a single machine |
| 6 | type: theorem |
| 7 | --- |
| 8 | On a single machine and without release dates, a preemptive schedule can be |
| 9 | turned into a non-preemptive one in which no job completes later: process the |
| 10 | jobs one after the other from time , in the order of their completion |
| 11 | times (ties broken by start times and then by the numbering of the jobs). A |
| 12 | job then completes at the total processing time of the jobs before it and |
| 13 | itself, and the machine has processed these jobs entirely by the original |
| 14 | completion time of the job, so this total is at most that time. |
| 15 | |
| 16 | Hence a problem and the same problem with preemption allowed have the same |
| 17 | decision versions when there is one operation per job, at most one machine, |
| 18 | no release dates, the precedence constraints have zero lags, the objective |
| 19 | depends monotonically on the completion times (every objective except the |
| 20 | number of jobs not completed just in time), and there are no server, |
| 21 | forbidden times, no-idle constraints or batch setups. Deadlines, machine sets, |
| 22 | communication delays, no-wait and transportation delays may be present; with |
| 23 | one operation per job on one machine the last three impose nothing more on |
| 24 | the new schedule. |
| 25 | |
| 26 | A specification reduces to by dropping preemption if it is of this |
| 27 | kind, has no interruption or preemption, and the same specification with the |
| 28 | other of the two is field by field a special case of . |
| 29 | |
| 30 | **Theorem.** A specification that reduces to another by dropping preemption |
| 31 | describes a problem whose decision version reduces to that of the other. |
| 32 | -/ |
| 33 | |
| 34 | namespace Lax434175.PreemptionUseless |
| 35 | open Lax434175.Problems Lax434175.Assembly |
| 36 | open Lax434175 Lax434175.Operations Lax434175.OperationsFamily Lax434175.TimeReversal |
| 37 | |
| 38 | def atMostOne : Counts.Bound → Bool |
| 39 | | .atMost 0 | .atMost 1 => true |
| 40 | | _ => false |
| 41 | |
| 42 | def zeroLags (v : Precedence.Value) : Bool := |
| 43 | match v.lags with |
| 44 | | .zero => true |
| 45 | | _ => false |
| 46 | |
| 47 | def regular : Objectives.Value → Bool |
| 48 | | .sumZ | .sumWZ => false |
| 49 | | _ => true |
| 50 | |
| 51 | /-- The interruption swapped between none and preemption. -/ |
| 52 | def 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. -/ |
| 58 | def 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. -/ |
| 66 | def 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. -/ |
| 73 | def ReducesByPreemption (s t : Spec family) : Prop := |
| 74 | Applies s = true ∧ ∃ m, swapped (s.module .interruption) = some m ∧ (withInterruption s m).le t |
| 75 | |
| 76 | instance (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 | |
| 86 | axiom reducible_of_reducesByPreemption {s t : Spec family} : |
| 87 | ReducesByPreemption s t → Reducible (problem family s) (problem family t) |
| 88 | |
| 89 | end Lax434175.PreemptionUseless |
| 90 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments