The standard reading of scheduling instances and schedules
Lax434175.StandardReading · concepts/Lax434175/StandardReading.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
The words in which the literature writes scheduling instances, schedules and online information, for the operations family, the batching family and the two standalone problems. All numbers are written in binary, as entries of the word.
Blocks. A finite set of tuples of numbers is written canonically: the number of tuples, then every tuple, preceded by its length, in increasing lexicographic order and without repetition.
Instances of the operations family. A field is written by its view, the meaning its constraints use, and not by its internal representation, so that two representations of the same constraints have the same word. The word consists of
- a flag, for the standard encoding and for high multiplicity, the number of jobs and the number of machines;
- for every job a record, preceded by its length: its number of operations, the processing time of every operation on every machine, its deadline ( for none, or followed by the deadline), and three blocks: the sets of machines each operation may occupy, the setup time of each operation at the server, and the transport delays between its operations; and its batch for batch setups;
- a block of the facts on pairs of jobs: when precedes , for the lag of such a pair ( for a negative lag), and when the pair has communication delay ;
- a block of the global facts: for every forbidden time, for the setup time from batch to batch , for the batches of jobs, and, when the problem has a transport robot, for the empty moving time of the robot from machine to machine , for all machines (all when the robot has no empty moves);
- for every job its release date, weight and due date ( and when the objective has none), three numbers each, in the order of the jobs.
The release dates, weights and due dates come last so that changing the objective — which the threshold steps between objectives do — rewrites only the end of the word. With high multiplicity the jobs are written as a block of their distinct records, each followed by the job's release date, weight and due date and preceded by the number of jobs that have both, and there are no facts on pairs.
Instances of batching: the number of jobs, the setup time and the capacity, then for every job its processing time, release date, weight, due date, deadline and size, then the block of precedence pairs, each with its lag. Rejection: the number of jobs and the budget, then the processing time and rejection cost of every job. Machine covering: the numbers of jobs and machines and the processing times.
Schedules. A schedule of the operations family is the list of its pieces, each written as its job, operation, start and length (a rational as numerator and reduced denominator) and the sorted machines it occupies. With high multiplicity a schedule is written compactly, by machine patterns: a list of groups, each a number of machines followed by the pieces every one of them runs, a piece written as the type of its job (the position of the job's tuple in the block of distinct records), its operation, start and length. The groups use consecutive machines, for a group, and the -th piece of a type and an operation goes to the -th job of that type, in the order of the jobs; every operation is one piece. A batch schedule writes for every job its batch and the start and processing time of that batch; a rejection schedule for every job whether it is accepted and its start; a covering the machine of every job.
Online. For problems whose jobs arrive online, the scheduler sees at time the records of the jobs released by (with their numbers), the facts on pairs of them, and the global facts; two schedules made the same decisions up to if they have the same pieces starting before . Other problems are revealed at once.
Concept map
Lean source view on GitHub
| 1 | import Lax434175.Results |
| 2 | import Lax434175.ResultParameters |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: The standard reading of scheduling instances and schedules |
| 7 | type: definition |
| 8 | --- |
| 9 | The words in which the literature writes scheduling instances, schedules and |
| 10 | online information, for the operations family, the batching family and the two |
| 11 | standalone problems. All numbers are written in binary, as entries of the word. |
| 12 | |
| 13 | **Blocks.** A finite set of tuples of numbers is written canonically: the |
| 14 | number of tuples, then every tuple, preceded by its length, in increasing |
| 15 | lexicographic order and without repetition. |
| 16 | |
| 17 | **Instances of the operations family.** A field is written by its *view*, the |
| 18 | meaning its constraints use, and not by its internal representation, so that |
| 19 | two representations of the same constraints have the same word. The word |
| 20 | consists of |
| 21 | |
| 22 | - a flag, `0` for the standard encoding and `1` for high multiplicity, the number |
| 23 | of jobs and the number of machines; |
| 24 | - for every job a record, preceded by its length: its number of operations, the |
| 25 | processing time of every operation on every machine, its deadline (`0` for |
| 26 | none, or `1` followed by the deadline), and three blocks: the sets of machines |
| 27 | each operation may occupy, the setup time of each operation at the server, and |
| 28 | the transport delays between its operations; and its batch for batch setups; |
| 29 | - a block of the facts on pairs of jobs: `(0, i, j)` when `i` precedes `j`, |
| 30 | `(1, i, j, s, l)` for the lag `±l` of such a pair (`s = 1` for a negative lag), |
| 31 | and `(2, i, j, c)` when the pair has communication delay `c`; |
| 32 | - a block of the global facts: `(0, t)` for every forbidden time, |
| 33 | `(1, a, b, s)` for the setup time `s` from batch `a` to batch `b`, for the |
| 34 | batches of jobs, and, when the problem has a transport robot, `(2, i, i', t)` |
| 35 | for the empty moving time `t` of the robot from machine `i` to machine `i'`, |
| 36 | for all machines (all `0` when the robot has no empty moves); |
| 37 | - for every job its release date, weight and due date (`1` and `0` when the |
| 38 | objective has none), three numbers each, in the order of the jobs. |
| 39 | |
| 40 | The release dates, weights and due dates come last so that changing the |
| 41 | objective — which the threshold steps between objectives do — rewrites only the |
| 42 | end of the word. With high multiplicity the jobs are written as a block of their |
| 43 | distinct records, each followed by the job's release date, weight and due date and |
| 44 | preceded by the number of jobs that have both, and there are no facts on pairs. |
| 45 | |
| 46 | **Instances of batching**: the number of jobs, the setup time and the capacity, |
| 47 | then for every job its processing time, release date, weight, due date, deadline |
| 48 | and size, then the block of precedence pairs, each with its lag. **Rejection**: the number of jobs |
| 49 | and the budget, then the processing time and rejection cost of every job. |
| 50 | **Machine covering**: the numbers of jobs and machines and the processing times. |
| 51 | |
| 52 | **Schedules.** A schedule of the operations family is the list of its pieces, |
| 53 | each written as its job, operation, start and length (a rational as numerator |
| 54 | and reduced denominator) and the sorted machines it occupies. With high |
| 55 | multiplicity a schedule is written compactly, by *machine patterns*: a list of |
| 56 | groups, each a number of machines followed by the pieces every one of them |
| 57 | runs, a piece written as the type of its job (the position of the job's tuple in |
| 58 | the block of distinct records), its operation, start and length. The groups use |
| 59 | consecutive machines, for a group, and the -th piece of a type and an |
| 60 | operation goes to the -th job of that type, in the order of the jobs; every |
| 61 | operation is one piece. A batch schedule |
| 62 | writes for every job its batch and the start and processing time of that batch; |
| 63 | a rejection schedule for every job whether it is accepted and its start; a |
| 64 | covering the machine of every job. |
| 65 | |
| 66 | **Online.** For problems whose jobs arrive online, the scheduler sees at time |
| 67 | the records of the jobs released by (with their numbers), the facts on pairs |
| 68 | of them, and the global facts; two schedules made the same decisions up to if |
| 69 | they have the same pieces starting before . Other problems are revealed at |
| 70 | once. |
| 71 | -/ |
| 72 | |
| 73 | namespace Lax434175.StandardReading |
| 74 | open Lax434175 Lax434175.Problems Lax434175.Assembly Lax434175.Results |
| 75 | open Lax434175.ResultParameters |
| 76 | |
| 77 | -- Blocks |
| 78 | |
| 79 | /-- The list writes the set: increasing, without repetition, and with the same |
| 80 | elements. -/ |
| 81 | def Lists (S : Set (List ℕ)) (L : List (List ℕ)) : Prop := |
| 82 | L.Pairwise (· < ·) ∧ ∀ t, t ∈ L ↔ t ∈ S |
| 83 | |
| 84 | /-- A list of tuples, each preceded by its length, after their number. -/ |
| 85 | def flat (L : List (List ℕ)) : List ℕ := L.length :: L.flatMap fun t => t.length :: t |
| 86 | |
| 87 | /-- The word is the canonical block of the set. -/ |
| 88 | def Block (S : Set (List ℕ)) (b : List ℕ) : Prop := ∃ L, Lists S L ∧ b = flat L |
| 89 | |
| 90 | /-- An integer as sign and absolute value. -/ |
| 91 | def int (z : ℤ) : List ℕ := [if z < 0 then 1 else 0, z.natAbs] |
| 92 | |
| 93 | /-- A deadline: `0` for none, `1` and the value otherwise. -/ |
| 94 | def enat (e : ℕ∞) : List ℕ := if e = ⊤ then [0] else [1, e.toNat] |
| 95 | |
| 96 | /-- A rational as numerator and denominator. -/ |
| 97 | def rat (q : NNRat) : List ℕ := [q.num, q.den] |
| 98 | |
| 99 | /-- A set of machines, sorted. -/ |
| 100 | def machinesWord {m : ℕ} (S : Finset (Fin m)) : List ℕ := |
| 101 | (S.image Fin.val).sort (· ≤ ·) |
| 102 | |
| 103 | -- The operations family |
| 104 | |
| 105 | section Ops |
| 106 | |
| 107 | variable {s : Spec OperationsFamily.family} (x : Inst OperationsFamily.family s) |
| 108 | |
| 109 | /-- The fixed part of the record of a job. -/ |
| 110 | def jobHead (j : Fin x.base.jobs) : List ℕ := |
| 111 | [x.base.ops j] ++ |
| 112 | (List.ofFn fun k : Fin (x.base.ops j) => List.ofFn fun i => x.base.p j k i).flatten ++ |
| 113 | enat (Deadlines.view (K := Operations.kernel) (s.module .deadlines) (x.data .deadlines) j) |
| 114 | |
| 115 | /-- The release date, weight and due date of a job. -/ |
| 116 | def objOf (j : Fin x.base.jobs) : List ℕ := [x.base.r j, Ops.weight s x j, Ops.due s x j] |
| 117 | |
| 118 | /-- The release dates, weights and due dates of all jobs, three numbers each. -/ |
| 119 | def objWord : List ℕ := (List.ofFn (objOf x)).flatten |
| 120 | |
| 121 | /-- The machines an operation of the job may occupy. -/ |
| 122 | def machineTuples (j : Fin x.base.jobs) : Set (List ℕ) := |
| 123 | {t | ∃ (k : Fin (x.base.ops j)) (S : Finset (Fin x.base.machines)), |
| 124 | Operations.Machines.view (s.module .machineSets) |
| 125 | (x.data .machineSets : Operations.Machines.Data _ x.base) ⟨j, k⟩ S ∧ |
| 126 | t = k.val :: machinesWord S} |
| 127 | |
| 128 | /-- The setup times of the operations of the job at the server. -/ |
| 129 | def serverTuples (j : Fin x.base.jobs) : Set (List ℕ) := |
| 130 | {t | ∃ (k : Fin (x.base.ops j)) (f : Operations.Op x.base → ℕ), |
| 131 | Servers.view (s.module .server) (x.data .server : Servers.Data (Operations.Op x.base) _) = |
| 132 | some f ∧ t = [k.val, f ⟨j, k⟩]} |
| 133 | |
| 134 | /-- The transport delays between the operations of the job. -/ |
| 135 | def transportTuples (j : Fin x.base.jobs) : Set (List ℕ) := |
| 136 | {t | ∃ k k' : Fin (x.base.ops j), |
| 137 | t = [k.val, k'.val, (x.data .transportation : Transportation.Data x.base.toShop).1 j k k']} |
| 138 | |
| 139 | /-- The batch of the job for batch setups. -/ |
| 140 | def batchOf (j : Fin x.base.jobs) : ℕ := |
| 141 | ShopExtras.BatchSetups.batch (x := x.base.toShop) (s.module .batchSetups) |
| 142 | (x.data .batchSetups) j |
| 143 | |
| 144 | /-- The word is the record of the job. -/ |
| 145 | def Record (j : Fin x.base.jobs) (b : List ℕ) : Prop := |
| 146 | ∃ b₁ b₂ b₃, Block (machineTuples x j) b₁ ∧ Block (serverTuples x j) b₂ ∧ |
| 147 | Block (transportTuples x j) b₃ ∧ b = jobHead x j ++ b₁ ++ b₂ ++ b₃ ++ [batchOf x j] |
| 148 | |
| 149 | /-- The facts on pairs of jobs. -/ |
| 150 | def pairTuples : Set (List ℕ) := |
| 151 | {t | ∃ i j : Fin x.base.jobs, Ops.prec s x i j ∧ t = [0, i.val, j.val]} ∪ |
| 152 | {t | ∃ i j : Fin x.base.jobs, Ops.prec s x i j ∧ |
| 153 | t = [1, i.val, j.val] ++ int ((s.module .precedence).lags.view (x.data .precedence).2 i j)} ∪ |
| 154 | {t | ∃ (i j : Fin x.base.jobs) (c : ℕ), CommunicationDelays.view (s.module .communicationDelays) |
| 155 | (x.data .communicationDelays : CommunicationDelays.Data _ x.base.toPar) i j c ∧ |
| 156 | t = [2, i.val, j.val, c]} |
| 157 | |
| 158 | /-- The global facts. -/ |
| 159 | def globalTuples : Set (List ℕ) := |
| 160 | {t | ∃ τ ∈ ForbiddenTimes.view (s.module .forbiddenTimes) (x.data .forbiddenTimes), t = [0, τ]} ∪ |
| 161 | {t | ∃ i j : Fin x.base.jobs, t = [1, batchOf x i, batchOf x j, |
| 162 | ShopExtras.BatchSetups.setup (x := x.base.toShop) (s.module .batchSetups) |
| 163 | (x.data .batchSetups) (batchOf x i) (batchOf x j)]} ∪ |
| 164 | {t | (s.module .transportation).robot = true ∧ ∃ i i' : Fin x.base.machines, |
| 165 | t = [2, i.val, i'.val, (x.data .transportation : Transportation.Data x.base.toShop).2 i i']} |
| 166 | |
| 167 | /-- The records of all jobs, in order, each preceded by its length. -/ |
| 168 | def Records (b : List ℕ) : Prop := |
| 169 | ∃ R : Fin x.base.jobs → List ℕ, (∀ j, Record x j (R j)) ∧ |
| 170 | b = (List.ofFn fun j => (R j).length :: R j).flatten |
| 171 | |
| 172 | /-- The distinct records, each with the number of jobs that have it. -/ |
| 173 | noncomputable def typeTuples : Set (List ℕ) := |
| 174 | {t | ∃ b j, Record x j b ∧ |
| 175 | t = Nat.card {j' // Record x j' b ∧ objOf x j' = objOf x j} :: (b ++ objOf x j)} |
| 176 | |
| 177 | /-- The word of an instance of the operations family. -/ |
| 178 | def EncodesOps (w : List ℕ) : Prop := |
| 179 | ∃ b₂ b₃, Block (pairTuples x) b₂ ∧ Block (globalTuples x) b₃ ∧ |
| 180 | ((s.module .encoding = .standard ∧ ∃ b₁, Records x b₁ ∧ |
| 181 | w = [0, x.base.jobs, x.base.machines] ++ b₁ ++ b₂ ++ b₃ ++ objWord x) ∨ |
| 182 | (s.module .encoding = .highMultiplicity ∧ pairTuples x = ∅ ∧ ∃ b₁, Block (typeTuples x) b₁ ∧ |
| 183 | w = [1, x.base.jobs, x.base.machines] ++ b₁ ++ b₂ ++ b₃)) |
| 184 | |
| 185 | /-- The word of a piece of a schedule. -/ |
| 186 | def pieceWord (q : Operations.Piece x.base) : List ℕ := |
| 187 | [q.op.1.val, q.op.2.val] ++ rat q.start ++ rat q.length ++ machinesWord q.machines |
| 188 | |
| 189 | /-- The word of a schedule: its pieces in order. -/ |
| 190 | def schedWord (σ : Operations.Sched x.base) : List ℕ := flat (σ.pieces.map (pieceWord x)) |
| 191 | |
| 192 | /-- The type of a job in a high-multiplicity word: the position of its tuple in |
| 193 | the canonical list of the distinct records. -/ |
| 194 | def TypeIndex (j : Fin x.base.jobs) (t : ℕ) : Prop := |
| 195 | ∃ L b, Lists (typeTuples x) L ∧ Record x j b ∧ |
| 196 | L[t]? = some (Nat.card {j' // Record x j' b ∧ objOf x j' = objOf x j} :: (b ++ objOf x j)) |
| 197 | |
| 198 | end Ops |
| 199 | |
| 200 | /-- A piece of a machine pattern: the type of its job, its operation, start and |
| 201 | length. -/ |
| 202 | structure Slot where |
| 203 | type : ℕ |
| 204 | op : ℕ |
| 205 | start : NNRat |
| 206 | length : NNRat |
| 207 | |
| 208 | /-- A group of a compact schedule: a number of machines and the pieces each of |
| 209 | them runs. -/ |
| 210 | abbrev Group := ℕ × List Slot |
| 211 | |
| 212 | /-- The word of a group. -/ |
| 213 | def groupWord (g : Group) : List ℕ := |
| 214 | g.1 :: flat (g.2.map fun q => [q.type, q.op] ++ rat q.start ++ rat q.length) |
| 215 | |
| 216 | /-- The word of a compact schedule. -/ |
| 217 | def compactWord (G : List Group) : List ℕ := flat (G.map groupWord) |
| 218 | |
| 219 | /-- The pieces of a compact schedule with their machines, the groups using |
| 220 | consecutive machines from `base` on. -/ |
| 221 | def expand : List Group → ℕ → List (ℕ × Slot) |
| 222 | | [], _ => [] |
| 223 | | (c, P) :: G, base => |
| 224 | (List.range c).flatMap (fun k => P.map fun q => (base + k, q)) ++ expand G (base + c) |
| 225 | |
| 226 | section Ops |
| 227 | |
| 228 | variable {s : Spec OperationsFamily.family} (x : Inst OperationsFamily.family s) |
| 229 | |
| 230 | /-- The schedule is the one the compact schedule writes: piece by piece the same |
| 231 | machine, operation, start and length, a job of the slot's type, and the `k`-th |
| 232 | slot of a type and an operation for the `k`-th job of that type. -/ |
| 233 | def ExpandsTo (G : List Group) (σ : Operations.Sched x.base) : Prop := |
| 234 | σ.pieces.length = (expand G 0).length ∧ |
| 235 | ∀ (n : ℕ) (hσ : n < σ.pieces.length) (hG : n < (expand G 0).length), |
| 236 | (σ.pieces[n].machines.image Fin.val = {((expand G 0)[n]).1}) ∧ |
| 237 | σ.pieces[n].op.2.val = ((expand G 0)[n]).2.op ∧ |
| 238 | σ.pieces[n].start = ((expand G 0)[n]).2.start ∧ |
| 239 | σ.pieces[n].length = ((expand G 0)[n]).2.length ∧ |
| 240 | TypeIndex x σ.pieces[n].op.1 ((expand G 0)[n]).2.type ∧ |
| 241 | Nat.card {j : Fin x.base.jobs // j < σ.pieces[n].op.1 ∧ TypeIndex x j ((expand G 0)[n]).2.type} = |
| 242 | ((expand G 0).take n).countP fun b => |
| 243 | b.2.type == ((expand G 0)[n]).2.type && b.2.op == ((expand G 0)[n]).2.op |
| 244 | |
| 245 | /-- What is revealed at time `t`: the records of the jobs released by `t` with |
| 246 | their numbers, the facts on pairs of them, and the global facts. -/ |
| 247 | def RevealedOps (t : NNRat) (w : List ℕ) : Prop := |
| 248 | ∃ (R : Fin x.base.jobs → List ℕ) (b₂ b₃ : List ℕ), (∀ j, Record x j (R j)) ∧ |
| 249 | Block {u ∈ pairTuples x | ∀ v ∈ u.drop 1 |>.take 2, |
| 250 | ∃ j : Fin x.base.jobs, j.val = v ∧ (x.base.r j : NNRat) ≤ t} b₂ ∧ |
| 251 | Block (globalTuples x) b₃ ∧ |
| 252 | w = [x.base.machines] ++ ((List.ofFn fun j => (j, R j)).filter fun p => |
| 253 | decide ((x.base.r p.1 : NNRat) ≤ t)).flatMap |
| 254 | (fun p => p.1.val :: p.2.length :: (p.2 ++ objOf x p.1)) ++ |
| 255 | b₂ ++ b₃ |
| 256 | |
| 257 | end Ops |
| 258 | |
| 259 | open Classical in |
| 260 | /-- The standard reading of the operations family. -/ |
| 261 | noncomputable def ops : Reading OperationsFamily.family where |
| 262 | Encodes _ w x := EncodesOps x w |
| 263 | Decodes s x w σ := if s.module .encoding = .highMultiplicity then |
| 264 | ∃ G, w = compactWord G ∧ ExpandsTo x G σ else w = schedWord x σ |
| 265 | reveal s := |
| 266 | { same := fun x y t => |
| 267 | if s.module .releaseDates = .online then ∀ w, RevealedOps x t w ↔ RevealedOps y t w |
| 268 | else ∀ w, EncodesOps x w ↔ EncodesOps y w |
| 269 | agree := fun x y σ τ t => |
| 270 | flat ((σ.pieces.filter fun q => decide (q.start < t)).map (pieceWord x)) = |
| 271 | flat ((τ.pieces.filter fun q => decide (q.start < t)).map (pieceWord y)) } |
| 272 | |
| 273 | -- The batching family |
| 274 | |
| 275 | section Batch |
| 276 | |
| 277 | variable {s : Spec BatchFamily.family} (x : Inst BatchFamily.family s) |
| 278 | |
| 279 | /-- The record of a job. -/ |
| 280 | def batchRecord (j : Fin x.base.jobs) : List ℕ := |
| 281 | [x.base.p j, x.base.r j, Batch.weight s x j, |
| 282 | Objectives.dueDate (K := BatchFamily.kernel) s.objective x.objectiveData j] ++ |
| 283 | enat (Deadlines.view (K := BatchFamily.kernel) (s.module (.field .deadlines)) |
| 284 | (x.data (.field .deadlines)) j) ++ |
| 285 | [Batching.Capacity.size (x := x.base) (s.module (.field .capacity)) (x.data (.field .capacity)) j] |
| 286 | |
| 287 | /-- The precedence pairs, each with its lag. -/ |
| 288 | def batchPairs : Set (List ℕ) := |
| 289 | {t | ∃ i j : Fin x.base.jobs, |
| 290 | (s.module (.field .precedence)).order.view (x.data (.field .precedence)).1 i j ∧ |
| 291 | t = [i.val, j.val] ++ int ((s.module (.field .precedence)).lags.view (x.data (.field .precedence)).2 i j)} |
| 292 | |
| 293 | /-- The word of a batching instance. -/ |
| 294 | def EncodesBatch (w : List ℕ) : Prop := |
| 295 | ∃ b, Block (batchPairs x) b ∧ |
| 296 | w = [x.base.jobs, x.base.setup, |
| 297 | Batching.Capacity.bound (x := x.base) (s.module (.field .capacity)) (x.data (.field .capacity))] ++ |
| 298 | (List.ofFn fun j => batchRecord x j).flatten ++ b |
| 299 | |
| 300 | /-- The word of a batch schedule: for every job its batch and that batch's start |
| 301 | and processing time. -/ |
| 302 | def batchSchedWord (σ : BatchFamily.Sched x.base) : List ℕ := |
| 303 | (List.ofFn fun j => [σ.batch j, σ.start (σ.batch j), σ.length (σ.batch j)]).flatten |
| 304 | |
| 305 | end Batch |
| 306 | |
| 307 | /-- The standard reading of the batching family. -/ |
| 308 | noncomputable def batch : Reading BatchFamily.family where |
| 309 | Encodes _ w x := EncodesBatch x w |
| 310 | Decodes _ x w σ := w = batchSchedWord x σ |
| 311 | reveal _ := |
| 312 | { same := fun x y _ => ∀ w, EncodesBatch x w ↔ EncodesBatch y w |
| 313 | agree := fun x y σ τ _ => batchSchedWord x σ = batchSchedWord y τ } |
| 314 | |
| 315 | -- The standalone problems |
| 316 | |
| 317 | /-- The standard reading of single-machine scheduling with rejection. -/ |
| 318 | noncomputable def rejection : PReading Rejection.problem where |
| 319 | Encodes w x := w = [x.jobs, x.budget] ++ (List.ofFn fun j => [x.p j, x.e j]).flatten |
| 320 | Decodes _ w σ := w = (List.ofFn fun j => |
| 321 | [if j ∈ σ.accepted then 1 else 0, σ.start j]).flatten |
| 322 | reveal := |
| 323 | { same := fun x y _ => x = y |
| 324 | agree := fun _ _ _ _ _ => True } |
| 325 | |
| 326 | /-- The standard reading of machine covering. -/ |
| 327 | def covering : PReading MachineCovering.problem where |
| 328 | Encodes w x := w = [x.jobs, x.machines] ++ List.ofFn x.p |
| 329 | Decodes _ w σ := w = List.ofFn fun j => (σ j).val |
| 330 | reveal := |
| 331 | { same := fun x y _ => x = y |
| 332 | agree := fun _ _ _ _ _ => True } |
| 333 | |
| 334 | end Lax434175.StandardReading |
| 335 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments