Lax Lean Archive

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

Single-machine scheduling with rejection

Lax434175.Rejection · concepts/Lax434175/Rejection.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 problem 1∣∑j∈rejectej≤B∣∑Cj1 \mid \sum_{j \in \mathrm{reject}} e_j \le B \mid \sum C_j. An instance has nn jobs with processing times pjp_j and rejection costs eje_j, and a budget BB. A solution rejects some jobs and assigns a start time to every accepted job. It is feasible if the rejection costs of the rejected jobs sum to at most BB and no two accepted jobs overlap on the machine. The cost is the total completion time of the accepted jobs.

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

    Lean source view on GitHub

    1import Mathlib.Algebra.BigOperators.Group.Finset.Basic
    2import Mathlib.Data.Fintype.BigOperators
    3import Lax434175.Problems
    4
    5/-!
    6---
    7title: Single-machine scheduling with rejection
    8type: definition
    9---
    10The problem 1∣∑j∈rejectej≤B∣∑Cj1 \mid \sum_{j \in \mathrm{reject}} e_j \le B \mid \sum C_j. An
    11instance has nn jobs with processing times pjp_j and rejection costs eje_j,
    12and a budget BB. A solution rejects some jobs and assigns a start time to
    13every accepted job. It is feasible if the rejection costs of the rejected
    14jobs sum to at most BB and no two accepted jobs overlap on the machine. The
    15cost is the total completion time of the accepted jobs.
    16-/
    17
    18namespace Lax434175.Rejection
    19open Lax434175.Problems
    20
    21structure Inst where
    22 jobs : ℕ
    23 p : Fin jobs → ℕ
    24 /-- The rejection cost of a job. -/
    25 e : Fin jobs → ℕ
    26 budget : ℕ
    27
    28structure Sched (x : Inst) where
    29 /-- The accepted jobs. -/
    30 accepted : Finset (Fin x.jobs)
    31 start : Fin x.jobs → ℕ
    32
    33def completion (x : Inst) (σ : Sched x) (j : Fin x.jobs) : ℕ := σ.start j + x.p j
    34
    35/-- The rejected jobs respect the budget and the accepted jobs do not
    36overlap. -/
    37def feasible (x : Inst) (σ : Sched x) : Prop :=
    38 ∑ j ∈ Finset.univ \ σ.accepted, x.e j ≤ x.budget ∧
    39 ∀ i ∈ σ.accepted, ∀ j ∈ σ.accepted, i ≠ j →
    40 completion x σ i ≤ σ.start j ∨ completion x σ j ≤ σ.start i
    41
    42/-- `1 | Σ_{j ∈ reject} e_j ≤ B | ΣC_j` -/
    43def problem : Problem where
    44 Inst := Inst
    45 Sched := Sched
    46 feasible := feasible
    47 cost x σ := ((∑ j ∈ σ.accepted, completion x σ j : ℕ) : ℚ)
    48
    49end Lax434175.Rejection
    50
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…