Lax Lean Archive

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

Results of The Scheduling Zoo, problems with restarts on parallel machines

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

definition

Loading review…

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

    Definition

    The 9 results of The Scheduling Zoo on its problems with restarts on parallel machines that are stated here, each as a proposition about a reading of the problem (Results.PReadingResults.PReading; for a family, Results.ReadingResults.Reading at the problem's specification): its words of instances and schedules and what an online scheduler sees. Each names its source; where the proposition is weaker than the wording, a note says what is left out.

    Concept map
    60 concepts
    100%
    Conjunctive normal formAssembling problems from fieldsOne family for serial and parallel batchingBatching problems in three-field notationBatch scheduling on a single machineCommunication delaysBounds on the number of machines and jobsDeadlinesForbidden times and input encodingsInterruption as a field of parallel-machineschedulingScheduling kernelsMaximizing the minimum machine loadMachine sets and multiprocessor tasksConstraint modules and objectivesNon-preemptive scheduling on parallelmachinesCompletion-time objectivesOnline scheduling as a gameScheduling with operationsOne family for parallel machines and shopsOne family for parallel machines with andwithout preemptionParallel machinesProblems on parallel machines in three-fieldnotationParameters along embeddingsPrecedence constraints and time lagsPreemptive scheduling on parallel machinesPreemptive shop problems in three-fieldnotationPreemptive shop schedulingOptimization problems and embeddingsSingle-machine scheduling with rejectionRelease datesPreemption with restarts on parallelmachinesParameters of the zoo's resultsThe kinds of results on scheduling problemsA single server with setup timesNo-idle shops and batch setup timesOne family for shops with and withoutpreemptionShop problems in three-field notationShop schedulingThreshold reductions between objectivesTransportation delays and a transport robotScheduling problems as parameterizedproblems on wordsParameters of scheduling problemsThe Scheduling Zoo, problems with restartson parallel machinesResults of The Scheduling Zoo, problemswith restarts on parallel machinesBinary encoding of an input and a certificateThe complexity class NPThe complexity class PFixed-Parameter Time on the Word RAMFPT-Reductions, FPT, Hardness andCompletenessFinite Relational StructuresFirst-Order Formulas and the Classes Σ_tand Π_tModel Checking and Weighted FaginDefinabilityThe W-Hierarchy and the A-HierarchyNP-Hardness of a Problem on Words ofNumbersBinary encoding of finite wordsPolynomial-time computation by a wordRAMPolynomial-time computation by a TuringmachineThe word RAMComputing a function within a time boundParameterized Problems andFPT-Reductions on a Word RAM
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax434175.ZooRestarts
    2import Lax434175.Results
    3import Lax434175.ResultParameters
    4
    5/-!
    6---
    7title: Results of The Scheduling Zoo, problems with restarts on parallel machines
    8type: definition
    9---
    10The 9 results of The Scheduling Zoo on its problems with restarts on parallel machines that are
    11stated here, each as a proposition about a reading of the problem
    12(`Results.PReading`; for a family, `Results.Reading` at the problem's
    13specification): its words of instances and schedules and what an online
    14scheduler sees. Each names its source; where the proposition is weaker than
    15the wording, a note says what is left out.
    16-/
    17
    18namespace Lax434175.ZooRestartsResults
    19open Lax434175 Lax434175.Problems Lax434175.Results Lax434175.ResultParameters Lax434175.ZooRestarts
    20
    21/-- `1|online-rj;restarts|ΣCj`: has a deterministic 3/2-competitive algorithm.
    22
    23Rob van Stee and
    24Johannes A. La Poutré (2005). Minimizing the total completion time on-line on a single machine,
    25using restarts. https://doi.org/10.1016/j.jalgor.2004.10.001
    26-/
    27def p0_r0 (R : Reading F) : Prop :=
    28 DetCompetitive (R.at p0) (const ((3 : ℝ) / 2))
    29
    30/-- `1|online-rj;restarts|ΣCj`: deterministic competitive ratio ge1.2108.
    31
    32Leah Epstein and
    33Rob van Stee (2003). Lower bounds for on-line single-machine scheduling. https://doi.org/10.1016/S0304-3975(02)00488-7
    34-/
    35def p0_r1 (R : Reading F) : Prop :=
    36 DetLowerBound (R.at p0) (1.2108 : ℝ)
    37
    38/-- `1|online-rj;restarts|ΣCj`: randomized competitive ratio ge1.1068.
    39
    40Leah Epstein and
    41Rob van Stee (2003). Lower bounds for on-line single-machine scheduling. https://doi.org/10.1016/S0304-3975(02)00488-7
    42-/
    43def p0_r2 (R : Reading F) : Prop :=
    44 RandLowerBound (R.at p0) (1.1068 : ℝ)
    45
    46/-- `1|online-rj;restarts|ΣwjCj`: deterministic competitive ratio ge1.2232.
    47
    48Leah Epstein and
    49Rob van Stee (2003). Lower bounds for on-line single-machine scheduling. https://doi.org/10.1016/S0304-3975(02)00488-7
    50-/
    51def p1_r0 (R : Reading F) : Prop :=
    52 DetLowerBound (R.at p1) (1.2232 : ℝ)
    53
    54/-- `1|online-rj;restarts|ΣwjCj`: randomized competitive ratio ge1.1161.
    55
    56Leah Epstein and
    57Rob van Stee (2003). Lower bounds for on-line single-machine scheduling. https://doi.org/10.1016/S0304-3975(02)00488-7
    58-/
    59def p1_r1 (R : Reading F) : Prop :=
    60 RandLowerBound (R.at p1) (1.1161 : ℝ)
    61
    62/-- `1|online-rj;restarts|ΣFj`: deterministic competitive ratio Omega(sqrtn).
    63
    64Leah Epstein and
    65Rob van Stee (2003). Lower bounds for on-line single-machine scheduling. https://doi.org/10.1016/S0304-3975(02)00488-7
    66-/
    67def p2_r0 (R : Reading F) : Prop :=
    68 DetLowerBoundFn (R.at p2) (fun x => Real.sqrt ((Ops.n p2 x) : ℝ))
    69
    70/-- `1|online-rj;restarts|ΣFj`: randomized competitive ratio Omega(sqrtn).
    71
    72Leah Epstein and
    73Rob van Stee (2003). Lower bounds for on-line single-machine scheduling. https://doi.org/10.1016/S0304-3975(02)00488-7
    74-/
    75def p2_r1 (R : Reading F) : Prop :=
    76 RandLowerBoundFn (R.at p2) (fun x => Real.sqrt ((Ops.n p2 x) : ℝ))
    77
    78/-- `1|online-rj;restarts|ΣwjFj`: deterministic competitive ratio Omega(n).
    79
    80Leah Epstein and
    81Rob van Stee (2003). Lower bounds for on-line single-machine scheduling. https://doi.org/10.1016/S0304-3975(02)00488-7
    82-/
    83def p3_r0 (R : Reading F) : Prop :=
    84 DetLowerBoundFn (R.at p3) (fun x => ((Ops.n p3 x) : ℝ))
    85
    86/-- `1|online-rj;restarts|ΣwjFj`: randomized competitive ratio Omega(n).
    87
    88Leah Epstein and
    89Rob van Stee (2003). Lower bounds for on-line single-machine scheduling. https://doi.org/10.1016/S0304-3975(02)00488-7
    90-/
    91def p3_r1 (R : Reading F) : Prop :=
    92 RandLowerBoundFn (R.at p3) (fun x => ((Ops.n p3 x) : ℝ))
    93
    94end Lax434175.ZooRestartsResults
    95
    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…