At most k scheduled jobs, and prescribed machine loads
Lax434175.Wrappers · concepts/Lax434175/Wrappers.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
Two problems built on a problem 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 scheduled jobs. An instance is an instance of together with a number . A schedule is a schedule of together with a set of at most jobs, the jobs it schedules; it is feasible if the schedule is feasible for . Its cost is the weight of the jobs that are not in or not kept, so that a cost of at most says that some schedule of at most jobs keeps weight at least , with the total weight. This is the weighted question parameterized by the number of scheduled jobs: a schedule of at most jobs and weight at least a target.
Prescribed machine loads. An instance is an instance of together with a number for every machine . A schedule is feasible if it is feasible for and every machine runs exactly jobs, a job running on a machine if a piece of one of its operations occupies it. The cost is the cost in ; with the threshold 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
Lean source view on GitHub
| 1 | import Mathlib.Data.Set.Card |
| 2 | import Lax434175.OperationsFamily |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: At most k scheduled jobs, and prescribed machine loads |
| 7 | type: definition |
| 8 | --- |
| 9 | Two problems built on a problem of the family with operations, as used for |
| 10 | interval scheduling with eligible machine sets (lax-767944). |
| 11 | |
| 12 | A job is *kept* by a schedule if it is on time, for an objective that counts |
| 13 | late jobs, or just in time, for one that counts jobs not just in time; for the |
| 14 | other objectives no job is kept. |
| 15 | |
| 16 | **At most scheduled jobs.** An instance is an instance of together |
| 17 | with a number . A schedule is a schedule of together with a set of |
| 18 | at most jobs, the jobs it schedules; it is feasible if the schedule is |
| 19 | feasible for . Its cost is the weight of the jobs that are not in or not |
| 20 | kept, so that a cost of at most says that some schedule of at most jobs |
| 21 | keeps weight at least , with the total weight. This is the weighted |
| 22 | question parameterized by the number of scheduled jobs: a schedule of at |
| 23 | most jobs and weight at least a target. |
| 24 | |
| 25 | **Prescribed machine loads.** An instance is an instance of together |
| 26 | with a number for every machine . A schedule is feasible if it is |
| 27 | feasible for and every machine runs exactly jobs, a job running |
| 28 | on a machine if a piece of one of its operations occupies it. The cost is the |
| 29 | cost in ; with the threshold and an objective that counts jobs not just |
| 30 | in time, the question is whether all jobs can be scheduled with these loads |
| 31 | (Das, Opler and Valla). |
| 32 | -/ |
| 33 | |
| 34 | namespace Lax434175.Wrappers |
| 35 | open Lax434175 Lax434175.Problems Lax434175.Assembly |
| 36 | |
| 37 | variable (s : Spec OperationsFamily.family) |
| 38 | |
| 39 | /-- The weight of a job. -/ |
| 40 | def 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. -/ |
| 44 | def 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 |
| 48 | time for one counting jobs not just in time, and never otherwise. -/ |
| 49 | def 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 | |
| 56 | open Classical in |
| 57 | /-- At most `k` scheduled jobs: the instance carries `k`, a schedule names the |
| 58 | at most `k` jobs it schedules, and the cost is the weight of the jobs not |
| 59 | scheduled or not kept. -/ |
| 60 | noncomputable 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. -/ |
| 67 | def 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 |
| 72 | machine, and a feasible schedule runs exactly that many jobs on every machine. -/ |
| 73 | def 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 | |
| 80 | end Lax434175.Wrappers |
| 81 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments