Machine sets encoded by long processing times
Lax434175.EncodingsEligibility · concepts/Lax434175/EncodingsEligibility.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
On unrelated machines every processing time is finite, and the problems on unrelated machines have no machine sets. A machine on which job may not run is instead encoded by a processing time too long for every schedule within the threshold. Four relations of the Scheduling Zoo rest on this encoding; each maps an instance with machine sets and threshold to an instance on unrelated machines with the same jobs, machines and times for , and a long time for .
- to and to : the time . A job on a machine outside its set completes after , so a schedule within the threshold uses only the machines of the sets, and it is a schedule of the instance with machine sets of the same cost. A job without a machine in its set makes both instances infeasible within the threshold.
- to : the time again. A job of positive weight on a machine outside its set costs more than ; a job of weight costs nothing anywhere and is moved to the end of a machine of its set. An instance with a job whose set is empty is mapped to a threshold that no schedule meets.
- to : the time , so a job outside its set is never just in time; such jobs are moved to the end of a machine of their set, which makes no just-in-time job late. An instance with a job whose set is empty is mapped to a threshold that no schedule meets.
Theorem. The decision version of each of the four problems with machine sets reduces to that of the problem on unrelated machines, with the same numbers of jobs and machines.
The reduction is computed on the standard words: a program reads the word of an instance with machine sets and its threshold and writes the word of the unrelated instance and its threshold, in polynomial time and with numbers at most one more than those it reads. So hardness goes up along the four relations.
Theorem. Along each of the four relations, NP-hardness and strong NP-hardness on the standard reading go from the problem with machine sets to the problem on unrelated machines, and so does W[t]-hardness for the number of machines.
Concept map
Evidence
This concept declares 16 statements. Each proof establishes one of them relative to its assumptions.
1 machineSets_makespan proven
2 machineSets_sumC proven
3 machineSets_sumWC proven
4 machineSets_sumWZ proven
5 npHard_makespan proven
6 npHard_sumC proven
7 npHard_sumWC proven
8 npHard_sumWZ proven
9 stronglyNPHard_makespan proven
10 stronglyNPHard_sumC proven
11 stronglyNPHard_sumWC proven
12 stronglyNPHard_sumWZ proven
13 wHard_m_makespan proven
14 wHard_m_sumC proven
15 wHard_m_sumWC proven
Lean source view on GitHub
| 1 | import Lax434175.ZooParallel |
| 2 | import Lax434175.Parameters |
| 3 | import Lax434175.StandardReading |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Machine sets encoded by long processing times |
| 8 | type: theorem |
| 9 | --- |
| 10 | On unrelated machines every processing time is finite, and the problems on |
| 11 | unrelated machines have no machine sets. A machine on which job may not run is instead encoded by a |
| 12 | processing time too long for every schedule within the threshold. Four |
| 13 | relations of the Scheduling Zoo rest on this encoding; each maps an instance |
| 14 | with machine sets and threshold to an instance on unrelated machines |
| 15 | with the same jobs, machines and times for , and a long |
| 16 | time for . |
| 17 | |
| 18 | - to and |
| 19 | to : the time . A job |
| 20 | on a machine outside its set completes after , so a schedule within the |
| 21 | threshold uses only the machines of the sets, and it is a schedule of the |
| 22 | instance with machine sets of the same cost. A job without a machine in its |
| 23 | set makes both instances infeasible within the threshold. |
| 24 | - to : the time |
| 25 | again. A job of positive weight on a machine outside its set costs |
| 26 | more than ; a job of weight costs nothing anywhere and is moved to |
| 27 | the end of a machine of its set. An instance with a job whose set is empty |
| 28 | is mapped to a threshold that no schedule meets. |
| 29 | - to : the time |
| 30 | , so a job outside its set is never just in time; such jobs are |
| 31 | moved to the end of a machine of their set, which makes no just-in-time job |
| 32 | late. An instance with a job whose set is empty is mapped to a threshold |
| 33 | that no schedule meets. |
| 34 | |
| 35 | **Theorem.** The decision version of each of the four problems with machine |
| 36 | sets reduces to that of the problem on unrelated machines, with the same |
| 37 | numbers of jobs and machines. |
| 38 | |
| 39 | The reduction is computed on the standard words: a program reads the word of an |
| 40 | instance with machine sets and its threshold and writes the word of the |
| 41 | unrelated instance and its threshold, in polynomial time and with numbers at |
| 42 | most one more than those it reads. So hardness goes up along the four |
| 43 | relations. |
| 44 | |
| 45 | **Theorem.** Along each of the four relations, NP-hardness and strong |
| 46 | NP-hardness on the standard reading go from the problem with machine sets to the |
| 47 | problem on unrelated machines, and so does W[t]-hardness for the number of |
| 48 | machines. |
| 49 | -/ |
| 50 | |
| 51 | namespace Lax434175.EncodingsEligibility |
| 52 | open Lax434175 Lax434175.Problems Lax434175.Assembly Lax434175.Parameters |
| 53 | |
| 54 | /-- The numbers of jobs and machines of an instance. -/ |
| 55 | def size {s : Spec OperationsFamily.family} (x : Inst OperationsFamily.family s) : ℕ × ℕ := |
| 56 | (x.base.jobs, x.base.machines) |
| 57 | |
| 58 | /-- `P|Mj|Cmax` reduces to `R||Cmax`. -/ |
| 59 | axiom machineSets_makespan : |
| 60 | ReducibleWith (A := problem _ ZooParallel.p107) (B := problem _ ZooParallel.p5) size size |
| 61 | (fun a b => b = a) |
| 62 | |
| 63 | /-- `Q|Mj|ΣCj` reduces to `R||ΣCj`. -/ |
| 64 | axiom machineSets_sumC : |
| 65 | ReducibleWith (A := problem _ ZooParallel.p33) (B := problem _ ZooParallel.p31) size size |
| 66 | (fun a b => b = a) |
| 67 | |
| 68 | /-- `P|Mj|ΣwjCj` reduces to `R||ΣwjCj`. -/ |
| 69 | axiom machineSets_sumWC : |
| 70 | ReducibleWith (A := problem _ ZooParallel.p130) (B := problem _ ZooParallel.p222) size size |
| 71 | (fun a b => b = a) |
| 72 | |
| 73 | /-- `P|Mj|ΣwjZj` reduces to `R||ΣwjZj`. -/ |
| 74 | axiom machineSets_sumWZ : |
| 75 | ReducibleWith (A := problem _ ZooParallel.p200) (B := problem _ ZooParallel.p208) size size |
| 76 | (fun a b => b = a) |
| 77 | |
| 78 | open Lax434175.Results Lax434175.ResultParameters |
| 79 | |
| 80 | /-- NP-hardness goes up along `P|Mj|Cmax → R||Cmax`. -/ |
| 81 | axiom npHard_makespan : |
| 82 | NPHard (StandardReading.ops.at ZooParallel.p107) → NPHard (StandardReading.ops.at ZooParallel.p5) |
| 83 | |
| 84 | /-- NP-hardness goes up along `Q|Mj|ΣCj → R||ΣCj`. -/ |
| 85 | axiom npHard_sumC : |
| 86 | NPHard (StandardReading.ops.at ZooParallel.p33) → NPHard (StandardReading.ops.at ZooParallel.p31) |
| 87 | |
| 88 | /-- NP-hardness goes up along `P|Mj|ΣwjCj → R||ΣwjCj`. -/ |
| 89 | axiom npHard_sumWC : |
| 90 | NPHard (StandardReading.ops.at ZooParallel.p130) → NPHard (StandardReading.ops.at ZooParallel.p222) |
| 91 | |
| 92 | /-- NP-hardness goes up along `P|Mj|ΣwjZj → R||ΣwjZj`. -/ |
| 93 | axiom npHard_sumWZ : |
| 94 | NPHard (StandardReading.ops.at ZooParallel.p200) → NPHard (StandardReading.ops.at ZooParallel.p208) |
| 95 | |
| 96 | /-- Strong NP-hardness goes up along `P|Mj|Cmax → R||Cmax`. -/ |
| 97 | axiom stronglyNPHard_makespan : |
| 98 | StronglyNPHard (StandardReading.ops.at ZooParallel.p107) → |
| 99 | StronglyNPHard (StandardReading.ops.at ZooParallel.p5) |
| 100 | |
| 101 | /-- Strong NP-hardness goes up along `Q|Mj|ΣCj → R||ΣCj`. -/ |
| 102 | axiom stronglyNPHard_sumC : |
| 103 | StronglyNPHard (StandardReading.ops.at ZooParallel.p33) → |
| 104 | StronglyNPHard (StandardReading.ops.at ZooParallel.p31) |
| 105 | |
| 106 | /-- Strong NP-hardness goes up along `P|Mj|ΣwjCj → R||ΣwjCj`. -/ |
| 107 | axiom stronglyNPHard_sumWC : |
| 108 | StronglyNPHard (StandardReading.ops.at ZooParallel.p130) → |
| 109 | StronglyNPHard (StandardReading.ops.at ZooParallel.p222) |
| 110 | |
| 111 | /-- Strong NP-hardness goes up along `P|Mj|ΣwjZj → R||ΣwjZj`. -/ |
| 112 | axiom stronglyNPHard_sumWZ : |
| 113 | StronglyNPHard (StandardReading.ops.at ZooParallel.p200) → |
| 114 | StronglyNPHard (StandardReading.ops.at ZooParallel.p208) |
| 115 | |
| 116 | /-- W[t]-hardness for the number of machines goes up along `P|Mj|Cmax → R||Cmax`. -/ |
| 117 | axiom wHard_m_makespan (t : ℕ) : |
| 118 | WHard (StandardReading.ops.at ZooParallel.p107) t (lift (Ops.m ZooParallel.p107)) → |
| 119 | WHard (StandardReading.ops.at ZooParallel.p5) t (lift (Ops.m ZooParallel.p5)) |
| 120 | |
| 121 | /-- W[t]-hardness for the number of machines goes up along `Q|Mj|ΣCj → R||ΣCj`. -/ |
| 122 | axiom wHard_m_sumC (t : ℕ) : |
| 123 | WHard (StandardReading.ops.at ZooParallel.p33) t (lift (Ops.m ZooParallel.p33)) → |
| 124 | WHard (StandardReading.ops.at ZooParallel.p31) t (lift (Ops.m ZooParallel.p31)) |
| 125 | |
| 126 | /-- W[t]-hardness for the number of machines goes up along `P|Mj|ΣwjCj → R||ΣwjCj`. -/ |
| 127 | axiom wHard_m_sumWC (t : ℕ) : |
| 128 | WHard (StandardReading.ops.at ZooParallel.p130) t (lift (Ops.m ZooParallel.p130)) → |
| 129 | WHard (StandardReading.ops.at ZooParallel.p222) t (lift (Ops.m ZooParallel.p222)) |
| 130 | |
| 131 | /-- W[t]-hardness for the number of machines goes up along `P|Mj|ΣwjZj → R||ΣwjZj`. -/ |
| 132 | axiom wHard_m_sumWZ (t : ℕ) : |
| 133 | WHard (StandardReading.ops.at ZooParallel.p200) t (lift (Ops.m ZooParallel.p200)) → |
| 134 | WHard (StandardReading.ops.at ZooParallel.p208) t (lift (Ops.m ZooParallel.p208)) |
| 135 | |
| 136 | end Lax434175.EncodingsEligibility |
| 137 |
Used by
none
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments