P | M_j | Σ w_j Z_j is strongly W[1]-hard for the number of machines
Lax434175.IsemStrong · concepts/Lax434175/IsemStrong.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
The reduction behind starts from a Multicoloured Clique instance with vertices and colours, writes the interval scheduling instance of Construction 1 of lax-888481 with its threshold, pads it (), and writes the standard word of the zoo instance. The numbers Construction 1 writes are at most , and it has jobs and one more per edge.
Before the standard word is written, the threshold is lowered to . No schedule has weight above , so the answer is kept; the map is computed in polynomial time on the word RAM, and it keeps the number of machines.
If , then , the instance has at least jobs, and the standard word has a record for each, so its length is at least . Padding, dropping the unused machines and writing the standard word raise the numbers and the length only polynomially, so every number of the standard word is at most . If , the instance has no job, the lowered threshold is at most , and every number of the standard word is at most .
Theorem. Multicoloured Clique fpt-reduces to under the standard reading, parameterized by the number of machines, restricted to the words whose numbers are at most . Since Multicoloured Clique is W[1]-complete (lax-496464), the problem is strongly W[1]-hard for the number of machines.
Concept map
Lean source view on GitHub
| 1 | import Lax434175.IsemStandard |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: P | M_j | Σ w_j Z_j is strongly W[1]-hard for the number of machines |
| 6 | type: theorem |
| 7 | --- |
| 8 | The reduction behind `IsemStandard` starts from a Multicoloured Clique instance with |
| 9 | vertices and colours, writes the interval scheduling instance of Construction 1 of |
| 10 | lax-888481 with its threshold, pads it (`IsemLink`), and writes the standard word of the zoo |
| 11 | instance. The numbers Construction 1 writes are at most , and it has |
| 12 | jobs and one more per edge. |
| 13 | |
| 14 | Before the standard word is written, the threshold is lowered to |
| 15 | . No schedule has weight above , so the answer is kept; |
| 16 | the map is computed in polynomial time on the word RAM, and it keeps the number of machines. |
| 17 | |
| 18 | If , then , the instance has at least jobs, and the standard word |
| 19 | has a record for each, so its length is at least . Padding, dropping the unused |
| 20 | machines and writing the standard word raise the numbers and the length only polynomially, so |
| 21 | every number of the standard word is at most . If |
| 22 | , the instance has no job, the lowered threshold is at most , and every number of the |
| 23 | standard word is at most . |
| 24 | |
| 25 | **Theorem.** Multicoloured Clique fpt-reduces to under the |
| 26 | standard reading, parameterized by the number of machines, restricted to the words whose |
| 27 | numbers are at most . Since Multicoloured Clique is W[1]-complete |
| 28 | (lax-496464), the problem is strongly W[1]-hard for the number of machines. |
| 29 | -/ |
| 30 | |
| 31 | namespace Lax434175.IsemStrong |
| 32 | open Lax434175 Lax434175.Results Lax434175.ResultParameters |
| 33 | |
| 34 | /-- `P|M_j|Σ w_j Z_j` is strongly W[1]-hard in the number of machines under the standard |
| 35 | reading. -/ |
| 36 | axiom p200_r0_holds : ZooParallelResults.p200_r0 StandardReading.ops |
| 37 | |
| 38 | end Lax434175.IsemStrong |
| 39 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments