Parameters of scheduling problems
Lax434175.ZooParameters · concepts/Lax434175/ZooParameters.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
The parameters by which scheduling problems are commonly parameterized are functions of an instance.
Over every kernel: the number of jobs and the number of distinct release dates. On parallel machines and in shops: the number of machines, the maximum processing time and the number of distinct processing times. For every objective value: the number of distinct weights and the number of distinct due dates, where an unweighted value has the weights and a value without due dates the due dates .
The first five depend on the kernel instance only. They are therefore preserved by every embedding induced by a field-wise comparison and by every reduction in place.
Theorem. Reading the data of an objective value with a more general value changes neither the number of distinct weights nor the number of distinct due dates.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Mathlib.Data.Finset.Image |
| 2 | import Mathlib.Data.Finset.Lattice.Fold |
| 3 | import Mathlib.Data.Fintype.Prod |
| 4 | import Lax434175.ParallelMachines |
| 5 | import Lax434175.Shops |
| 6 | import Lax434175.Objectives |
| 7 | |
| 8 | /-! |
| 9 | --- |
| 10 | title: Parameters of scheduling problems |
| 11 | type: theorem |
| 12 | --- |
| 13 | The parameters by which scheduling problems are commonly parameterized are |
| 14 | functions of an instance. |
| 15 | |
| 16 | Over every kernel: the number of jobs and the number of distinct release |
| 17 | dates. On parallel machines and in shops: the number of machines, the |
| 18 | maximum processing time and the number of distinct processing |
| 19 | times. For every objective value: the number of distinct weights and the |
| 20 | number of distinct due dates, where an unweighted value has the weights |
| 21 | and a value without due dates the due dates . |
| 22 | |
| 23 | The first five depend on the kernel instance only. They are therefore |
| 24 | preserved by every embedding induced by a field-wise comparison and by every |
| 25 | reduction in place. |
| 26 | |
| 27 | **Theorem.** Reading the data of an objective value with a more general |
| 28 | value changes neither the number of distinct weights nor the number of |
| 29 | distinct due dates. |
| 30 | -/ |
| 31 | |
| 32 | namespace Lax434175.ZooParameters |
| 33 | open Lax434175.Kernels Lax434175.Modules |
| 34 | |
| 35 | /-- The number of distinct values of a function on the jobs. -/ |
| 36 | def distinct {n : ℕ} (f : Fin n → ℕ) : ℕ := (Finset.univ.image f).card |
| 37 | |
| 38 | /-- The number of jobs. -/ |
| 39 | def jobs (K : Kernel) : K.Inst → ℕ := K.jobs |
| 40 | |
| 41 | /-- The number of distinct release dates. -/ |
| 42 | def releaseDates (K : Kernel) (x : K.Inst) : ℕ := distinct (K.release x) |
| 43 | |
| 44 | namespace Parallel |
| 45 | |
| 46 | /-- The number of machines. -/ |
| 47 | def machines (M : ParallelMachines.Model) : M.kernel.Inst → ℕ := ParallelMachines.machines M |
| 48 | |
| 49 | /-- The maximum processing time. -/ |
| 50 | def pmax (M : ParallelMachines.Model) (x : M.kernel.Inst) : ℕ := |
| 51 | Finset.univ.sup fun j => Finset.univ.sup fun i => (M.inst x).p j i |
| 52 | |
| 53 | /-- The number of distinct processing times. -/ |
| 54 | def processingTimes (M : ParallelMachines.Model) (x : M.kernel.Inst) : ℕ := |
| 55 | (Finset.univ.image fun q : Fin (M.inst x).jobs × Fin (M.inst x).machines => |
| 56 | (M.inst x).p q.1 q.2).card |
| 57 | |
| 58 | end Parallel |
| 59 | |
| 60 | namespace Shop |
| 61 | |
| 62 | /-- The number of machines. -/ |
| 63 | def machines : Shops.kernel.Inst → ℕ := Shops.machines |
| 64 | |
| 65 | /-- The maximum processing time of an operation. -/ |
| 66 | def pmax (x : Shops.Inst) : ℕ := |
| 67 | Finset.univ.sup fun j => Finset.univ.sup fun k => x.p j k |
| 68 | |
| 69 | /-- The number of distinct processing times of operations. -/ |
| 70 | def processingTimes (x : Shops.Inst) : ℕ := |
| 71 | (Finset.univ.image fun o : Shops.Op x => x.p o.1 o.2).card |
| 72 | |
| 73 | end Shop |
| 74 | |
| 75 | /-- The number of distinct weights. -/ |
| 76 | def weights (K : Kernel) (v : Objectives.Value) (x : K.Inst) (d : Objectives.Data K v x) : ℕ := |
| 77 | distinct (Objectives.weight v d) |
| 78 | |
| 79 | /-- The number of distinct due dates. -/ |
| 80 | def dueDates (K : Kernel) (v : Objectives.Value) (x : K.Inst) (d : Objectives.Data K v x) : ℕ := |
| 81 | distinct (Objectives.dueDate v d) |
| 82 | |
| 83 | axiom weights_embed (K : Kernel) (v w : Objectives.Value) (h : Objectives.le v w = true) |
| 84 | (x : K.Inst) (d : Objectives.Data K v x) : |
| 85 | weights K w x (Objectives.embed h x d) = weights K v x d |
| 86 | |
| 87 | axiom dueDates_embed (K : Kernel) (v w : Objectives.Value) (h : Objectives.le v w = true) |
| 88 | (x : K.Inst) (d : Objectives.Data K v x) : |
| 89 | dueDates K w x (Objectives.embed h x d) = dueDates K v x d |
| 90 | |
| 91 | end Lax434175.ZooParameters |
| 92 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments