Lax Lean Archive

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

Results of The Scheduling Zoo, problems outside the families

Lax434175.ZooStandaloneResults · concepts/Lax434175/ZooStandaloneResults.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 8 results of The Scheduling Zoo on its problems outside the families 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
    59 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 problemsResults of The Scheduling Zoo, problemsoutside the familiesBinary 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.Rejection
    2import Lax434175.MachineCovering
    3import Lax434175.Results
    4import Lax434175.ResultParameters
    5
    6/-!
    7---
    8title: Results of The Scheduling Zoo, problems outside the families
    9type: definition
    10---
    11The 8 results of The Scheduling Zoo on its problems outside the families that are
    12stated here, each as a proposition about a reading of the problem
    13(`Results.PReading`; for a family, `Results.Reading` at the problem's
    14specification): its words of instances and schedules and what an online
    15scheduler sees. Each names its source; where the proposition is weaker than
    16the wording, a note says what is left out.
    17-/
    18
    19namespace Lax434175.ZooStandaloneResults
    20open Lax434175 Lax434175.Problems Lax434175.Results Lax434175.ResultParameters
    21
    22/-- `P||Cmin`: has a PTAS running in time O(c_epsilon n log m) where c_epsilon is a constant depending on the desired approximation ratio 1+epsilon.
    23
    24Gerhard J. Woeginger (1997). A polynomial-time approximation scheme for maximizing the minimum machine completion time. http://www.sciencedirect.com/science/article/pii/S0167637796000557
    25
    26Note: a maximization problem: value at least 1 - ε times the optimum.
    27-/
    28def cover_r0 (R : PReading MachineCovering.problem) : Prop :=
    29 ∃ f : ℚ → ℕ, SchemeMaxWithin R (fun ε x => f ε * (Cover.n x) * Nat.log 2 (Cover.m x))
    30
    31/-- `1|Σ_j∈reject ej≤B|ΣCj`: is NP-hard.
    32
    33Danny Hermelin and Michael Pinedo and Dvir Shabtay and Nimrod Talmon (2019). On the parameterized tractability of single machine scheduling with rejection. https://doi.org/10.1016/j.ejor.2018.07.038
    34-/
    35def reject_r0 (R : PReading Rejection.problem) : Prop :=
    36 NPHard R
    37
    38/-- `1|Σ_j∈reject ej≤B|ΣCj`: is in Ppseudo.
    39
    40Danny Hermelin and Michael Pinedo and Dvir Shabtay and Nimrod Talmon (2019). On the parameterized tractability of single machine scheduling with rejection. https://doi.org/10.1016/j.ejor.2018.07.038
    41-/
    42def reject_r1 (R : PReading Rejection.problem) : Prop :=
    43 PseudoPoly R
    44
    45/-- `1|Σ_j∈reject ej≤B|ΣCj`, parameter #accept: is W[1]-hard.
    46
    47Danny Hermelin and Michael Pinedo and Dvir Shabtay and Nimrod Talmon (2019). On the parameterized tractability of single machine scheduling with rejection. https://doi.org/10.1016/j.ejor.2018.07.038
    48-/
    49def reject_r2 (R : PReading Rejection.problem) : Prop :=
    50 WHard R 1 (lift (Reject.accepted))
    51
    52/-- `1|Σ_j∈reject ej≤B|ΣCj`, parameter #p: is fixed parameter tractable.
    53
    54Danny Hermelin and Michael Pinedo and Dvir Shabtay and Nimrod Talmon (2019). On the parameterized tractability of single machine scheduling with rejection. https://doi.org/10.1016/j.ejor.2018.07.038
    55-/
    56def reject_r3 (R : PReading Rejection.problem) : Prop :=
    57 IsFPT R (lift (Reject.numP))
    58
    59/-- `1|Σ_j∈reject ej≤B|ΣCj`, parameter #e: is fixed parameter tractable.
    60
    61Danny Hermelin and Michael Pinedo and Dvir Shabtay and Nimrod Talmon (2019). On the parameterized tractability of single machine scheduling with rejection. https://doi.org/10.1016/j.ejor.2018.07.038
    62-/
    63def reject_r4 (R : PReading Rejection.problem) : Prop :=
    64 IsFPT R (lift (Reject.numE))
    65
    66/-- `1|Σ_j∈reject ej≤B|ΣCj`, parameter pmax: is fixed parameter tractable.
    67
    68Danny Hermelin and Michael Pinedo and Dvir Shabtay and Nimrod Talmon (2019). On the parameterized tractability of single machine scheduling with rejection. https://doi.org/10.1016/j.ejor.2018.07.038
    69-/
    70def reject_r5 (R : PReading Rejection.problem) : Prop :=
    71 IsFPT R (lift (Reject.pmax))
    72
    73/-- `1|Σ_j∈reject ej≤B|ΣCj`, parameter emax: is fixed parameter tractable.
    74
    75Danny Hermelin and Michael Pinedo and Dvir Shabtay and Nimrod Talmon (2019). On the parameterized tractability of single machine scheduling with rejection. https://doi.org/10.1016/j.ejor.2018.07.038
    76-/
    77def reject_r6 (R : PReading Rejection.problem) : Prop :=
    78 IsFPT R (lift (Reject.emax))
    79
    80end Lax434175.ZooStandaloneResults
    81
    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…