Preemption does not help the total weighted completion time
Lax434175.McNaughton · concepts/Lax434175/McNaughton.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
McNaughton (1959), Theorem 4.1: on identical parallel machines, every preemptive schedule can be turned into one without preemption whose total weighted completion time is not larger. The proof is an exchange: in a schedule with split times, the jobs around the last one are rearranged in one of two ways, whose changes of the cost are and for sums of weights and ; one of them is not positive, and it leaves split times.
Without preemption a schedule is also a preemptive one, so is a special case of field by field. The theorem gives the converse, for every bound on the number of machines: the same kernel instance, the same data and parameters in every field except interruption (which changes from preemption to none and carries no data), and the same threshold. The interruption field cannot be kept: a reduction in place in the sense of would keep every invariant field parameter, and whether an instance is read with preemption is one.
Theorem. For every bound on the number of machines, the decision version of reduces to that of with the same kernel instance, the same parameters of every field other than interruption, and the same threshold; in particular the zoo's and reduce to and .
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax434175.ZooParallel |
| 2 | import Lax434175.ZooPreemptive |
| 3 | import Lax434175.Parameters |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Preemption does not help the total weighted completion time |
| 8 | type: theorem |
| 9 | --- |
| 10 | McNaughton (1959), Theorem 4.1: on identical parallel machines, every |
| 11 | preemptive schedule can be turned into one without preemption whose total |
| 12 | weighted completion time is not larger. The proof is an exchange: in a |
| 13 | schedule with split times, the jobs around the last one are rearranged in |
| 14 | one of two ways, whose changes of the cost are and for |
| 15 | sums of weights and ; one of them is not positive, and it leaves |
| 16 | split times. |
| 17 | |
| 18 | Without preemption a schedule is also a preemptive one, so |
| 19 | is a special case of field |
| 20 | by field. The theorem gives the converse, for every bound on the number of |
| 21 | machines: the same kernel instance, the same data and parameters in every field |
| 22 | except interruption (which changes from preemption to none and carries no data), |
| 23 | and the same threshold. The interruption field cannot be kept: a reduction in |
| 24 | place in the sense of `Parameters.InPlace` would keep every invariant field |
| 25 | parameter, and whether an instance is read with preemption is one. |
| 26 | |
| 27 | **Theorem.** For every bound on the number of machines, the decision version of |
| 28 | reduces to that of with the |
| 29 | same kernel instance, the same parameters of every field other than |
| 30 | interruption, and the same threshold; in particular the zoo's |
| 31 | and reduce to |
| 32 | and . |
| 33 | -/ |
| 34 | |
| 35 | namespace Lax434175.McNaughton |
| 36 | open Lax434175 Lax434175.Problems Lax434175.Assembly Lax434175.Parameters |
| 37 | |
| 38 | /-- `P|pmtn|ΣwjCj` with a bound on the number of machines. -/ |
| 39 | def preemptive (b : Counts.Bound) : Spec OperationsFamily.family := |
| 40 | OperationsFamily.spec (interruption := .pmtn) (machineCount := b) (objective := .sumWC) |
| 41 | |
| 42 | /-- `P||ΣwjCj` with the same bound. -/ |
| 43 | def nonpreemptive (b : Counts.Bound) : Spec OperationsFamily.family := |
| 44 | OperationsFamily.spec (machineCount := b) (objective := .sumWC) |
| 45 | |
| 46 | /-- **McNaughton's theorem.** The same instance, every field but interruption |
| 47 | kept, and the same threshold. -/ |
| 48 | axiom preemption_useless (b : Counts.Bound) : |
| 49 | ∃ r : DecisionReduction (problem OperationsFamily.family (preemptive b)) |
| 50 | (problem OperationsFamily.family (nonpreemptive b)), |
| 51 | r.Sound ∧ (∀ x D, (r.map x D).base = x.base) ∧ |
| 52 | (∀ i, i ≠ OperationsFamily.FieldName.interruption → |
| 53 | ∀ (κ : FieldParameter (OperationsFamily.family.module i)) x D, |
| 54 | ofField OperationsFamily.family i κ (nonpreemptive b) (r.map x D) = |
| 55 | ofField OperationsFamily.family i κ (preemptive b) x) ∧ |
| 56 | ∀ x D, r.threshold x D = D |
| 57 | |
| 58 | /-- The zoo's `P|pmtn|ΣwjCj` reduces to `P||ΣwjCj`. -/ |
| 59 | axiom zoo_any : |
| 60 | Reducible (problem OperationsFamily.family ZooPreemptive.p39) |
| 61 | (problem OperationsFamily.family ZooParallel.p2) |
| 62 | |
| 63 | /-- The zoo's `P2|pmtn|ΣwjCj` reduces to `P2||ΣwjCj`. -/ |
| 64 | axiom zoo_two : |
| 65 | Reducible (problem OperationsFamily.family ZooPreemptive.p11) |
| 66 | (problem OperationsFamily.family ZooParallel.p32) |
| 67 | |
| 68 | end Lax434175.McNaughton |
| 69 |
Used by
none
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments