Lax Lean Archive

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

Preprocessing an interval scheduling instance down to a bounded number of live jobs

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

    The step that makes the dynamic program fixed-parameter tractable. Two jobs with the same processing time and the same deadline occupy the same interval, so on any one machine they are interchangeable; of the jobs sharing an interval and eligible on a given machine, only the mm heaviest can ever be useful, because a schedule places at most mm of them at once and a lighter one can always be exchanged for a heavier unused one. Keeping, for each machine, the mm best jobs of each interval eligible there, and discarding the rest, leaves the optimum unchanged.

    What the step buys is a bound independent of the number of jobs. A job alive at time tt has a deadline in (t,t+pmax⁡](t, t+p_{\max}] and a processing time in [1,pmax⁡][1, p_{\max}], so there are at most pmax⁡2p_{\max}^2 intervals it could occupy; each interval keeps at most mm jobs per machine and there are mm machines. So at most pmax⁡2m2p_{\max}^2 m^2 surviving jobs are alive at any one instant — a bound in the parameter alone. Fed into the state-space bound of the dynamic program, this makes the table's size a function of mm and pmax⁡p_{\max}.

    Concept map
    3 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 card_keep_alive_le proven

    2 optimumOn_keep proven

    Lean source view on GitHub

    1import Lax470956.DynamicProgram
    2
    3/-!
    4---
    5title: Preprocessing an interval scheduling instance down to a bounded number of live jobs
    6type: definition
    7---
    8The step that makes the dynamic program fixed-parameter tractable. Two jobs with the
    9same processing time and the same deadline occupy the same interval, so on any one
    10machine they are interchangeable; of the jobs sharing an interval and eligible on a
    11given machine, only the mm heaviest can ever be useful, because a schedule places at
    12most mm of them at once and a lighter one can always be exchanged for a heavier unused
    13one. Keeping, for each machine, the mm best jobs of each interval eligible there, and
    14discarding the rest, leaves the optimum unchanged.
    15
    16What the step buys is a bound independent of the number of jobs. A job alive at time tt
    17has a deadline in (t,t+pmax⁡](t, t+p_{\max}] and a processing time in [1,pmax⁡][1, p_{\max}], so there
    18are at most pmax⁡2p_{\max}^2 intervals it could occupy; each interval keeps at most mm jobs
    19per machine and there are mm machines. So at most pmax⁡2m2p_{\max}^2 m^2 surviving jobs are
    20alive at any one instant — a bound in the parameter alone. Fed into the state-space
    21bound of the dynamic program, this makes the table's size a function of mm and pmax⁡p_{\max}.
    22
    23# Formalization notes
    24
    25Discarding is modelled as a set of kept jobs together with the best weight achievable
    26using only those, rather than as a second instance on a smaller job set. The two say the
    27same thing, and the first states it without transporting an instance along a change of
    28index type — which would make the statement about the transport as much as about the
    29preprocessing.
    30
    31Ties in weight are broken by the job's index. "The mm best" has to be well defined, and
    32some tie-break is needed to define it; the index is the tie-break a program would use,
    33since it is the order the jobs arrive in. `Better` is the resulting strict linear order:
    34heavier, or equally heavy and earlier.
    35
    36A job is kept when it is among the mm best *for some machine it is eligible on*, not
    37for all of them. The exchange argument needs this: a job is discarded only when every machine that could run
    38it already keeps mm better alternatives for its interval. It is also why the bound counts
    39machines twice.
    40-/
    41
    42namespace Lax470956.Preprocessing
    43
    44open Lax470956.Scheduling Lax470956.Scheduling.Instance Lax470956.DynamicProgram
    45
    46variable (I : Instance)
    47
    48/-- `j` is strictly better than `j'`: heavier, or equally heavy and earlier in index
    49order. -/
    50def Better (j j' : Fin I.jobs) : Prop :=
    51 I.w j' < I.w j ∨ (I.w j' = I.w j ∧ (j : ℕ) < (j' : ℕ))
    52
    53instance (j j' : Fin I.jobs) : Decidable (Better I j j') :=
    54 inferInstanceAs (Decidable (_ ∨ _))
    55
    56/-- The jobs occupying the interval `[dd - pp, dd)` that are eligible on machine `i`. -/
    57def slotOf (i : Fin I.machines) (dd pp : ℕ) : Finset (Fin I.jobs) :=
    58 Finset.univ.filter fun j => I.d j = dd ∧ I.p j = pp ∧ i ∈ I.eligible j
    59
    60/-- The jobs occupying the same interval as `j` that are eligible on machine `i`. -/
    61def sameSlot (i : Fin I.machines) (j : Fin I.jobs) : Finset (Fin I.jobs) :=
    62 slotOf I i (I.d j) (I.p j)
    63
    64/-- How many jobs of `j`'s slot on machine `i` beat `j`. -/
    65def rank (i : Fin I.machines) (j : Fin I.jobs) : ℕ :=
    66 ((sameSlot I i j).filter fun j' => Better I j' j).card
    67
    68/-- **The preprocessing step.** Keep a job when, for some machine it is eligible on, it
    69is among the `m` best jobs of its interval there. -/
    70def keep : Finset (Fin I.jobs) :=
    71 Finset.univ.filter fun j => ∃ i ∈ I.eligible j, rank I i j < I.machines
    72
    73/-- The best weight achievable by a feasible schedule that uses only jobs from `K`. -/
    74def optimumOn (K : Finset (Fin I.jobs)) : ℕ :=
    75 (Finset.univ.filter fun σ : I.Schedule => Feasible σ ∧ ∀ j, σ j ≠ none → j ∈ K).sup
    76 weight
    77
    78/-- **Lemma 5.** Preprocessing does not change the optimum: the best weight achievable
    79using only the kept jobs is the optimum of the whole instance. -/
    80axiom optimumOn_keep (I : Instance) : optimumOn I (keep I) = optimum I
    81
    82/-- **Observation 5.** At most `p_max ^ 2 * m ^ 2` kept jobs are alive at any one
    83instant — a bound in the parameter alone, with no dependence on the number of jobs. -/
    84axiom card_keep_alive_le (I : Instance) (t : ℕ) :
    85 ((keep I).filter fun j => Active t j).card ≤ I.pmax * I.pmax * (I.machines * I.machines)
    86
    87end Lax470956.Preprocessing
    88
    Show ProofShow Proof
    Formalization notes

    Discarding is modelled as a set of kept jobs together with the best weight achievable using only those, rather than as a second instance on a smaller job set. The two say the same thing, and the first states it without transporting an instance along a change of index type — which would make the statement about the transport as much as about the preprocessing.

    Ties in weight are broken by the job's index. "The mm best" has to be well defined, and some tie-break is needed to define it; the index is the tie-break a program would use, since it is the order the jobs arrive in. BetterBetter is the resulting strict linear order: heavier, or equally heavy and earlier.

    A job is kept when it is among the mm best for some machine it is eligible on, not for all of them. The exchange argument needs this: a job is discarded only when every machine that could run it already keeps mm better alternatives for its interval. It is also why the bound counts machines twice.

    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…