Standard words into high-multiplicity words
Lax434175.HighMultiplicity · concepts/Lax434175/HighMultiplicity.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
A high-multiplicity word lists every distinct job once, with its record, release date, weight and due date, preceded by the number of jobs that have them (). It does not say which job is which, and it has no facts on pairs of jobs.
Theorem. The standard reading determines the answer for every specification with high multiplicity. Two instances written by one high-multiplicity word have the same numbers of jobs and machines and the same global facts, and a bijection between their jobs keeps every record, release date, weight and due date; renaming the jobs along it maps the feasible schedules of one instance to those of the other, at the same cost.
A program reads the standard word of an instance without facts on pairs of jobs and writes the high-multiplicity word of the same instance: for every job it counts the jobs with the same record, release date, weight and due date, and it writes the distinct tuples in increasing order. It runs in polynomial time on every word.
Theorem. Let , where has the standard encoding, no precedence constraints and no communication delays, and has high multiplicity. Then NP-hardness goes up from to , and so does W[t]-hardness for parameters of and of , if on every instance written by a high-multiplicity word of the lift of an instance of , is at most a computable function of . Being in P goes down from to , and so does fixed-parameter tractability under the same bound, for a parameter of computable in polynomial time.
Strong NP-hardness is not carried: a high-multiplicity word can be much shorter than the standard word of the same instance, so numbers that are small for the standard word can be large for the high-multiplicity word.
Theorem. Along , NP-hardness and W[t]-hardness for the number of machines go up, and fixed-parameter tractability for the number of distinct processing times goes down. Here the number of distinct processing times of is computed in polynomial time by writing the high-multiplicity word and computing it there, which fixed-parameter tractability of includes.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax434175.Propagation |
| 2 | import Lax434175.ZooParallel |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Standard words into high-multiplicity words |
| 7 | type: theorem |
| 8 | --- |
| 9 | A high-multiplicity word lists every distinct job once, with its record, release |
| 10 | date, weight and due date, preceded by the number of jobs that have them |
| 11 | (`StandardReading`). It does not say which job is which, and it has no facts on |
| 12 | pairs of jobs. |
| 13 | |
| 14 | **Theorem.** The standard reading determines the answer for every specification |
| 15 | with high multiplicity. Two instances written by one high-multiplicity word have |
| 16 | the same numbers of jobs and machines and the same global facts, and a bijection |
| 17 | between their jobs keeps every record, release date, weight and due date; |
| 18 | renaming the jobs along it maps the feasible schedules of one instance to those |
| 19 | of the other, at the same cost. |
| 20 | |
| 21 | A program reads the standard word of an instance without facts on pairs of jobs |
| 22 | and writes the high-multiplicity word of the same instance: for every job it |
| 23 | counts the jobs with the same record, release date, weight and due date, and it |
| 24 | writes the distinct tuples in increasing order. It runs in polynomial time on |
| 25 | every word. |
| 26 | |
| 27 | **Theorem.** Let , where has the standard encoding, no precedence |
| 28 | constraints and no communication delays, and has high multiplicity. Then |
| 29 | NP-hardness goes up from to , and so does W[t]-hardness for parameters |
| 30 | of and of , if on every instance written by a |
| 31 | high-multiplicity word of the lift of an instance of , is at |
| 32 | most a computable function of . Being in P goes down from to |
| 33 | , and so does fixed-parameter tractability under the same bound, for a |
| 34 | parameter of computable in polynomial time. |
| 35 | |
| 36 | Strong NP-hardness is not carried: a high-multiplicity word can be much shorter |
| 37 | than the standard word of the same instance, so numbers that are small for the |
| 38 | standard word can be large for the high-multiplicity word. |
| 39 | |
| 40 | **Theorem.** Along , NP-hardness |
| 41 | and W[t]-hardness for the number of machines go up, and fixed-parameter |
| 42 | tractability for the number of distinct processing times goes down. Here the |
| 43 | number of distinct processing times of is computed in |
| 44 | polynomial time by writing the high-multiplicity word and computing it there, |
| 45 | which fixed-parameter tractability of includes. |
| 46 | -/ |
| 47 | |
| 48 | namespace Lax434175.HighMultiplicity |
| 49 | open Lax434175 Lax434175.Problems Lax434175.Assembly Lax434175.Results Lax434175.ResultParameters |
| 50 | open Lax434175.Propagation |
| 51 | |
| 52 | /-- The standard reading determines the answer for every specification with high |
| 53 | multiplicity. -/ |
| 54 | axiom determined {t : Spec OperationsFamily.family} |
| 55 | (ht : t.module .encoding = .highMultiplicity) : Determined StandardReading.ops t |
| 56 | |
| 57 | /-- The arrow `s ≤ t` from a specification with the standard encoding and without |
| 58 | facts on pairs of jobs to one with high multiplicity. -/ |
| 59 | structure Step (s t : Spec OperationsFamily.family) : Prop where |
| 60 | le : s.le t |
| 61 | standard : s.module .encoding = .standard |
| 62 | highMultiplicity : t.module .encoding = .highMultiplicity |
| 63 | noPrecedence : (s.module .precedence).order = .none |
| 64 | noDelays : s.module .communicationDelays = .none |
| 65 | |
| 66 | variable {s t : Spec OperationsFamily.family} |
| 67 | |
| 68 | /-- On every instance `y` with threshold `D'` written by a high-multiplicity word of the |
| 69 | lift of an instance `x` of `s` with threshold `D`, `κt y D'` is at most `g (κs x D)`. -/ |
| 70 | def ParamBound (hF : OperationsFamily.family.Sound) (h : s.le t) (κs : TParameter (problem _ s)) |
| 71 | (κt : TParameter (problem _ t)) (g : ℕ → ℕ) : Prop := |
| 72 | ∀ u x D y D', EncodesDecision (StandardReading.ops.at t) u ((Assembly.lift _ hF h).map x) D → |
| 73 | EncodesDecision (StandardReading.ops.at t) u y D' → κt y D' ≤ g (κs x D) |
| 74 | |
| 75 | open Lax496464.WH_A2_FptReductions Lax496464.WH_B4_Hierarchies |
| 76 | |
| 77 | /-- NP-hardness goes up from the standard encoding to high multiplicity. -/ |
| 78 | axiom npHard_up (hst : Step s t) : |
| 79 | NPHard (StandardReading.ops.at s) → NPHard (StandardReading.ops.at t) |
| 80 | |
| 81 | /-- W[t]-hardness goes up from the standard encoding to high multiplicity. -/ |
| 82 | axiom wHard_up (hst : Step s t) (hF : OperationsFamily.family.Sound) (w : ℕ) |
| 83 | {κs : TParameter (problem _ s)} {κt : TParameter (problem _ t)} (g : ℕ → ℕ) (hg : Computable g) |
| 84 | (hκ : ParamBound hF hst.le κs κt g) : |
| 85 | WHard (StandardReading.ops.at s) w κs → WHard (StandardReading.ops.at t) w κt |
| 86 | |
| 87 | /-- Being in P goes down from high multiplicity to the standard encoding. -/ |
| 88 | axiom inP_down (hst : Step s t) : |
| 89 | InP (StandardReading.ops.at t) → InP (StandardReading.ops.at s) |
| 90 | |
| 91 | /-- Fixed-parameter tractability goes down from high multiplicity to the standard |
| 92 | encoding. -/ |
| 93 | axiom isFPT_down (hst : Step s t) (hF : OperationsFamily.family.Sound) |
| 94 | {κs : TParameter (problem _ s)} {κt : TParameter (problem _ t)} |
| 95 | (g : ℕ → ℕ) (hg : Computable g) (hκ : ParamBound hF hst.le κs κt g) |
| 96 | (hps : IsParameterized (parameterized (StandardReading.ops.at s) κs)) : |
| 97 | IsFPT (StandardReading.ops.at t) κt → IsFPT (StandardReading.ops.at s) κs |
| 98 | |
| 99 | /-- NP-hardness goes up along `P||Cmax → P|HM|Cmax`. -/ |
| 100 | axiom npHard_makespan : |
| 101 | NPHard (StandardReading.ops.at ZooParallel.p0) → NPHard (StandardReading.ops.at ZooParallel.p254) |
| 102 | |
| 103 | /-- W[t]-hardness for the number of machines goes up along `P||Cmax → P|HM|Cmax`. -/ |
| 104 | axiom wHard_m_makespan (w : ℕ) : |
| 105 | WHard (StandardReading.ops.at ZooParallel.p0) w (Results.lift (Ops.m ZooParallel.p0)) → |
| 106 | WHard (StandardReading.ops.at ZooParallel.p254) w (Results.lift (Ops.m ZooParallel.p254)) |
| 107 | |
| 108 | /-- Fixed-parameter tractability for the number of distinct processing times goes down |
| 109 | along `P||Cmax → P|HM|Cmax`. -/ |
| 110 | axiom isFPT_numP_makespan : |
| 111 | IsFPT (StandardReading.ops.at ZooParallel.p254) (Results.lift (Ops.numP ZooParallel.p254)) → |
| 112 | IsFPT (StandardReading.ops.at ZooParallel.p0) (Results.lift (Ops.numP ZooParallel.p0)) |
| 113 | |
| 114 | end Lax434175.HighMultiplicity |
| 115 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments