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

At most k scheduled jobs, and prescribed machine loads

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

definition

Loading review…

Sign in with ORCID

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

    Two problems built on a problem ss of the family with operations, as used for interval scheduling with eligible machine sets (lax-767944).

    A job is kept by a schedule if it is on time, for an objective that counts late jobs, or just in time, for one that counts jobs not just in time; for the other objectives no job is kept.

    At most kk scheduled jobs. An instance is an instance xx of ss together with a number kk. A schedule is a schedule of xx together with a set SS of at most kk jobs, the jobs it schedules; it is feasible if the schedule is feasible for ss. Its cost is the weight of the jobs that are not in SS or not kept, so that a cost of at most DD says that some schedule of at most kk jobs keeps weight at least W−DW - D, with WW the total weight. This is the weighted question parameterized by the number kk of scheduled jobs: a schedule of at most kk jobs and weight at least a target.

    Prescribed machine loads. An instance is an instance xx of ss together with a number qiq_i for every machine ii. A schedule is feasible if it is feasible for ss and every machine ii runs exactly qiq_i jobs, a job running on a machine if a piece of one of its operations occupies it. The cost is the cost in ss; with the threshold 00 and an objective that counts jobs not just in time, the question is whether all jobs can be scheduled with these loads (Das, Opler and Valla).

    Concept map
    32 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Data.Set.Card
    2import Lax434175.OperationsFamily
    3
    4/-!
    5---
    6title: At most k scheduled jobs, and prescribed machine loads
    7type: definition
    8---
    9Two problems built on a problem ss of the family with operations, as used for
    10interval scheduling with eligible machine sets (lax-767944).
    11
    12A job is *kept* by a schedule if it is on time, for an objective that counts
    13late jobs, or just in time, for one that counts jobs not just in time; for the
    14other objectives no job is kept.
    15
    16**At most kk scheduled jobs.** An instance is an instance xx of ss together
    17with a number kk. A schedule is a schedule of xx together with a set SS of
    18at most kk jobs, the jobs it schedules; it is feasible if the schedule is
    19feasible for ss. Its cost is the weight of the jobs that are not in SS or not
    20kept, so that a cost of at most DD says that some schedule of at most kk jobs
    21keeps weight at least W−DW - D, with WW the total weight. This is the weighted
    22question parameterized by the number kk of scheduled jobs: a schedule of at
    23most kk jobs and weight at least a target.
    24
    25**Prescribed machine loads.** An instance is an instance xx of ss together
    26with a number qiq_i for every machine ii. A schedule is feasible if it is
    27feasible for ss and every machine ii runs exactly qiq_i jobs, a job running
    28on a machine if a piece of one of its operations occupies it. The cost is the
    29cost in ss; with the threshold 00 and an objective that counts jobs not just
    30in time, the question is whether all jobs can be scheduled with these loads
    31(Das, Opler and Valla).
    32-/
    33
    34namespace Lax434175.Wrappers
    35open Lax434175 Lax434175.Problems Lax434175.Assembly
    36
    37variable (s : Spec OperationsFamily.family)
    38
    39/-- The weight of a job. -/
    40def weight (x : Inst OperationsFamily.family s) (j : Fin x.base.jobs) : ℕ :=
    41 Objectives.weight (K := Operations.kernel) s.objective x.objectiveData j
    42
    43/-- The due date of a job. -/
    44def due (x : Inst OperationsFamily.family s) (j : Fin x.base.jobs) : ℕ :=
    45 Objectives.dueDate (K := Operations.kernel) s.objective x.objectiveData j
    46
    47/-- The job is kept: on time for an objective counting late jobs, just in
    48time for one counting jobs not just in time, and never otherwise. -/
    49def Kept (x : Inst OperationsFamily.family s) (σ : Operations.Sched x.base)
    50 (j : Fin x.base.jobs) : Prop :=
    51 match Objectives.kind s.objective with
    52 | .late => Operations.kernel.completion x.base σ j ≤ (due s x j : NNRat)
    53 | .notJustInTime => Operations.kernel.completion x.base σ j = (due s x j : NNRat)
    54 | _ => False
    55
    56open Classical in
    57/-- At most `k` scheduled jobs: the instance carries `k`, a schedule names the
    58at most `k` jobs it schedules, and the cost is the weight of the jobs not
    59scheduled or not kept. -/
    60noncomputable def atMostScheduled : Problem where
    61 Inst := Inst OperationsFamily.family s × ℕ
    62 Sched x := Operations.Sched x.1.base × Finset (Fin x.1.base.jobs)
    63 feasible x σ := (problem _ s).feasible x.1 σ.1 ∧ σ.2.card ≤ x.2
    64 cost x σ := ∑ j, (weight s x.1 j : ℚ) * if j ∈ σ.2 ∧ Kept s x.1 σ.1 j then 0 else 1
    65
    66/-- The jobs that run on a machine. -/
    67def jobsOn (x : Inst OperationsFamily.family s) (σ : Operations.Sched x.base)
    68 (i : Fin x.base.machines) : Set (Fin x.base.jobs) :=
    69 {j | ∃ k, Operations.Occupies σ ⟨j, k⟩ i}
    70
    71/-- Prescribed machine loads: the instance carries a number of jobs for every
    72machine, and a feasible schedule runs exactly that many jobs on every machine. -/
    73def prescribedLoads : Problem where
    74 Inst := (x : Inst OperationsFamily.family s) × (Fin x.base.machines → ℕ)
    75 Sched x := Operations.Sched x.1.base
    76 feasible x σ := (problem _ s).feasible x.1 σ ∧
    77 ∀ i, Set.ncard (jobsOn s x.1 σ i) = x.2 i
    78 cost x σ := (problem _ s).cost x.1 σ
    79
    80end Lax434175.Wrappers
    81
    Builds on
    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…