While this submission is a draft, it cannot be used by other submissions.

Interval scheduling is W[1]-hard for the number of machines

Lax470956.Theorem1 · concepts/Lax470956/Theorem1.lean · lax-470956

proven

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Multicoloured Clique, parameterized by the number of colours, fpt-reduces to interval scheduling with eligible machine sets, parameterized by the number mm 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 mm. It is therefore fixed-parameter tractable only if W[1]=FPT\mathrm{W}[1] = \mathrm{FPT}, which is not believed: no algorithm solves it in f(m)poly(n)f(m) \cdot \mathrm{poly}(n) time unless the hierarchy collapses. The third theorem of this submission shows that adding pmaxp_{\max} to the parameter does make the problem tractable, so the two results together locate the boundary.

    The reduction turns an instance with kk colours into a scheduling instance on (k2)+1\binom{k}{2}+1 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
    9 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax470956.MulticolouredClique
    2import Lax470956.SchedulingProblems
    3
    4/-!
    5---
    6title: Interval scheduling is W[1]-hard for the number of machines
    7type: theorem
    8---
    9Multicoloured Clique, parameterized by the number of colours, fpt-reduces to interval
    10scheduling with eligible machine sets, parameterized by the number mm of machines.
    11
    12Multicoloured Clique is W[1]-complete (Fellows, Hermelin, Rosamond and Vialette 2009), so
    13this says that interval scheduling with eligible machine sets is W[1]-hard for mm. It is
    14therefore fixed-parameter tractable only if W[1]=FPT\mathrm{W}[1] = \mathrm{FPT}, which is not
    15believed: no algorithm solves it in f(m)poly(n)f(m) \cdot \mathrm{poly}(n) time unless the
    16hierarchy collapses. The third theorem of
    17this submission shows that adding pmaxp_{\max} to the parameter does make the problem
    18tractable, so the two results together locate the boundary.
    19
    20The reduction turns an instance with kk colours into a scheduling instance on
    21(k2)+1\binom{k}{2}+1 machines — one for each pair of colours, which selects an edge between
    22those two colour classes, and one validation machine. The parameter of the image depends
    23on the parameter of the source alone, so the reduction is an fpt-reduction
    24and not merely a correct one.
    25
    26# Formalization notes
    27
    28The statement is the existence of an fpt-reduction, which unfolds to one map, one
    29program and one constant serving every instance and every admitting word length. It does
    30not mention the construction: which gadget realizes the reduction is the content of the
    31proof, not of the claim.
    32
    33The claim carries the running time of the reduction, not only its combinatorial
    34correctness. The two are separate obligations and a proof has to discharge both; the
    35weights this reduction emits grow as a polynomial in the number of vertices and the
    36number of colours, so the fitting conditions on the image are not automatic and the
    37running-time half is where they are paid for.
    38
    39The class W[1] is not formalized, so W[1]-hardness is not itself a statement of this
    40submission. What is stated is the reduction from the standard complete problem, which is
    41what a W[1]-hardness proof establishes. Reading it as W[1]-hardness uses two facts from
    42the literature and no Lean statement depends on them: that Multicoloured Clique is
    43W[1]-complete, and that fpt-reductions compose.
    44-/
    45
    46namespace Lax470956.Theorem1
    47
    48open Lax470956.ParameterizedComplexity
    49
    50/-- **Theorem 1.** Multicoloured Clique fpt-reduces to interval scheduling with eligible
    51machine sets, parameterized by the number of machines. -/
    52axiom mcc_fptReduces_byMachines :
    53 MulticolouredClique.problem ≤fpt SchedulingProblems.byMachines
    54
    55end Lax470956.Theorem1
    56
    Show Proof
    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.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…