Interval scheduling with eligible machine sets as a zoo problem
Lax434175.IsemLink · concepts/Lax434175/IsemLink.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
An instance of interval scheduling with eligible machine sets has jobs and machines; job has a processing time , a deadline , a weight and a set of eligible machines. A schedule runs some of the jobs, each on an eligible machine during exactly , such that jobs on one machine do not overlap; the question is whether the scheduled jobs can have weight at least .
Read the same data as an instance of : identical machines, job with processing time , due date , weight 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 if and only if the zoo instance has a schedule of cost at most .
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 by the word of the interval scheduling instance and , 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 , 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 ; 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 has the same answer as the zoo instance of its padding with threshold , where 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 parameterized by the number of machines.
Multicoloured Clique fpt-reduces to the former (Theorem 1 of lax-888481), so composing the two reductions makes W[1]-hard for the number of machines; the composition of two such reductions is not stated here.
Concept map
Evidence
This concept declares 6 statements. Each proof establishes one of them relative to its assumptions.
1 allEligible_pad proven
2 byMachines_fptReduces_jitByMachines proven
3 fpt_jitByMachinesAndPmax proven
4 hasWeight_iff proven
5 hasWeight_iff_zoo proven
6 hasWeight_pad proven
Lean source view on GitHub
| 1 | import Lax888481.Theorem3 |
| 2 | import Lax434175.ParallelProblems |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Interval scheduling with eligible machine sets as a zoo problem |
| 7 | type: theorem |
| 8 | --- |
| 9 | An instance of interval scheduling with eligible machine sets has jobs and |
| 10 | machines; job has a processing time , a deadline |
| 11 | , a weight and a set of eligible machines. A schedule runs some of |
| 12 | the jobs, each on an eligible machine during exactly , such |
| 13 | that jobs on one machine do not overlap; the question is whether the |
| 14 | scheduled jobs can have weight at least . |
| 15 | |
| 16 | Read the same data as an instance of : identical |
| 17 | machines, job with processing time , due date , weight and |
| 18 | machine set the eligible machines. Here every job is scheduled, and the cost |
| 19 | is the total weight of the jobs that do not complete exactly at their due |
| 20 | date. |
| 21 | |
| 22 | **Theorem.** If every job has an eligible machine, the interval scheduling |
| 23 | instance has a schedule of weight at least if and only if the zoo instance |
| 24 | has a schedule of cost at most . |
| 25 | |
| 26 | The jobs completing at their due dates form the interval schedule; conversely |
| 27 | the jobs left out of an interval schedule are run one after another, on an |
| 28 | eligible machine each, after all due dates. |
| 29 | |
| 30 | Encoding the zoo instance and threshold by the word of the |
| 31 | interval scheduling instance and , the zoo problem on the instances in |
| 32 | which every job has an eligible machine is a parameterized problem on words. |
| 33 | |
| 34 | **Theorem.** This problem, parameterized by , is |
| 35 | fixed-parameter tractable. |
| 36 | |
| 37 | An interval scheduling instance may have jobs without an eligible machine, |
| 38 | which no schedule runs. Padding the instance gives each of them one new |
| 39 | machine, eligible for them alone, and weight ; the other jobs keep their |
| 40 | data. The number of machines grows by one. |
| 41 | |
| 42 | **Theorem.** Padding keeps the answer, and in the padded instance every job |
| 43 | has an eligible machine. Hence every interval scheduling instance with |
| 44 | threshold has the same answer as the zoo instance of its padding with |
| 45 | threshold , where are the padded weights. |
| 46 | |
| 47 | Padding is computed on words by a word RAM program in one pass, linear in the |
| 48 | length of the word, and raises the number of machines by one. |
| 49 | |
| 50 | **Theorem.** Interval scheduling with eligible machine sets, parameterized by |
| 51 | the number of machines, fpt-reduces to |
| 52 | parameterized by the number of machines. |
| 53 | |
| 54 | Multicoloured Clique fpt-reduces to the former (Theorem 1 of lax-888481), so |
| 55 | composing the two reductions makes W[1]-hard |
| 56 | for the number of machines; the composition of two such reductions is not |
| 57 | stated here. |
| 58 | -/ |
| 59 | |
| 60 | namespace Lax434175.IsemLink |
| 61 | open Lax434175 Lax434175.Problems Lax434175.Assembly |
| 62 | open Lax888481.Scheduling Lax888481.InstanceEncoding Lax888481.SchedulingProblems |
| 63 | open Lax888481.ParameterizedComplexity |
| 64 | |
| 65 | /-- `P | M_j | Σ w_j Z_j` -/ |
| 66 | def jitSets : Spec ParallelProblems.nonpreemptive := |
| 67 | ParallelProblems.spec _ .identical (machineSets := .sets) (objective := .sumWZ) |
| 68 | |
| 69 | /-- The machine instance of an interval scheduling instance. -/ |
| 70 | def 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. -/ |
| 77 | def 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. -/ |
| 97 | def totalWeight (I : Instance) : ℕ := ∑ j, I.w j |
| 98 | |
| 99 | /-- Every job has an eligible machine. -/ |
| 100 | def AllEligible (I : Instance) : Prop := ∀ j, (I.eligible j).Nonempty |
| 101 | |
| 102 | axiom 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 |
| 107 | instances in which every job has an eligible machine, parameterized by the |
| 108 | number of machines plus the largest processing time. -/ |
| 109 | def 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 | |
| 115 | axiom fpt_jitByMachinesAndPmax : FPT jitByMachinesAndPmax |
| 116 | |
| 117 | /-- `P | M_j | Σ w_j Z_j` on the words of interval scheduling, for the |
| 118 | instances in which every job has an eligible machine, parameterized by the |
| 119 | number of machines. -/ |
| 120 | def 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 |
| 127 | machine gets the new last machine and weight `0`. -/ |
| 128 | def 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 | |
| 139 | axiom allEligible_pad (I : Instance) : AllEligible (pad I) |
| 140 | |
| 141 | axiom hasWeight_pad (I : Instance) (W : ℕ) : I.HasWeight W ↔ (pad I).HasWeight W |
| 142 | |
| 143 | axiom byMachines_fptReduces_jitByMachines : byMachines ≤fpt jitByMachines |
| 144 | |
| 145 | axiom hasWeight_iff_zoo (I : Instance) (W : ℕ) : |
| 146 | I.HasWeight W ↔ |
| 147 | (problem _ jitSets).Decides (toZoo (pad I)) (((totalWeight (pad I) : ℤ) - W : ℤ) : ℚ) |
| 148 | |
| 149 | end Lax434175.IsemLink |
| 150 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments