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

Interval scheduling with eligible machine sets as a zoo problem

Lax434175.IsemLink · concepts/Lax434175/IsemLink.lean · lax-434175

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

    An instance of interval scheduling with eligible machine sets has nn jobs and mm machines; job jj has a processing time 1≤pj≤dj1 \le p_j \le d_j, a deadline djd_j, a weight wjw_j and a set of eligible machines. A schedule runs some of the jobs, each on an eligible machine during exactly [dj−pj,dj)[d_j - p_j, d_j), such that jobs on one machine do not overlap; the question is whether the scheduled jobs can have weight at least WW.

    Read the same data as an instance of P∣Mj∣∑wjZjP \mid M_j \mid \sum w_j Z_j: identical machines, job jj with processing time pjp_j, due date djd_j, weight wjw_j and machine set the eligible machines. Here every job is scheduled, and the cost is the total weight of the jobs that do not complete exactly at their due date.

    Theorem. If every job has an eligible machine, the interval scheduling instance has a schedule of weight at least WW if and only if the zoo instance has a schedule of cost at most ∑jwj−W\sum_j w_j - W.

    The jobs completing at their due dates form the interval schedule; conversely the jobs left out of an interval schedule are run one after another, on an eligible machine each, after all due dates.

    Encoding the zoo instance and threshold ∑jwj−W\sum_j w_j - W by the word of the interval scheduling instance and WW, the zoo problem on the instances in which every job has an eligible machine is a parameterized problem on words.

    Theorem. This problem, parameterized by m+pmax⁡m + p_{\max}, is fixed-parameter tractable.

    An interval scheduling instance may have jobs without an eligible machine, which no schedule runs. Padding the instance gives each of them one new machine, eligible for them alone, and weight 00; the other jobs keep their data. The number of machines grows by one.

    Theorem. Padding keeps the answer, and in the padded instance every job has an eligible machine. Hence every interval scheduling instance with threshold WW has the same answer as the zoo instance of its padding with threshold ∑jwj′−W\sum_j w'_j - W, where w′w' are the padded weights.

    Padding is computed on words by a word RAM program in one pass, linear in the length of the word, and raises the number of machines by one.

    Theorem. Interval scheduling with eligible machine sets, parameterized by the number of machines, fpt-reduces to P∣Mj∣∑wjZjP \mid M_j \mid \sum w_j Z_j parameterized by the number of machines.

    Multicoloured Clique fpt-reduces to the former (Theorem 1 of lax-888481), so composing the two reductions makes P∣Mj∣∑wjZjP \mid M_j \mid \sum w_j Z_j W[1]-hard for the number of machines; the composition of two such reductions is not stated here.

    Concept map
    29 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 allEligible_pad proven

    4 hasWeight_iff proven

    5 hasWeight_iff_zoo proven

    6 hasWeight_pad proven

    Lean source view on GitHub

    1import Lax888481.Theorem3
    2import Lax434175.ParallelProblems
    3
    4/-!
    5---
    6title: Interval scheduling with eligible machine sets as a zoo problem
    7type: theorem
    8---
    9An instance of interval scheduling with eligible machine sets has nn jobs and
    10mm machines; job jj has a processing time 1≤pj≤dj1 \le p_j \le d_j, a deadline
    11djd_j, a weight wjw_j and a set of eligible machines. A schedule runs some of
    12the jobs, each on an eligible machine during exactly [dj−pj,dj)[d_j - p_j, d_j), such
    13that jobs on one machine do not overlap; the question is whether the
    14scheduled jobs can have weight at least WW.
    15
    16Read the same data as an instance of P∣Mj∣∑wjZjP \mid M_j \mid \sum w_j Z_j: identical
    17machines, job jj with processing time pjp_j, due date djd_j, weight wjw_j and
    18machine set the eligible machines. Here every job is scheduled, and the cost
    19is the total weight of the jobs that do not complete exactly at their due
    20date.
    21
    22**Theorem.** If every job has an eligible machine, the interval scheduling
    23instance has a schedule of weight at least WW if and only if the zoo instance
    24has a schedule of cost at most ∑jwj−W\sum_j w_j - W.
    25
    26The jobs completing at their due dates form the interval schedule; conversely
    27the jobs left out of an interval schedule are run one after another, on an
    28eligible machine each, after all due dates.
    29
    30Encoding the zoo instance and threshold ∑jwj−W\sum_j w_j - W by the word of the
    31interval scheduling instance and WW, the zoo problem on the instances in
    32which every job has an eligible machine is a parameterized problem on words.
    33
    34**Theorem.** This problem, parameterized by m+pmax⁡m + p_{\max}, is
    35fixed-parameter tractable.
    36
    37An interval scheduling instance may have jobs without an eligible machine,
    38which no schedule runs. Padding the instance gives each of them one new
    39machine, eligible for them alone, and weight 00; the other jobs keep their
    40data. The number of machines grows by one.
    41
    42**Theorem.** Padding keeps the answer, and in the padded instance every job
    43has an eligible machine. Hence every interval scheduling instance with
    44threshold WW has the same answer as the zoo instance of its padding with
    45threshold ∑jwj′−W\sum_j w'_j - W, where w′w' are the padded weights.
    46
    47Padding is computed on words by a word RAM program in one pass, linear in the
    48length of the word, and raises the number of machines by one.
    49
    50**Theorem.** Interval scheduling with eligible machine sets, parameterized by
    51the number of machines, fpt-reduces to P∣Mj∣∑wjZjP \mid M_j \mid \sum w_j Z_j
    52parameterized by the number of machines.
    53
    54Multicoloured Clique fpt-reduces to the former (Theorem 1 of lax-888481), so
    55composing the two reductions makes P∣Mj∣∑wjZjP \mid M_j \mid \sum w_j Z_j W[1]-hard
    56for the number of machines; the composition of two such reductions is not
    57stated here.
    58-/
    59
    60namespace Lax434175.IsemLink
    61open Lax434175 Lax434175.Problems Lax434175.Assembly
    62open Lax888481.Scheduling Lax888481.InstanceEncoding Lax888481.SchedulingProblems
    63open Lax888481.ParameterizedComplexity
    64
    65/-- `P | M_j | Σ w_j Z_j` -/
    66def jitSets : Spec ParallelProblems.nonpreemptive :=
    67 ParallelProblems.spec _ .identical (machineSets := .sets) (objective := .sumWZ)
    68
    69/-- The machine instance of an interval scheduling instance. -/
    70def base (I : Instance) : ParallelMachines.Inst where
    71 jobs := I.jobs
    72 machines := I.machines
    73 p := fun j _ => I.p j
    74 r := fun _ => 0
    75
    76/-- The zoo instance of an interval scheduling instance. -/
    77def toZoo (I : Instance) : Inst ParallelProblems.nonpreemptive jitSets where
    78 base := base I
    79 data := fun i => by
    80 cases i
    81 · exact ()
    82 · exact ()
    83 · exact ()
    84 · exact ()
    85 · exact fun j i => i ∈ I.eligible j
    86 all_goals first | exact () | exact ((), ())
    87 admitted := fun i => by
    88 cases i
    89 · exact fun _ _ _ => rfl
    90 all_goals first | exact trivial | exact ⟨trivial, fun _ h => nomatch h⟩ | skip
    91 · exact fun _ => rfl
    92 all_goals first | exact trivial | exact ⟨fun _ _ h => h, trivial⟩
    93 objectiveData := (I.w, I.d)
    94 objectiveAdmitted := trivial
    95
    96/-- The total weight of the jobs. -/
    97def totalWeight (I : Instance) : ℕ := ∑ j, I.w j
    98
    99/-- Every job has an eligible machine. -/
    100def AllEligible (I : Instance) : Prop := ∀ j, (I.eligible j).Nonempty
    101
    102axiom hasWeight_iff (I : Instance) (hI : AllEligible I) (W : ℕ) :
    103 I.HasWeight W ↔
    104 (problem _ jitSets).Decides (toZoo I) (((totalWeight I : ℤ) - W : ℤ) : ℚ)
    105
    106/-- `P | M_j | Σ w_j Z_j` on the words of interval scheduling, for the
    107instances in which every job has an eligible machine, parameterized by the
    108number of machines plus the largest processing time. -/
    109def jitByMachinesAndPmax : Lax888481.ParameterizedComplexity.Problem where
    110 Domain := {x | ∃ I W, EncodesDecisionInstance x I W ∧ AllEligible I}
    111 Yes x := ∃ I W, EncodesDecisionInstance x I W ∧
    112 (problem _ jitSets).Decides (toZoo I) (((totalWeight I : ℤ) - W : ℤ) : ℚ)
    113 param x := machineCount x + pmaxOf x
    114
    115axiom fpt_jitByMachinesAndPmax : FPT jitByMachinesAndPmax
    116
    117/-- `P | M_j | Σ w_j Z_j` on the words of interval scheduling, for the
    118instances in which every job has an eligible machine, parameterized by the
    119number of machines. -/
    120def jitByMachines : Lax888481.ParameterizedComplexity.Problem where
    121 Domain := {x | ∃ I W, EncodesDecisionInstance x I W ∧ AllEligible I}
    122 Yes x := ∃ I W, EncodesDecisionInstance x I W ∧
    123 (problem _ jitSets).Decides (toZoo I) (((totalWeight I : ℤ) - W : ℤ) : ℚ)
    124 param x := machineCount x
    125
    126/-- The padding of an interval scheduling instance: a job without an eligible
    127machine gets the new last machine and weight `0`. -/
    128def pad (I : Instance) : Instance where
    129 jobs := I.jobs
    130 machines := I.machines + 1
    131 p := I.p
    132 d := I.d
    133 w := fun j => if (I.eligible j).Nonempty then I.w j else 0
    134 eligible := fun j => if (I.eligible j).Nonempty then (I.eligible j).map Fin.castSuccEmb
    135 else {Fin.last I.machines}
    136 p_pos := I.p_pos
    137 p_le_d := I.p_le_d
    138
    139axiom allEligible_pad (I : Instance) : AllEligible (pad I)
    140
    141axiom hasWeight_pad (I : Instance) (W : ℕ) : I.HasWeight W ↔ (pad I).HasWeight W
    142
    143axiom byMachines_fptReduces_jitByMachines : byMachines ≤fpt jitByMachines
    144
    145axiom hasWeight_iff_zoo (I : Instance) (W : ℕ) :
    146 I.HasWeight W ↔
    147 (problem _ jitSets).Decides (toZoo (pad I)) (((totalWeight (pad I) : ℤ) - W : ℤ) : ℚ)
    148
    149end Lax434175.IsemLink
    150
    Show ProofShow ProofShow ProofShow ProofShow ProofShow Proof

    Discussion

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

    Loading discussion…