Lax Lean Archive

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

The Scheduling Zoo, problems with restarts on parallel machines

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

proven

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

    Theorem

    The 4 problems with restarts on parallel machines of The Scheduling Zoo, each as a specification, and the 4 relations of the zoo among them that are derived here.

    A relation of the zoo states that one problem generalizes another. The 2 relations of the first list hold field by field, so that the more special problem is a special case of the more general one. The 0 relations of the second list need a threshold step, so that the decision version of the more special problem reduces to that of the more general one. The 2 relations of the third list replace completion time by flow time and likewise give a reduction of decision versions. Each pair lists the more general problem first.

    Theorem. Every pair of the first list is a special case, and every pair of the other lists is a reduction of decision versions.

    Concept map
    32 concepts; 1 descendant hidden
    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.

    1 flowReductions_hold proven

    2 specialCases_hold proven

    3 thresholdReductions_hold proven

    Lean source view on GitHub

    1import Lax434175.OperationsFamily
    2
    3/-!
    4---
    5title: The Scheduling Zoo, problems with restarts on parallel machines
    6type: theorem
    7---
    8The 4 problems with restarts on parallel machines of The Scheduling Zoo, each as a
    9specification, and the 4 relations of the zoo among them that are
    10derived here.
    11
    12A relation of the zoo states that one problem generalizes another. The
    132 relations of the first list hold field by field, so that the more
    14special problem is a special case of the more general one. The
    150 relations of the second list need a threshold step, so that the
    16decision version of the more special problem reduces to that of the more
    17general one. The 2 relations of the third list replace completion
    18time by flow time and likewise give a reduction of decision versions. Each pair lists the more general problem first.
    19
    20**Theorem.** Every pair of the first list is a special case, and every pair
    21of the other lists is a reduction of decision versions.
    22-/
    23
    24namespace Lax434175.ZooRestarts
    25open Lax434175 Lax434175.Problems Lax434175.Assembly
    26
    27/-- The family of the problems listed here. -/
    28abbrev F := OperationsFamily.family
    29
    30/-- `1|online-rj;restarts|ΣCj` -/
    31def p0 : Spec F :=
    32 OperationsFamily.spec (interruption := .restarts) (release := .online)
    33 (machineCount := .atMost 1) (objective := .sumC)
    34
    35/-- `1|online-rj;restarts|ΣwjCj` -/
    36def p1 : Spec F :=
    37 OperationsFamily.spec (interruption := .restarts) (release := .online)
    38 (machineCount := .atMost 1) (objective := .sumWC)
    39
    40/-- `1|online-rj;restarts|ΣFj` -/
    41def p2 : Spec F :=
    42 OperationsFamily.spec (interruption := .restarts) (release := .online)
    43 (machineCount := .atMost 1) (objective := .sumF)
    44
    45/-- `1|online-rj;restarts|ΣwjFj` -/
    46def p3 : Spec F :=
    47 OperationsFamily.spec (interruption := .restarts) (release := .online)
    48 (machineCount := .atMost 1) (objective := .sumWF)
    49
    50/-- The problems with their names in three-field notation. -/
    51def problems : List (String × Spec F) := [
    52 ("1|online-rj;restarts|ΣCj", p0),
    53 ("1|online-rj;restarts|ΣwjCj", p1),
    54 ("1|online-rj;restarts|ΣFj", p2),
    55 ("1|online-rj;restarts|ΣwjFj", p3)]
    56
    57/-- The relations that hold field by field: general problem, special problem. -/
    58def specialCases : List (Spec F × Spec F) := [
    59 (p1, p0), (p3, p2)]
    60
    61/-- The relations that need a threshold step: general problem, special problem. -/
    62def thresholdReductions : List (Spec F × Spec F) := [
    63]
    64
    65axiom specialCases_hold : ∀ e ∈ specialCases,
    66 SpecialCase (problem F e.2) (problem F e.1)
    67
    68axiom thresholdReductions_hold : ∀ e ∈ thresholdReductions,
    69 Reducible (problem F e.2) (problem F e.1)
    70
    71/-- The relations through flow time: general problem, special problem. -/
    72def flowReductions : List (Spec F × Spec F) := [
    73 (p2, p0), (p3, p1)]
    74
    75axiom flowReductions_hold : ∀ e ∈ flowReductions,
    76 Reducible (problem F e.2) (problem F e.1)
    77
    78end Lax434175.ZooRestarts
    79
    Show ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…