Lax Lean Archive

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

Interval scheduling is fixed-parameter tractable for the machines and the largest processing time

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

proven

Loading review…

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

    Interval scheduling with eligible machine sets is fixed-parameter tractable for the combined parameter m+pmax⁡m + p_{\max}. There are one word RAM program and one constant cc such that, at every word length, on every decision instance whose encoding fits into words, the program halts within

    c⋅(m⋅pmax⁡+1)2m⋅(m+1)⋅(∣x∣+1)c \cdot (m \cdot p_{\max} + 1)^{2m} \cdot (m+1) \cdot (|x|+1)

    instructions and writes 11 if a feasible schedule of weight WW exists and 00 if none does.

    The algorithm sweeps the time axis. At each point it records, for every machine, how much longer that machine stays busy (a vector of mm numbers, each at most pmax⁡p_{\max}) and the best weight achieving that configuration. A preprocessing step first discards all but a bounded number of jobs per starting time, so the number of jobs alive at any moment, and hence the number of reachable configurations, is bounded by a function of the parameter alone.

    Together with the first theorem, which rules out fixed-parameter tractability for mm alone unless W[1]=FPT\mathrm{W}[1] = \mathrm{FPT}, and the second, which rules it out for pmax⁡p_{\max} alone unless P=NP\mathrm{P} = \mathrm{NP}, this locates the problem: the combined parameter is tractable and neither half of it is.

    Concept map
    7 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 fpt_byMachinesAndPmax proven

    2 fptTime_byMachinesAndPmax proven

    Lean source view on GitHub

    1import Lax470956.SchedulingProblems
    2
    3/-!
    4---
    5title: Interval scheduling is fixed-parameter tractable for the machines and the largest processing time
    6type: theorem
    7---
    8Interval scheduling with eligible machine sets is fixed-parameter tractable for the
    9combined parameter m+pmax⁡m + p_{\max}. There are one word RAM program and one constant cc
    10such that, at every word length, on every decision instance whose encoding fits into
    11words, the program halts within
    12c⋅(m⋅pmax⁡+1)2m⋅(m+1)⋅(∣x∣+1)c \cdot (m \cdot p_{\max} + 1)^{2m} \cdot (m+1) \cdot (|x|+1)
    13instructions and writes 11 if a feasible schedule of weight WW exists and 00 if none
    14does.
    15
    16The algorithm sweeps the time axis. At each point it records, for every machine, how much
    17longer that machine stays busy (a vector of mm numbers, each at most pmax⁡p_{\max}) and the
    18best weight achieving that configuration. A preprocessing step first discards all but a
    19bounded number of jobs per starting time, so the number of jobs alive at any moment, and
    20hence the number of reachable configurations, is bounded by a function of the parameter alone.
    21
    22Together with the first theorem, which rules out fixed-parameter tractability for mm
    23alone unless W[1]=FPT\mathrm{W}[1] = \mathrm{FPT}, and the second, which rules it out for
    24pmax⁡p_{\max} alone unless P=NP\mathrm{P} = \mathrm{NP}, this locates the problem: the
    25combined parameter is tractable and neither half of it is.
    26
    27# Formalization notes
    28
    29Two statements are made. The first gives the running time explicitly, with the dependence on
    30the parameter written out, for the words that leave room for the algorithm's table. The second
    31is `FPT` from `ParameterizedComplexity`, for every word whose entries fit.
    32
    33The first statement's domain has a second clause beyond `Fits`. `Fits` says that the entries
    34of the instance are words, which is needed because deadlines and weights are not bounded by the
    35length of the word. The second clause says that c (m pmax⁡+1)2mc\,(m\,p_{\max}+1)^{2m} is a word. The
    36algorithm's table is indexed by machine configurations, there are (pmax⁡+1)m(p_{\max}+1)^m of them, and
    37a machine with 2w2^w cells cannot address a larger table, so without the clause the claimed
    38time would not be achievable.
    39
    40`FPT` has no such clause, so the second statement is not a weakening of the first. The
    41program compares the word's length with the table: when the word is at least as long as the
    42table, the table fits, since every admissible word fits with room for a multiple of its
    43length; when the word is shorter than the table, its length is bounded by a function of the
    44parameter, and the program tries every schedule instead. The function of the parameter is
    45then much larger than (m pmax⁡)2m(m\,p_{\max})^{2m}.
    46
    47The program and the constant are quantified before the word length, so one program serves
    48every word length that admits its input. A program chosen after the word length could hide an
    49unbounded amount of information in its literals and would be a family of programs, not an
    50algorithm.
    51
    52The theorem is stated for the decision problem with a threshold rather than for the
    53optimization problem. The algorithm computes the optimum and the comparison is one further
    54instruction; the decision version has the same shape as the two hardness theorems.
    55-/
    56
    57namespace Lax470956.Theorem3
    58
    59open Lax808846.Ram Lax808846.RamComputes
    60open Lax470956.InstanceEncoding Lax470956.SchedulingProblems Lax470956.ParameterizedComplexity
    61
    62open Classical in
    63/-- **Theorem 3.** One word RAM program decides interval scheduling with eligible machine
    64sets within `c * (m * p_max + 1) ^ (2 * m) * (m + 1) * (|x| + 1)` instructions, at every
    65word length admitting the instance and a table indexed by machine configurations.
    66
    67The paper states the bound as `O((m · p_max)^{2m} · m · n)`. Written with an explicit
    68constant, the product needs the `+1`s: with no machines, or with no jobs, `(m · p_max)^{2m} · m`
    69is zero, and no program answers in zero instructions. Apart from those terms, the bound differs
    70from the paper's in measuring the input by `|x|` instead of `n`. -/
    71axiom fptTime_byMachinesAndPmax :
    72 ∃ (prog : Program) (c : ℕ), ∀ w : ℕ,
    73 ComputesInTime w prog
    74 {x | x ∈ DecisionInstances ∧ Fits c w x ∧
    75 c * (machineCount x * pmaxOf x + 1) ^ (2 * machineCount x) ≤ 2 ^ w}
    76 (fun x => if byMachinesAndPmax.Yes x then [1] else [0])
    77 (fun x => c * (machineCount x * pmaxOf x + 1) ^ (2 * machineCount x) *
    78 (machineCount x + 1) * (x.length + 1))
    79
    80/-- **Theorem 3**, in the general form: the problem parameterized by `m + p_max` is
    81fixed-parameter tractable.
    82
    83It does not follow from the explicit bound by weakening the function of the parameter,
    84because `FPT` asks for an answer on every word whose entries fit, and there the table need not
    85be addressable. Where it is not, the proof tries every schedule, and the function of the
    86parameter is much larger than `(m · p_max)^{2m}`. -/
    87axiom fpt_byMachinesAndPmax : FPT byMachinesAndPmax
    88
    89end Lax470956.Theorem3
    90
    Show ProofShow Proof
    Formalization notes

    Two statements are made. The first gives the running time explicitly, with the dependence on the parameter written out, for the words that leave room for the algorithm's table. The second is FPTFPT from ParameterizedComplexityParameterizedComplexity, for every word whose entries fit.

    The first statement's domain has a second clause beyond FitsFits. FitsFits says that the entries of the instance are words, which is needed because deadlines and weights are not bounded by the length of the word. The second clause says that c (m pmax⁡+1)2mc\,(m\,p_{\max}+1)^{2m} is a word. The algorithm's table is indexed by machine configurations, there are (pmax⁡+1)m(p_{\max}+1)^m of them, and a machine with 2w2^w cells cannot address a larger table, so without the clause the claimed time would not be achievable.

    FPTFPT has no such clause, so the second statement is not a weakening of the first. The program compares the word's length with the table: when the word is at least as long as the table, the table fits, since every admissible word fits with room for a multiple of its length; when the word is shorter than the table, its length is bounded by a function of the parameter, and the program tries every schedule instead. The function of the parameter is then much larger than (m pmax⁡)2m(m\,p_{\max})^{2m}.

    The program and the constant are quantified before the word length, so one program serves every word length that admits its input. A program chosen after the word length could hide an unbounded amount of information in its literals and would be a family of programs, not an algorithm.

    The theorem is stated for the decision problem with a threshold rather than for the optimization problem. The algorithm computes the optimum and the comparison is one further instruction; the decision version has the same shape as the two hardness theorems.

    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…