Problems on parallel machines in three-field notation
Lax434175.ParallelProblems · concepts/Lax434175/ParallelProblems.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
The family of problems of a machine model on parallel machines has the constraint fields machine environment, number of machines, number of jobs, processing times, machine sets, release dates, deadlines, precedence constraints with time lags, communication delays, a server, forbidden times and the input encoding, and the completion-time objectives.
A problem of the three-field notation is one specification of this family: is the machine environment and count, lists the values of the constraint fields, and is the objective. The entry of selects the preemptive machine model, and the entry restarts the model with restarts; the concept on one family for parallel machines joins the three models into a single family with an interruption field. For example , , and are the specifications below.
Theorem. In every machine model, a specification that is field by field a special case of another describes a special case of the other's problem, and a specification that reduces to another describes a problem whose decision version reduces to that of the other. The same holds for reductions through flow time in every machine model in which jobs start no later than they complete. In particular is a special case of .
Concept map
Evidence
This concept declares 5 statements. Each proof establishes one of them relative to its assumptions.
1 family_sound proven
2 reducible_of_reduces proven
3 reducible_of_reducesThroughFlow proven
4 single_sumC_specialCase proven
5 specialCase_of_le proven
Lean source view on GitHub
| 1 | import Lax434175.Assembly |
| 2 | import Lax434175.Counts |
| 3 | import Lax434175.ReleaseDates |
| 4 | import Lax434175.Deadlines |
| 5 | import Lax434175.Precedence |
| 6 | import Lax434175.Thresholds |
| 7 | import Lax434175.MachineSets |
| 8 | import Lax434175.CommunicationDelays |
| 9 | import Lax434175.Servers |
| 10 | import Lax434175.ForbiddenTimes |
| 11 | import Lax434175.Restarts |
| 12 | import Lax434175.Nonpreemptive |
| 13 | import Lax434175.Preemptive |
| 14 | |
| 15 | /-! |
| 16 | --- |
| 17 | title: Problems on parallel machines in three-field notation |
| 18 | type: theorem |
| 19 | --- |
| 20 | The family of problems of a machine model on parallel machines has the |
| 21 | constraint fields machine environment, number of machines, number of jobs, |
| 22 | processing times, machine sets, release dates, deadlines, precedence |
| 23 | constraints with time lags, communication delays, a server, forbidden times |
| 24 | and the input encoding, and the |
| 25 | completion-time objectives. |
| 26 | |
| 27 | A problem of the three-field notation is one |
| 28 | specification of this family: is the machine environment and count, |
| 29 | lists the values of the constraint fields, and is the |
| 30 | objective. The entry of selects the preemptive |
| 31 | machine model, and the entry restarts the model with restarts; the concept on |
| 32 | one family for parallel machines joins the three models into a single family |
| 33 | with an interruption field. For example , , |
| 34 | and |
| 35 | are the specifications below. |
| 36 | |
| 37 | **Theorem.** In every machine model, a specification that is field by field a |
| 38 | special case of another describes a special case of the other's problem, and |
| 39 | a specification that reduces to another describes a problem whose decision |
| 40 | version reduces to that of the other. The same holds for reductions through |
| 41 | flow time in every machine model in which jobs start no later than they |
| 42 | complete. In |
| 43 | particular is a special case of |
| 44 | . |
| 45 | -/ |
| 46 | |
| 47 | namespace Lax434175.ParallelProblems |
| 48 | open Lax434175.Problems Lax434175.Kernels Lax434175.Modules Lax434175.Assembly |
| 49 | open Lax434175 |
| 50 | |
| 51 | /-- The constraint fields of the family. -/ |
| 52 | inductive FieldName |
| 53 | | environment |
| 54 | | machineCount |
| 55 | | jobCount |
| 56 | | processingTimes |
| 57 | | machineSets |
| 58 | | releaseDates |
| 59 | | deadlines |
| 60 | | precedence |
| 61 | | communicationDelays |
| 62 | | server |
| 63 | | forbiddenTimes |
| 64 | | encoding |
| 65 | deriving DecidableEq |
| 66 | |
| 67 | instance : Fintype FieldName where |
| 68 | elems := {.environment, .machineCount, .jobCount, .processingTimes, .machineSets, .releaseDates, |
| 69 | .deadlines, .precedence, .communicationDelays, .server, |
| 70 | .forbiddenTimes, .encoding} |
| 71 | complete x := by cases x <;> decide |
| 72 | |
| 73 | /-- The problems of a machine model on parallel machines. -/ |
| 74 | abbrev family (M : ParallelMachines.Model) : Family M.kernel := |
| 75 | Thresholds.family FieldName fun |
| 76 | | .environment => ParallelMachines.environment M |
| 77 | | .machineCount => Counts.module _ (ParallelMachines.machines M) 1 |
| 78 | | .jobCount => Counts.module _ M.kernel.jobs |
| 79 | | .processingTimes => ParallelMachines.processingTimes M |
| 80 | | .machineSets => MachineSets.module M |
| 81 | | .releaseDates => ReleaseDates.module _ |
| 82 | | .deadlines => Deadlines.module _ |
| 83 | | .precedence => Precedence.module _ (ParallelMachines.machines M) |
| 84 | | .communicationDelays => CommunicationDelays.module M |
| 85 | | .server => Servers.parallel M |
| 86 | | .forbiddenTimes => ForbiddenTimes.module _ |
| 87 | | .encoding => ForbiddenTimes.encoding _ |
| 88 | |
| 89 | instance (M : ParallelMachines.Model) : Fintype (family M).ModuleName := |
| 90 | inferInstanceAs (Fintype FieldName) |
| 91 | |
| 92 | /-- The specification `α | β | γ` in a machine model. -/ |
| 93 | def spec (M : ParallelMachines.Model) (environment : ParallelMachines.Environment) |
| 94 | (machineCount : Counts.Bound := .any) |
| 95 | (jobCount : Counts.Bound := .any) |
| 96 | (machineSets : MachineSets.Value := .none) |
| 97 | (processingTimes : ParallelMachines.ProcessingTimes := .arbitrary) |
| 98 | (release : ReleaseDates.Value := .none) |
| 99 | (deadline : Deadlines.Value := .none) |
| 100 | (precedence : Precedence.Value := .none) |
| 101 | (communicationDelays : CommunicationDelays.Value := .none) |
| 102 | (server : Servers.Value := .none) |
| 103 | (forbiddenTimes : ForbiddenTimes.Value := .none) |
| 104 | (encoding : ForbiddenTimes.Encoding := .standard) |
| 105 | (objective : Objectives.Value) : Spec (family M) where |
| 106 | module |
| 107 | | .environment => environment |
| 108 | | .machineCount => machineCount |
| 109 | | .jobCount => jobCount |
| 110 | | .processingTimes => processingTimes |
| 111 | | .machineSets => machineSets |
| 112 | | .releaseDates => release |
| 113 | | .deadlines => deadline |
| 114 | | .precedence => precedence |
| 115 | | .communicationDelays => communicationDelays |
| 116 | | .server => server |
| 117 | | .forbiddenTimes => forbiddenTimes |
| 118 | | .encoding => encoding |
| 119 | objective := objective |
| 120 | |
| 121 | /-- The non-preemptive problems. -/ |
| 122 | abbrev nonpreemptive := family Nonpreemptive.model |
| 123 | |
| 124 | /-- The preemptive problems. -/ |
| 125 | abbrev preemptive := family Preemptive.model |
| 126 | |
| 127 | /-- The problems with restarts. -/ |
| 128 | abbrev restarts := family Restarts.model |
| 129 | |
| 130 | /-- `1 || ΣC_j` -/ |
| 131 | def single_sumC : Spec nonpreemptive := |
| 132 | spec _ (environment := .identical) (machineCount := .atMost 1) (objective := .sumC) |
| 133 | |
| 134 | /-- `1 | r_j | ΣC_j` -/ |
| 135 | def single_release_sumC : Spec nonpreemptive := |
| 136 | spec _ (environment := .identical) (machineCount := .atMost 1) (release := .releaseDates) |
| 137 | (objective := .sumC) |
| 138 | |
| 139 | /-- `P | p_j = 1, chains | C_max` -/ |
| 140 | def identical_unit_chains_makespan : Spec nonpreemptive := |
| 141 | spec _ (environment := .identical) (processingTimes := .unit) (precedence := ⟨.chains, .zero⟩) |
| 142 | (objective := .makespan) |
| 143 | |
| 144 | /-- `R | r_j, prec | Σw_jT_j` -/ |
| 145 | def unrelated_release_prec_sumWT : Spec nonpreemptive := |
| 146 | spec _ (environment := .unrelated) (release := .releaseDates) (precedence := ⟨.prec, .zero⟩) |
| 147 | (objective := .sumWT) |
| 148 | |
| 149 | /-- `P | pmtn, r_j | L_max` -/ |
| 150 | def identical_pmtn_release_lmax : Spec preemptive := |
| 151 | spec _ (environment := .identical) (release := .releaseDates) (objective := .lmax) |
| 152 | |
| 153 | axiom family_sound (M : ParallelMachines.Model) : (family M).Sound |
| 154 | |
| 155 | axiom specialCase_of_le (M : ParallelMachines.Model) {s t : Spec (family M)} : |
| 156 | s.le t → SpecialCase (problem (family M) s) (problem (family M) t) |
| 157 | |
| 158 | axiom reducible_of_reduces (M : ParallelMachines.Model) {s t : Spec (family M)} : |
| 159 | Thresholds.Reduces s t → Reducible (problem (family M) s) (problem (family M) t) |
| 160 | |
| 161 | axiom reducible_of_reducesThroughFlow (M : ParallelMachines.Model) |
| 162 | (h : M.kernel.StartsBeforeCompletion) {s t : Spec (family M)} : |
| 163 | Thresholds.ReducesThroughFlow s t → Reducible (problem (family M) s) (problem (family M) t) |
| 164 | |
| 165 | axiom single_sumC_specialCase : |
| 166 | SpecialCase (problem nonpreemptive single_sumC) |
| 167 | (problem nonpreemptive unrelated_release_prec_sumWT) |
| 168 | |
| 169 | end Lax434175.ParallelProblems |
| 170 |
Builds on
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments