Interval scheduling is W[1]-hard for the number of machines
Lax470956.Theorem1 · concepts/Lax470956/Theorem1.lean · lax-470956
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Multicoloured Clique, parameterized by the number of colours, fpt-reduces to interval scheduling with eligible machine sets, parameterized by the number of machines.
Multicoloured Clique is W[1]-complete (Fellows, Hermelin, Rosamond and Vialette 2009), so this says that interval scheduling with eligible machine sets is W[1]-hard for . It is therefore fixed-parameter tractable only if , which is not believed: no algorithm solves it in time unless the hierarchy collapses. The third theorem of this submission shows that adding to the parameter does make the problem tractable, so the two results together locate the boundary.
The reduction turns an instance with colours into a scheduling instance on machines — one for each pair of colours, which selects an edge between those two colour classes, and one validation machine. The parameter of the image depends on the parameter of the source alone, so the reduction is an fpt-reduction and not merely a correct one.
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
Lean source view on GitHub
| 1 | import Lax470956.MulticolouredClique |
| 2 | import Lax470956.SchedulingProblems |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Interval scheduling is W[1]-hard for the number of machines |
| 7 | type: theorem |
| 8 | --- |
| 9 | Multicoloured Clique, parameterized by the number of colours, fpt-reduces to interval |
| 10 | scheduling with eligible machine sets, parameterized by the number of machines. |
| 11 | |
| 12 | Multicoloured Clique is W[1]-complete (Fellows, Hermelin, Rosamond and Vialette 2009), so |
| 13 | this says that interval scheduling with eligible machine sets is W[1]-hard for . It is |
| 14 | therefore fixed-parameter tractable only if , which is not |
| 15 | believed: no algorithm solves it in time unless the |
| 16 | hierarchy collapses. The third theorem of |
| 17 | this submission shows that adding to the parameter does make the problem |
| 18 | tractable, so the two results together locate the boundary. |
| 19 | |
| 20 | The reduction turns an instance with colours into a scheduling instance on |
| 21 | machines — one for each pair of colours, which selects an edge between |
| 22 | those two colour classes, and one validation machine. The parameter of the image depends |
| 23 | on the parameter of the source alone, so the reduction is an fpt-reduction |
| 24 | and not merely a correct one. |
| 25 | |
| 26 | # Formalization notes |
| 27 | |
| 28 | The statement is the existence of an fpt-reduction, which unfolds to one map, one |
| 29 | program and one constant serving every instance and every admitting word length. It does |
| 30 | not mention the construction: which gadget realizes the reduction is the content of the |
| 31 | proof, not of the claim. |
| 32 | |
| 33 | The claim carries the running time of the reduction, not only its combinatorial |
| 34 | correctness. The two are separate obligations and a proof has to discharge both; the |
| 35 | weights this reduction emits grow as a polynomial in the number of vertices and the |
| 36 | number of colours, so the fitting conditions on the image are not automatic and the |
| 37 | running-time half is where they are paid for. |
| 38 | |
| 39 | The class W[1] is not formalized, so W[1]-hardness is not itself a statement of this |
| 40 | submission. What is stated is the reduction from the standard complete problem, which is |
| 41 | what a W[1]-hardness proof establishes. Reading it as W[1]-hardness uses two facts from |
| 42 | the literature and no Lean statement depends on them: that Multicoloured Clique is |
| 43 | W[1]-complete, and that fpt-reductions compose. |
| 44 | -/ |
| 45 | |
| 46 | namespace Lax470956.Theorem1 |
| 47 | |
| 48 | open Lax470956.ParameterizedComplexity |
| 49 | |
| 50 | /-- **Theorem 1.** Multicoloured Clique fpt-reduces to interval scheduling with eligible |
| 51 | machine sets, parameterized by the number of machines. -/ |
| 52 | axiom mcc_fptReduces_byMachines : |
| 53 | MulticolouredClique.problem ≤fpt SchedulingProblems.byMachines |
| 54 | |
| 55 | end Lax470956.Theorem1 |
| 56 |
Formalization notes
The statement is the existence of an fpt-reduction, which unfolds to one map, one program and one constant serving every instance and every admitting word length. It does not mention the construction: which gadget realizes the reduction is the content of the proof, not of the claim.
The claim carries the running time of the reduction, not only its combinatorial correctness. The two are separate obligations and a proof has to discharge both; the weights this reduction emits grow as a polynomial in the number of vertices and the number of colours, so the fitting conditions on the image are not automatic and the running-time half is where they are paid for.
The class W[1] is not formalized, so W[1]-hardness is not itself a statement of this submission. What is stated is the reduction from the standard complete problem, which is what a W[1]-hardness proof establishes. Reading it as W[1]-hardness uses two facts from the literature and no Lean statement depends on them: that Multicoloured Clique is W[1]-complete, and that fpt-reductions compose.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments