1|r_j|L_max is para-NP-hard for the largest and the number of processing times
Lax434175.SanityParams · concepts/Lax434175/SanityParams.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
The reduction that makes NP-hard (concept , from lax-391470 with the job lengths ) produces only instances whose processing times are or ; on a word that is not such an instance it produces the instance without jobs. So the problem is NP-hard already on the instances with , and on those with at most two distinct processing times.
Theorem. is para-NP-hard parameterized by , and parameterized by the number of distinct processing times, on the standard reading.
The explicit reductions of lax-391470 (Cook–Levin to satisfiability, then the formula instance, then the stacked instance) produce release times and deadlines at most a constant times the number of jobs: the time line of the formula instance has length with linear in the number of clauses, the stacked instance has connected pairs, five jobs each, and stacking adds at most per pair. So every number of the emitted word is linear in its length.
Theorem. is strongly NP-hard on the standard reading.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax434175.Sanity |
| 2 | import Lax434175.ZooParallelResults |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: 1|r_j|L_max is para-NP-hard for the largest and the number of processing times |
| 7 | type: theorem |
| 8 | --- |
| 9 | The reduction that makes NP-hard (concept `Sanity`, from |
| 10 | lax-391470 with the job lengths ) produces only instances whose |
| 11 | processing times are or ; on a word that is not such an instance it produces |
| 12 | the instance without jobs. So the problem is NP-hard already on the instances with |
| 13 | , and on those with at most two distinct processing times. |
| 14 | |
| 15 | **Theorem.** is para-NP-hard parameterized by , |
| 16 | and parameterized by the number of distinct processing times, on the |
| 17 | standard reading. |
| 18 | |
| 19 | The explicit reductions of lax-391470 (Cook–Levin to satisfiability, then the formula |
| 20 | instance, then the stacked instance) produce release times and deadlines at most a |
| 21 | constant times the number of jobs: the time line of the formula instance has length |
| 22 | with linear in the number of clauses, the stacked instance has |
| 23 | connected pairs, five jobs each, and stacking adds at most |
| 24 | per pair. So every number of the emitted word is linear in its length. |
| 25 | |
| 26 | **Theorem.** is strongly NP-hard on the standard reading. |
| 27 | -/ |
| 28 | |
| 29 | namespace Lax434175.SanityParams |
| 30 | open Lax434175 Lax434175.Results Lax434175.ResultParameters |
| 31 | |
| 32 | /-- `1|rj|Lmax`, parameter pmax: para-NP-hard on the standard reading. -/ |
| 33 | -- zoo-result: {"problem": "1|r_j|L_{\\max}", "param": "pmax", "claim": "is para-NP-hard", "note": "through lax-391470 (job lengths 2 and 3): NP-hard already with pmax ≤ 3"} |
| 34 | axiom paraNPHard_pmax : |
| 35 | ParaNPHard (StandardReading.ops.at ZooParallel.p158) (lift (Ops.pmax ZooParallel.p158)) |
| 36 | |
| 37 | /-- `1|rj|Lmax`, parameter #p: para-NP-hard on the standard reading. -/ |
| 38 | -- zoo-result: {"problem": "1|r_j|L_{\\max}", "param": "#p", "claim": "is para-NP-hard", "note": "through lax-391470 (job lengths 2 and 3), and #p ≤ pmax + 1"} |
| 39 | axiom paraNPHard_numP : |
| 40 | ParaNPHard (StandardReading.ops.at ZooParallel.p158) (lift (Ops.numP ZooParallel.p158)) |
| 41 | |
| 42 | /-- `1|rj|Lmax` is strongly NP-hard on the standard reading: with the explicit reductions |
| 43 | of lax-391470, every release time and deadline is at most a constant times the number of |
| 44 | jobs, so the emitted words have numbers linear in their length. -/ |
| 45 | axiom p158_r0_holds : ZooParallelResults.p158_r0 StandardReading.ops |
| 46 | |
| 47 | /-- `1|rj|Lmax` is strongly NP-hard, the result as cited from Elffers and de Weerdt. -/ |
| 48 | axiom p158_r1_holds : ZooParallelResults.p158_r1 StandardReading.ops |
| 49 | |
| 50 | /-- `1|rj|Lmax` is NP-hard for a fixed largest processing time. -/ |
| 51 | axiom p158_r2_holds : ZooParallelResults.p158_r2 StandardReading.ops |
| 52 | |
| 53 | /-- `1|rj|Lmax` is NP-hard for a fixed number of distinct processing times. -/ |
| 54 | axiom p158_r3_holds : ZooParallelResults.p158_r3 StandardReading.ops |
| 55 | |
| 56 | end Lax434175.SanityParams |
| 57 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments