Hardness of P | M_j | Σ w_j Z_j under the standard reading
Lax434175.IsemStandard · concepts/Lax434175/IsemStandard.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Interval scheduling with eligible machine sets is the problem read on the words of lax-888481 (). Its hardness carries to the zoo's problem under the standard reading by a word map computed in polynomial time on the word RAM: drop the machines no job may use and renumber the others, then write the standard word of the instance with the threshold . Dropping the unused machines keeps the answer and does not raise the number of machines or the largest processing time.
Theorem. Under the standard reading, is W[1]-hard parameterized by the number of machines.
Theorem. Under the standard reading, is NP-hard on the instances whose processing times are at most , so para-NP-hard parameterized by the largest processing time.
Fixed-parameter tractability goes the other way, from the standard reading to the words of interval scheduling, where every job has positive length. Under the standard reading a job may have length zero: it is then a point, which a job running strictly across it blocks, and which no other point blocks. So the points with the same due date and the same machines are one point with their total weight. Scaling all times by , where bounds the number of such points at one time, turns every job of positive length into and the -th point at time into : two jobs overlap after scaling exactly when they clash before. Jobs that can never be on time, and points other than the first of their kind, become jobs without a machine, which padding (as in ) gives a new machine of their own. The number of machines grows by one and the largest processing time by the factor .
Theorem. Under the standard reading, is fixed-parameter tractable parameterized by the number of machines plus the largest processing time.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax434175.ZooParallel |
| 2 | import Lax434175.Results |
| 3 | import Lax434175.ResultParameters |
| 4 | import Lax434175.StandardReading |
| 5 | import Lax434175.ZooParallelResults |
| 6 | |
| 7 | /-! |
| 8 | --- |
| 9 | title: Hardness of P | M_j | Σ w_j Z_j under the standard reading |
| 10 | type: theorem |
| 11 | --- |
| 12 | Interval scheduling with eligible machine sets is the problem |
| 13 | read on the words of lax-888481 (`IsemLink`). Its hardness carries to the zoo's problem |
| 14 | under the standard reading by a word map computed in polynomial time on the word RAM: drop |
| 15 | the machines no job may use and renumber the others, then write the standard word of the |
| 16 | instance with the threshold . Dropping the unused machines keeps the answer |
| 17 | and does not raise the number of machines or the largest processing time. |
| 18 | |
| 19 | **Theorem.** Under the standard reading, is W[1]-hard |
| 20 | parameterized by the number of machines. |
| 21 | |
| 22 | **Theorem.** Under the standard reading, is NP-hard on the |
| 23 | instances whose processing times are at most , so para-NP-hard parameterized by the |
| 24 | largest processing time. |
| 25 | |
| 26 | Fixed-parameter tractability goes the other way, from the standard reading to the words of |
| 27 | interval scheduling, where every job has positive length. Under the standard reading a job may |
| 28 | have length zero: it is then a point, which a job running strictly across it blocks, and which |
| 29 | no other point blocks. So the points with the same due date and the same machines are one point |
| 30 | with their total weight. Scaling all times by , where bounds |
| 31 | the number of such points at one time, turns every job of positive length into |
| 32 | and the -th point at time into : two |
| 33 | jobs overlap after scaling exactly when they clash before. Jobs that can never be on time, and |
| 34 | points other than the first of their kind, become jobs without a machine, which padding (as in |
| 35 | `IsemLink`) gives a new machine of their own. The number of machines grows by one and the |
| 36 | largest processing time by the factor . |
| 37 | |
| 38 | **Theorem.** Under the standard reading, is fixed-parameter |
| 39 | tractable parameterized by the number of machines plus the largest processing time. |
| 40 | -/ |
| 41 | |
| 42 | namespace Lax434175.IsemStandard |
| 43 | open Lax434175 Lax434175.Results Lax434175.ResultParameters |
| 44 | |
| 45 | -- zoo-result: {"problem": "P|M_j|\\sum w_jZ_j", "param": "m", "claim": "is W[1]-hard", "note": "Multicoloured Clique (W[1]-complete in lax-496464) fpt-reduces to it. The cited result says strongly W[1]-hard, which is proved as well (IsemStrong.p200_r0_holds)."} |
| 46 | axiom wHard_m : |
| 47 | WHard (StandardReading.ops.at ZooParallel.p200) 1 (lift (Ops.m ZooParallel.p200)) |
| 48 | |
| 49 | -- zoo-result: {"problem": "P|M_j|\\sum w_jZ_j", "param": "pmax", "claim": "is para-NP-hard"} |
| 50 | axiom paraNPHard_pmax : |
| 51 | ParaNPHard (StandardReading.ops.at ZooParallel.p200) (lift (Ops.pmax ZooParallel.p200)) |
| 52 | |
| 53 | -- zoo-result: {"problem": "P|M_j|\\sum w_jZ_j", "param": "m+pmax", "claim": "is fixed parameter tractable"} |
| 54 | axiom fpt_mPmax : Lax434175.ZooParallelResults.p200_r1 StandardReading.ops |
| 55 | |
| 56 | end Lax434175.IsemStandard |
| 57 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments