Lax Lean Archive

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

The scheduling problems, parameterized

Lax470956.SchedulingProblems · concepts/Lax470956/SchedulingProblems.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

    Definition

    Interval scheduling with eligible machine sets, as parameterized problems on words: the decision problem "is weight WW attainable?" parameterized by the number mm of machines, the same problem parameterized by m+pmax⁡m + p_{\max}, and the problem "can every job be scheduled?" parameterized by pmax⁡p_{\max}.

    The three theorems of this submission are about these three problems: the first is W[1]-hard, the second is fixed-parameter tractable, and the third is NP-hard already when its parameter is bounded by an absolute constant.

    Concept map
    6 concepts; 3 descendants hidden
    100%
    Proven claimOpen 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.InstanceEncoding
    2import Lax470956.ParameterizedComplexity
    3
    4/-!
    5---
    6title: The scheduling problems, parameterized
    7type: definition
    8---
    9Interval scheduling with eligible machine sets, as parameterized problems on words:
    10the decision problem "is weight WW attainable?" parameterized by the number mm of
    11machines, the same problem parameterized by m+pmax⁡m + p_{\max}, and the problem "can every
    12job be scheduled?" parameterized by pmax⁡p_{\max}.
    13
    14The three theorems of this submission are about these three problems: the first is
    15W[1]-hard, the second is fixed-parameter tractable, and the third is NP-hard already
    16when its parameter is bounded by an absolute constant.
    17
    18# Formalization notes
    19
    20Each parameter is read off the word rather than supplied beside it. The number of
    21machines is the word's second entry, so it costs a program nothing to obtain; pmax⁡p_{\max}
    22is the largest processing time, which a program computes in one pass over the
    23processing-time block, and which the parameter function therefore also computes rather
    24than reads. Both are functions of the word alone, as the definition of a parameterized problem asks.
    25
    26A word outside the domain has no meaningful parameter. The parameter function is total
    27regardless — it returns the second entry, or the largest entry of a block that may not
    28exist — and nothing is claimed about its value there, since every statement quantifies
    29over admissible words only.
    30
    31`pmaxOf` is defined on the word rather than on the decoded instance so that the
    32parameter of a problem is manifestly a function of the input. On an admissible word the
    33two agree, which is a lemma of the proof layer rather than part of the definition.
    34-/
    35
    36namespace Lax470956.SchedulingProblems
    37
    38open Lax470956.Scheduling Lax470956.InstanceEncoding Lax470956.ParameterizedComplexity
    39open Lax808846.Ram Lax808846.RamComputes
    40
    41/-- The largest processing time declared by a word: the largest of the `n` entries of
    42its processing-time block. -/
    43def pmaxOf (x : List ℕ) : ℕ :=
    44 ((List.range (jobCount x)).map (proc x)).foldr max 0
    45
    46/-- **Interval scheduling with eligible machine sets**, parameterized by the number of
    47machines. -/
    48def byMachines : Problem where
    49 Domain := DecisionInstances
    50 Yes x := ∃ I W, EncodesDecisionInstance x I W ∧ I.HasWeight W
    51 param x := machineCount x
    52
    53/-- The same problem, parameterized by the number of machines together with the largest
    54processing time. -/
    55def byMachinesAndPmax : Problem where
    56 Domain := DecisionInstances
    57 Yes x := ∃ I W, EncodesDecisionInstance x I W ∧ I.HasWeight W
    58 param x := machineCount x + pmaxOf x
    59
    60/-- **Scheduling every job**: is there a feasible schedule that rejects no job?
    61Parameterized by the largest processing time. Instances carry no threshold. -/
    62def allSchedulableByPmax : Problem where
    63 Domain := Instances
    64 Yes x := ∃ I, EncodesInstance x I ∧ I.AllSchedulable
    65 param x := pmaxOf x
    66
    67/-- **The parameter is computed by a word RAM program in linear time.** One program and
    68one constant `c` such that, at every word length, on every decision instance whose
    69entries fit, the program halts within `c · (|x| + 1)` instructions having written the
    70largest processing time.
    71
    72A parameterized problem whose parameter no machine can read is not one a machine can be
    73handed, and the parameter of the second and third problems above is not an entry of the
    74word but a maximum over a block of it. This says that reading it costs a single pass,
    75so that nothing in the running time of the third theorem is hidden in obtaining the
    76parameter it is stated in terms of. -/
    77axiom pmaxOf_computesInTime :
    78 ∃ (prog : Program) (c : ℕ), ∀ w : ℕ,
    79 ComputesInTime w prog
    80 {x | x ∈ DecisionInstances ∧ Fits c w x}
    81 (fun x => [pmaxOf x])
    82 (fun x => c * (x.length + 1))
    83
    84end Lax470956.SchedulingProblems
    85
    Show Proof
    Formalization notes

    Each parameter is read off the word rather than supplied beside it. The number of machines is the word's second entry, so it costs a program nothing to obtain; pmax⁡p_{\max} is the largest processing time, which a program computes in one pass over the processing-time block, and which the parameter function therefore also computes rather than reads. Both are functions of the word alone, as the definition of a parameterized problem asks.

    A word outside the domain has no meaningful parameter. The parameter function is total regardless — it returns the second entry, or the largest entry of a block that may not exist — and nothing is claimed about its value there, since every statement quantifies over admissible words only.

    pmaxOfpmaxOf is defined on the word rather than on the decoded instance so that the parameter of a problem is manifestly a function of the input. On an admissible word the two agree, which is a lemma of the proof layer rather than part of the definition.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…