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

Preemption does not help the total weighted completion time

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

    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 bb split times, the jobs around the last one are rearranged in one of two ways, whose changes of the cost are c(X−Y)c(X - Y) and −e(X−Y)-e(X - Y) for sums of weights XX and YY; one of them is not positive, and it leaves b−1b - 1 split times.

    Without preemption a schedule is also a preemptive one, so P∣∣∑wjCjP \mid\mid \sum w_jC_j is a special case of P∣pmtn∣∑wjCjP \mid pmtn \mid \sum w_jC_j 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 Parameters.InPlaceParameters.InPlace 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 P∣pmtn∣∑wjCjP \mid pmtn \mid \sum w_jC_j reduces to that of P∣∣∑wjCjP \mid\mid \sum w_jC_j with the same kernel instance, the same parameters of every field other than interruption, and the same threshold; in particular the zoo's P∣pmtn∣∑wjCjP \mid pmtn \mid \sum w_jC_j and P2∣pmtn∣∑wjCjP2 \mid pmtn \mid \sum w_jC_j reduce to P∣∣∑wjCjP \mid\mid \sum w_jC_j and P2∣∣∑wjCjP2 \mid\mid \sum w_jC_j.

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

    This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

    Lean source view on GitHub

    1import Lax434175.ZooParallel
    2import Lax434175.ZooPreemptive
    3import Lax434175.Parameters
    4
    5/-!
    6---
    7title: Preemption does not help the total weighted completion time
    8type: theorem
    9---
    10McNaughton (1959), Theorem 4.1: on identical parallel machines, every
    11preemptive schedule can be turned into one without preemption whose total
    12weighted completion time is not larger. The proof is an exchange: in a
    13schedule with bb split times, the jobs around the last one are rearranged in
    14one of two ways, whose changes of the cost are c(X−Y)c(X - Y) and −e(X−Y)-e(X - Y) for
    15sums of weights XX and YY; one of them is not positive, and it leaves b−1b - 1
    16split times.
    17
    18Without preemption a schedule is also a preemptive one, so
    19P∣∣∑wjCjP \mid\mid \sum w_jC_j is a special case of P∣pmtn∣∑wjCjP \mid pmtn \mid \sum w_jC_j field
    20by field. The theorem gives the converse, for every bound on the number of
    21machines: the same kernel instance, the same data and parameters in every field
    22except interruption (which changes from preemption to none and carries no data),
    23and the same threshold. The interruption field cannot be kept: a reduction in
    24place in the sense of `Parameters.InPlace` would keep every invariant field
    25parameter, 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
    28P∣pmtn∣∑wjCjP \mid pmtn \mid \sum w_jC_j reduces to that of P∣∣∑wjCjP \mid\mid \sum w_jC_j with the
    29same kernel instance, the same parameters of every field other than
    30interruption, and the same threshold; in particular the zoo's
    31P∣pmtn∣∑wjCjP \mid pmtn \mid \sum w_jC_j and P2∣pmtn∣∑wjCjP2 \mid pmtn \mid \sum w_jC_j reduce to
    32P∣∣∑wjCjP \mid\mid \sum w_jC_j and P2∣∣∑wjCjP2 \mid\mid \sum w_jC_j.
    33-/
    34
    35namespace Lax434175.McNaughton
    36open Lax434175 Lax434175.Problems Lax434175.Assembly Lax434175.Parameters
    37
    38/-- `P|pmtn|ΣwjCj` with a bound on the number of machines. -/
    39def preemptive (b : Counts.Bound) : Spec OperationsFamily.family :=
    40 OperationsFamily.spec (interruption := .pmtn) (machineCount := b) (objective := .sumWC)
    41
    42/-- `P||ΣwjCj` with the same bound. -/
    43def 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
    47kept, and the same threshold. -/
    48axiom 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`. -/
    59axiom 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`. -/
    64axiom zoo_two :
    65 Reducible (problem OperationsFamily.family ZooPreemptive.p11)
    66 (problem OperationsFamily.family ZooParallel.p32)
    67
    68end Lax434175.McNaughton
    69
    Show ProofShow ProofShow Proof

    Discussion

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

    Loading discussion…