Hardness of P | M_j | Σ w_j Z_j
Lax434175.JitHardness · concepts/Lax434175/JitHardness.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Read through interval scheduling with eligible machine sets (lax-888481), the zoo problem inherits the two hardness results of that problem.
W[1]-hardness for the number of machines. Multicoloured Clique, parameterized by the number of colours, fpt-reduces to interval scheduling parameterized by the number of machines (Theorem 1 of lax-888481), and that problem fpt-reduces to parameterized by the number of machines, by padding. Both reductions are strict fpt-reductions of the archive, computed by word RAM programs in linear fixed-parameter time; they raise the parameter by computable functions of it, and the numbers they write are below for a computable , where is the bit size of the input and its parameter. So both are fpt-reductions in the sense of lax-496464, and so is their composition.
Theorem. Multicoloured Clique fpt-reduces to parameterized by the number of machines. Since Multicoloured Clique is W[1]-complete (lax-496464), the problem is W[1]-hard.
NP-hardness for . For an interval scheduling instance , let be its padding: a job without an eligible machine gets one new machine and weight . Read as an instance of with threshold , the total weight of minus the total weight of .
Theorem. Deciding this instance is NP-hard already on the interval scheduling instances with processing times at most and unit weights: every language in NP reduces to it by a polynomial-time Turing machine writing the encoding of . On such an instance the threshold is met exactly when every job of can be scheduled, which is NP-hard by Theorem 2 of lax-888481. Padding keeps the processing times, so the zoo instances have , and the problem is para-NP-hard for .
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax434175.IsemLink |
| 2 | import Lax888481.Theorem2 |
| 3 | import Lax496464.WH_D12_MulticolouredClique |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Hardness of P | M_j | Σ w_j Z_j |
| 8 | type: theorem |
| 9 | --- |
| 10 | Read through interval scheduling with eligible machine sets (lax-888481), the |
| 11 | zoo problem inherits the two hardness results |
| 12 | of that problem. |
| 13 | |
| 14 | **W[1]-hardness for the number of machines.** Multicoloured Clique, |
| 15 | parameterized by the number of colours, fpt-reduces to interval scheduling |
| 16 | parameterized by the number of machines (Theorem 1 of lax-888481), and that |
| 17 | problem fpt-reduces to parameterized by the number of |
| 18 | machines, by padding. Both reductions are strict fpt-reductions of the |
| 19 | archive, computed by word RAM programs in linear fixed-parameter time; they |
| 20 | raise the parameter by computable functions of it, and the numbers they write |
| 21 | are below for a computable , where is the bit size |
| 22 | of the input and its parameter. So both are fpt-reductions in the sense of |
| 23 | lax-496464, and so is their composition. |
| 24 | |
| 25 | **Theorem.** Multicoloured Clique fpt-reduces to |
| 26 | parameterized by the number of machines. Since |
| 27 | Multicoloured Clique is W[1]-complete (lax-496464), the problem is W[1]-hard. |
| 28 | |
| 29 | **NP-hardness for .** For an interval scheduling instance |
| 30 | , let be its padding: a job without an eligible machine gets one new |
| 31 | machine and weight . Read as an instance of |
| 32 | with threshold , the |
| 33 | total weight of minus the total weight of . |
| 34 | |
| 35 | **Theorem.** Deciding this instance is NP-hard already on the interval |
| 36 | scheduling instances with processing times at most and unit weights: every |
| 37 | language in NP reduces to it by a polynomial-time Turing machine writing the |
| 38 | encoding of . On such an instance the threshold is met exactly when every |
| 39 | job of can be scheduled, which is NP-hard by Theorem 2 of lax-888481. |
| 40 | Padding keeps the processing times, so the zoo instances have |
| 41 | , and the problem is para-NP-hard for . |
| 42 | -/ |
| 43 | |
| 44 | namespace Lax434175.JitHardness |
| 45 | open Lax434175 Lax434175.Problems Lax434175.Assembly Lax434175.IsemLink |
| 46 | open Lax888481.Scheduling Lax888481.NPHardness |
| 47 | open Lax496464.WH_A2_FptReductions Lax496464.WH_B4_Hierarchies |
| 48 | |
| 49 | axiom mcc_fptReduces_jitByMachines : |
| 50 | Lax888481.MulticolouredClique.problem ≤ᶠᵖᵗ jitByMachines |
| 51 | |
| 52 | axiom w1Hard_jitByMachines : Hard (W 1) jitByMachines |
| 53 | |
| 54 | /-- The zoo instance of the padding of `I` meets the threshold: total weight of |
| 55 | the padding minus total weight of `I`. -/ |
| 56 | def JitYes (I : Instance) : Prop := |
| 57 | (problem _ jitSets).Decides (toZoo (pad I)) |
| 58 | (((totalWeight (pad I) : ℤ) - totalWeight I : ℤ) : ℚ) |
| 59 | |
| 60 | axiom npHardOn_jit_pmax_le : |
| 61 | NPHardOn JitYes fun I => I.pmax ≤ 25 ∧ ∀ j, I.w j = 1 |
| 62 | |
| 63 | end Lax434175.JitHardness |
| 64 |
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