Lax Lean Archive

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

Non-preemptive scheduling on parallel machines

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

    A non-preemptive schedule assigns to every job a nonempty set of machines and an integral start time. The job occupies these machines without interruption from its start time until its completion time, which is the start time plus the time it needs on these machines. A schedule is feasible for the kernel if no two jobs that share a machine overlap.

    In the classical problems every job occupies a single machine; which sets of machines a job may occupy is the subject of the machine-set field.

    Theorem. Every job starts no later than it completes.

    Concept map
    4 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax434175.ParallelMachines
    2
    3/-!
    4---
    5title: Non-preemptive scheduling on parallel machines
    6type: theorem
    7---
    8A non-preemptive schedule assigns to every job a nonempty set of machines
    9and an integral start time. The job occupies these machines without
    10interruption from its start time until its completion time, which is the
    11start time plus the time it needs on these machines. A schedule is feasible
    12for the kernel if no two jobs that share a machine overlap.
    13
    14In the classical problems every job occupies a single machine; which sets of
    15machines a job may occupy is the subject of the machine-set field.
    16
    17**Theorem.** Every job starts no later than it completes.
    18-/
    19
    20namespace Lax434175.Nonpreemptive
    21open Lax434175.Kernels Lax434175.ParallelMachines
    22
    23structure Sched (x : Inst) where
    24 machines : Fin x.jobs → Finset (Fin x.machines)
    25 start : Fin x.jobs → ℕ
    26
    27def completion (x : Inst) (σ : Sched x) (j : Fin x.jobs) : ℕ :=
    28 σ.start j + duration x j (σ.machines j)
    29
    30/-- Every job occupies some machine, and two distinct jobs that share a
    31machine do not overlap. -/
    32def feasible (x : Inst) (σ : Sched x) : Prop :=
    33 (∀ j, (σ.machines j).Nonempty) ∧
    34 ∀ i j, i ≠ j → ¬ Disjoint (σ.machines i) (σ.machines j) →
    35 completion x σ i ≤ σ.start j ∨ completion x σ j ≤ σ.start i
    36
    37/-- The kernel of non-preemptive scheduling on parallel machines. -/
    38def kernel : Kernel where
    39 Inst := Inst
    40 jobs := Inst.jobs
    41 release := Inst.r
    42 Sched := Sched
    43 feasible := feasible
    44 start _ σ j := (σ.start j : NNRat)
    45 completion x σ j := (completion x σ j : NNRat)
    46
    47/-- Non-preemptive scheduling as a machine model. -/
    48def model : Model where
    49 kernel := kernel
    50 inst x := x
    51 jobs_eq _ := rfl
    52 uses _ σ j S := Sched.machines σ j = S
    53
    54axiom startsBeforeCompletion : kernel.StartsBeforeCompletion
    55
    56end Lax434175.Nonpreemptive
    57
    Show 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…