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

Parameters of the zoo's results

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

definition

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

    Definition

    The parameters in which the zoo states results, as functions of the instances.

    On the operations family and the batching family: the number nn of jobs, the number mm of machines, the largest processing time pmax⁡p_{\max} and weight wmax⁡w_{\max}, the numbers #p\#p, #r\#r, #w\#w, #d\#d of distinct processing times, release dates, weights and due dates, the total weight WW and the total processing time PP. The processing time of an operation is its time on the first machine, as in the field of processing times, and that of a job the sum over its operations. A weight is 11 and a due date 00 when the objective has none.

    On the operations family also:

    • the number of kinds of machines (Knop and Koutecký): machines of one kind have the same processing time for every operation, so this is the number of distinct columns of the matrix (pij)(p_{ij});
    • the rank of that matrix over the rationals (Chen, Marx, Ye and Zhang);
    • qmax⁡q_{\max}, the largest processing time of the last operation of a job (and the predicate that every job has a last operation of positive length), and χ\chi, the largest number of jobs whose last operations, ending at their due dates, overlap at one instant — for jobs completed just in time the intervals [dj−qj,dj)[d_j - q_j, d_j) (Heeger, Hermelin, Itzhaki, Schieber and Shabtay; ω\omega there);
    • the largest communication delay cc;
    • the speed ratio smax⁡/smin⁡s_{\max}/s_{\min} of uniform machines, the least over the speeds that represent the instance;
    • the width of the precedence order, the largest number of pairwise incomparable jobs;
    • the number τ\tau of forbidden times, the instants at which no job may start or end;
    • nmax⁡n_{\max}, the largest number of operations of a job;
    • the number gg of batches into which batch setups group the jobs;
    • with the threshold DD: the gap D−LPD - \mathrm{LP} to the optimum LP\mathrm{LP} of the linear relaxation [CS-LP] of the vertex-cover formulation of Correa and Schulz, as in Ambühl and Mastrolilli (2009). With PP the transitive closure of the precedence relation and i∥ji \parallel j for different jobs related in neither direction, it minimizes ∑jpjwj+∑(i,j)∈Ppiwj+∑i∥jδijpiwj\sum_j p_jw_j + \sum_{(i,j) \in P} p_iw_j + \sum_{i \parallel j} \delta_{ij}p_iw_j over δ≥0\delta \ge 0 with δij+δji≥1\delta_{ij} + \delta_{ji} \ge 1 for i∥ji \parallel j, δik+δkj≥1\delta_{ik} + \delta_{kj} \ge 1 for (i,j)∈P(i, j) \in P, j∥kj \parallel k, k∥ik \parallel i, and δil+δkj≥1\delta_{il} + \delta_{kj} \ge 1 for (i,j),(k,l)∈P(i, j), (k, l) \in P, j∥kj \parallel k, l∥il \parallel i. Its optimum equals those of the relaxations of Potts and of Chudak and Hochbaum (their Theorems 2 to 4); the parameter is ⌈D−LP⌉\lceil D - \mathrm{LP} \rceil, and 00 when negative;
    • with the threshold DD: the time window of job jj runs from its release date to its deadline, and also ends at DD for the makespan and at dj+Dd_j + D for the maximum lateness, since the decision version asks for that. The pathwidth pw(I)\mathrm{pw}(I) of the interval graph of the windows is the largest number of windows containing one instant, minus one, and the maximum slack is the largest window length minus processing time (Hanen and Munier Kordon). A window without end has length 00 here; it occurs only without deadlines and with another objective.

    On the batching family also pw(I)\mathrm{pw}(I) and the maximum slack, with the same windows.

    On single-machine scheduling with rejection: nn, #p\#p, pmax⁡p_{\max}, the number #e\#e of distinct rejection costs, the largest rejection cost emax⁡e_{\max}, and the number of accepted jobs, read as an instance quantity: the least number of jobs a feasible solution accepts, nn minus the most jobs whose rejection costs fit the budget. On P∣∣Cmin⁡P \mid\mid C_{\min}: nn and mm.

    Concept map
    58 concepts
    100%
    Conjunctive normal formAssembling problems from fieldsOne family for serial and parallel batchingBatching problems in three-field notationBatch scheduling on a single machineCommunication delaysBounds on the number of machines and jobsDeadlinesForbidden times and input encodingsInterruption as a field of parallel-machineschedulingScheduling kernelsMaximizing the minimum machine loadMachine sets and multiprocessor tasksConstraint modules and objectivesNon-preemptive scheduling on parallelmachinesCompletion-time objectivesOnline scheduling as a gameScheduling with operationsOne family for parallel machines and shopsOne family for parallel machines with andwithout preemptionParallel machinesProblems on parallel machines in three-fieldnotationParameters along embeddingsPrecedence constraints and time lagsPreemptive scheduling on parallel machinesPreemptive shop problems in three-fieldnotationPreemptive shop schedulingOptimization problems and embeddingsSingle-machine scheduling with rejectionRelease datesPreemption with restarts on parallelmachinesParameters of the zoo's resultsThe kinds of results on scheduling problemsA single server with setup timesNo-idle shops and batch setup timesOne family for shops with and withoutpreemptionShop problems in three-field notationShop schedulingThreshold reductions between objectivesTransportation delays and a transport robotScheduling problems as parameterizedproblems on wordsParameters of scheduling problemsBinary encoding of an input and a certificateThe complexity class NPThe complexity class PFixed-Parameter Time on the Word RAMFPT-Reductions, FPT, Hardness andCompletenessFinite Relational StructuresFirst-Order Formulas and the Classes Σ_tand Π_tModel Checking and Weighted FaginDefinabilityThe W-Hierarchy and the A-HierarchyNP-Hardness of a Problem on Words ofNumbersBinary encoding of finite wordsPolynomial-time computation by a wordRAMPolynomial-time computation by a TuringmachineThe word RAMComputing a function within a time boundParameterized Problems andFPT-Reductions on a Word RAM
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    Lean source view on GitHub

    1import Lax434175.OperationsFamily
    2import Lax434175.BatchFamily
    3import Lax434175.ZooParameters
    4import Lax434175.Parameters
    5import Lax434175.Results
    6import Lax434175.Rejection
    7import Lax434175.MachineCovering
    8import Mathlib.LinearAlgebra.Matrix.Rank
    9
    10/-!
    11---
    12title: Parameters of the zoo's results
    13type: definition
    14---
    15The parameters in which the zoo states results, as functions of the instances.
    16
    17On the operations family and the batching family: the number nn of jobs, the
    18number mm of machines, the largest processing time pmax⁡p_{\max} and weight
    19wmax⁡w_{\max}, the numbers #p\#p, #r\#r, #w\#w, #d\#d of distinct processing times,
    20release dates, weights and due dates, the total weight WW and the total
    21processing time PP. The processing time of an operation is its time on the
    22first machine, as in the field of processing times, and that of a job the sum
    23over its operations. A weight is 11 and a due date 00 when the objective has
    24none.
    25
    26On the operations family also:
    27
    28- the number of *kinds* of machines (Knop and Koutecký): machines of one kind
    29 have the same processing time for every operation, so this is the number of
    30 distinct columns of the matrix (pij)(p_{ij});
    31- the *rank* of that matrix over the rationals (Chen, Marx, Ye and Zhang);
    32- qmax⁡q_{\max}, the largest processing time of the last operation of a job (and the
    33 predicate that every job has a last operation of positive length), and
    34 χ\chi, the largest number of jobs whose last operations, ending at their due
    35 dates, overlap at one instant — for jobs completed just in time the
    36 intervals [dj−qj,dj)[d_j - q_j, d_j) (Heeger, Hermelin, Itzhaki, Schieber and
    37 Shabtay; ω\omega there);
    38- the largest communication delay cc;
    39- the speed ratio smax⁡/smin⁡s_{\max}/s_{\min} of uniform machines, the least over the
    40 speeds that represent the instance;
    41- the width of the precedence order, the largest number of pairwise
    42 incomparable jobs;
    43- the number τ\tau of forbidden times, the instants at which no job may start
    44 or end;
    45- nmax⁡n_{\max}, the largest number of operations of a job;
    46- the number gg of batches into which batch setups group the jobs;
    47- with the threshold DD: the gap D−LPD - \mathrm{LP} to the optimum
    48 LP\mathrm{LP} of the linear relaxation [CS-LP] of the vertex-cover formulation
    49 of Correa and Schulz, as in Ambühl and Mastrolilli (2009). With PP the
    50 transitive closure of the precedence relation and i∥ji \parallel j for
    51 different jobs related in neither direction, it minimizes
    52 ∑jpjwj+∑(i,j)∈Ppiwj+∑i∥jδijpiwj\sum_j p_jw_j + \sum_{(i,j) \in P} p_iw_j + \sum_{i \parallel j} \delta_{ij}p_iw_j
    53 over δ≥0\delta \ge 0 with δij+δji≥1\delta_{ij} + \delta_{ji} \ge 1 for i∥ji \parallel j,
    54 δik+δkj≥1\delta_{ik} + \delta_{kj} \ge 1 for (i,j)∈P(i, j) \in P, j∥kj \parallel k,
    55 k∥ik \parallel i, and δil+δkj≥1\delta_{il} + \delta_{kj} \ge 1 for (i,j),(k,l)∈P(i, j), (k, l) \in P,
    56 j∥kj \parallel k, l∥il \parallel i. Its optimum equals those of the
    57 relaxations of Potts and of Chudak and Hochbaum (their Theorems 2 to 4); the
    58 parameter is ⌈D−LP⌉\lceil D - \mathrm{LP} \rceil, and 00 when negative;
    59- with the threshold DD: the time window of job jj runs from its release date
    60 to its deadline, and also ends at DD for the makespan and at dj+Dd_j + D for the
    61 maximum lateness, since the decision version asks for that. The pathwidth
    62 pw(I)\mathrm{pw}(I) of the interval graph of the windows is the largest number of
    63 windows containing one instant, minus one, and the maximum slack is the largest
    64 window length minus processing time (Hanen and Munier Kordon). A window without
    65 end has length 00 here; it occurs only without deadlines and with another
    66 objective.
    67
    68On the batching family also pw(I)\mathrm{pw}(I) and the maximum slack, with the
    69same windows.
    70
    71On single-machine scheduling with rejection: nn, #p\#p, pmax⁡p_{\max}, the number
    72#e\#e of distinct rejection costs, the largest rejection cost emax⁡e_{\max}, and the
    73number of accepted jobs, read as an instance quantity: the least number of jobs
    74a feasible solution accepts, nn minus the most jobs whose rejection costs fit
    75the budget. On P∣∣Cmin⁡P \mid\mid C_{\min}: nn and mm.
    76-/
    77
    78namespace Lax434175.ResultParameters
    79open Lax434175 Lax434175.Problems Lax434175.Assembly Lax434175.Parameters
    80open Lax434175.Results
    81
    82/-- The sum of two parameters. -/
    83def plus {P : Problem} (κ κ' : Parameter P) : Parameter P := fun x => κ x + κ' x
    84
    85/-- The largest number of the intervals `[a i, b i)` that contain one instant. -/
    86noncomputable def overlap {n : ℕ} (a b : Fin n → ℕ∞) : ℕ :=
    87 sSup {k | ∃ t : ℕ, k = (Finset.univ.filter fun j => a j ≤ t ∧ (t : ℕ∞) < b j).card}
    88
    89namespace Ops
    90
    91variable (s : Spec OperationsFamily.family)
    92
    93/-- The number of jobs. -/
    94def n : Parameter (problem _ s) := fun x => x.base.jobs
    95
    96/-- The number of machines. -/
    97def m : Parameter (problem _ s) := fun x => x.base.machines
    98
    99/-- The largest processing time of an operation. -/
    100def pmax : Parameter (problem _ s) := fun x =>
    101 Finset.univ.sup fun o : Operations.Op x.base => Operations.opTime x.base o
    102
    103/-- The number of distinct processing times of operations. -/
    104def numP : Parameter (problem _ s) := fun x =>
    105 (Finset.univ.image fun o : Operations.Op x.base => Operations.opTime x.base o).card
    106
    107/-- The number of distinct release dates. -/
    108def numR : Parameter (problem _ s) := fun x => ZooParameters.distinct x.base.r
    109
    110/-- The number of distinct weights. -/
    111def numW : Parameter (problem _ s) := fun x =>
    112 ZooParameters.weights Operations.kernel s.objective x.base x.objectiveData
    113
    114/-- The number of distinct due dates. -/
    115def numD : Parameter (problem _ s) := fun x =>
    116 ZooParameters.dueDates Operations.kernel s.objective x.base x.objectiveData
    117
    118/-- The weight of a job. -/
    119def weight (x : Inst _ s) (j : Fin x.base.jobs) : ℕ :=
    120 Objectives.weight (K := Operations.kernel) s.objective x.objectiveData j
    121
    122/-- The due date of a job. -/
    123def due (x : Inst _ s) (j : Fin x.base.jobs) : ℕ :=
    124 Objectives.dueDate (K := Operations.kernel) s.objective x.objectiveData j
    125
    126/-- The largest weight. -/
    127def wmax : Parameter (problem _ s) := fun x => Finset.univ.sup (weight s x)
    128
    129/-- The total weight. -/
    130def totalW : Parameter (problem _ s) := fun x => ∑ j, weight s x j
    131
    132/-- The processing time of a job: the sum over its operations. -/
    133def ptime (x : Operations.Inst) (j : Fin x.jobs) : ℕ :=
    134 ∑ k : Fin (x.ops j), Operations.opTime x ⟨j, k⟩
    135
    136/-- The total processing time. -/
    137def totalP : Parameter (problem _ s) := fun x => ∑ j, ptime x.base j
    138
    139/-- The number of kinds of machines: distinct columns of the matrix of
    140processing times. -/
    141def kinds : Parameter (problem _ s) := fun x =>
    142 (Finset.univ.image fun i : Fin x.base.machines =>
    143 fun o : Operations.Op x.base => x.base.p o.1 o.2 i).card
    144
    145/-- The rank of the matrix of processing times. -/
    146noncomputable def rank : Parameter (problem _ s) := fun x =>
    147 (Matrix.of fun (o : Operations.Op x.base) (i : Fin x.base.machines) =>
    148 (x.base.p o.1 o.2 i : ℚ)).rank
    149
    150/-- The processing time of the last operation of a job, `0` without operations. -/
    151def lastTime (x : Operations.Inst) (j : Fin x.jobs) : ℕ :=
    152 if h : 0 < x.ops j then Operations.opTime x ⟨j, ⟨x.ops j - 1, by omega⟩⟩ else 0
    153
    154/-- Every job has a last operation of positive length. -/
    155def lastPositive (x : (problem _ s).Inst) : Prop := ∀ j, 0 < lastTime x.base j
    156
    157/-- `q_max`: the largest processing time of a last operation. -/
    158def qmax : Parameter (problem _ s) := fun x => Finset.univ.sup (lastTime x.base)
    159
    160/-- `χ`: the largest number of jobs whose last operations, ending at their due
    161dates, overlap at one instant. -/
    162noncomputable def chi : Parameter (problem _ s) := fun x =>
    163 overlap (fun j => ((due s x j - lastTime x.base j : ℕ) : ℕ∞)) (fun j => (due s x j : ℕ∞))
    164
    165/-- The largest communication delay. -/
    166noncomputable def cmax : Parameter (problem _ s) := fun x =>
    167 sSup {c | ∃ i j, CommunicationDelays.view (s.module .communicationDelays)
    168 (x.data .communicationDelays : CommunicationDelays.Data _ x.base.toPar) i j c}
    169
    170/-- The speed ratio `s_max / s_min` of uniform machines: the least over the
    171speeds representing the instance. -/
    172noncomputable def speedRatio (x : Inst _ s) : ℝ :=
    173 sInf {r | ∃ (q : Operations.Op x.base → ℕ) (sp : Fin x.base.machines → ℕ),
    174 (∀ o i, 0 < sp i ∧ x.base.p o.1 o.2 i * sp i = q o) ∧
    175 ∀ i i', (sp i : ℝ) ≤ r * sp i'}
    176
    177/-- The precedence relation of an instance. -/
    178def prec (x : Inst _ s) (i j : Fin x.base.jobs) : Prop :=
    179 (s.module .precedence).order.view (x.data .precedence).1 i j
    180
    181/-- The width of the precedence order: the largest set of jobs no two of which
    182are related by the transitive closure. -/
    183noncomputable def width : Parameter (problem _ s) := fun x =>
    184 sSup {k | ∃ S : Finset (Fin x.base.jobs), S.card = k ∧
    185 ∀ i ∈ S, ∀ j ∈ S, ¬ Relation.TransGen (prec s x) i j}
    186
    187/-- The end of the time window of a job with the threshold `D`: its deadline,
    188and also `D` for the makespan and `d_j + D` for the maximum lateness. -/
    189noncomputable def windowEnd (x : Inst _ s) (D : ℤ) (j : Fin x.base.jobs) : ℕ∞ :=
    190 min (Deadlines.view (K := Operations.kernel) (s.module .deadlines) (x.data .deadlines) j)
    191 (match s.objective with
    192 | .makespan => (D.toNat : ℕ∞)
    193 | .lmax => (((due s x j : ℤ) + D).toNat : ℕ∞)
    194 | _ => ⊤)
    195
    196/-- `pw(I)`: the largest number of time windows containing one instant, minus
    197one. -/
    198noncomputable def pw : TParameter (problem _ s) := fun x D =>
    199 overlap (fun j => (x.base.r j : ℕ∞)) (windowEnd s x D) - 1
    200
    201/-- The maximum slack: the largest window length minus processing time. -/
    202noncomputable def slackmax : TParameter (problem _ s) := fun x D =>
    203 Finset.univ.sup fun j => (windowEnd s x D j).toNat - ptime x.base j - x.base.r j
    204
    205/-- `τ`: the number of forbidden times, the instants at which no job may start or end. -/
    206def tau : Parameter (problem _ s) := fun x =>
    207 (ForbiddenTimes.view (s.module .forbiddenTimes) (x.data .forbiddenTimes)).dedup.length
    208
    209/-- `n_max`: the largest number of operations of a job. -/
    210def nmax : Parameter (problem _ s) := fun x => Finset.univ.sup x.base.ops
    211
    212/-- `g`: the number of batches into which batch setups group the jobs. -/
    213def numBatches : Parameter (problem _ s) := fun x =>
    214 (Finset.univ.image fun j => ShopExtras.BatchSetups.batch (x := x.base.toShop)
    215 (s.module .batchSetups) (x.data .batchSetups) j).card
    216
    217/-- Two different jobs related in neither direction by the precedence order. -/
    218def Incomparable (x : Inst _ s) (i j : Fin x.base.jobs) : Prop :=
    219 i ≠ j ∧ ¬ Relation.TransGen (prec s x) i j ∧ ¬ Relation.TransGen (prec s x) j i
    220
    221/-- A feasible solution of [CS-LP] (Correa and Schulz; Ambühl and Mastrolilli 2009). -/
    222def CSFeasible (x : Inst _ s) (δ : Fin x.base.jobs → Fin x.base.jobs → ℝ) : Prop :=
    223 (∀ i j, 0 ≤ δ i j) ∧
    224 (∀ i j, Incomparable s x i j → 1 ≤ δ i j + δ j i) ∧
    225 (∀ i j k, Relation.TransGen (prec s x) i j → Incomparable s x j k → Incomparable s x k i →
    226 1 ≤ δ i k + δ k j) ∧
    227 (∀ i j k l, Relation.TransGen (prec s x) i j → Incomparable s x j k →
    228 Relation.TransGen (prec s x) k l → Incomparable s x l i → 1 ≤ δ i l + δ k j)
    229
    230open Classical in
    231/-- The objective of [CS-LP]. -/
    232noncomputable def csValue (x : Inst _ s) (δ : Fin x.base.jobs → Fin x.base.jobs → ℝ) : ℝ :=
    233 ∑ j, (ptime x.base j * weight s x j : ℝ) +
    234 ∑ i, ∑ j, (if Relation.TransGen (prec s x) i j then (ptime x.base i * weight s x j : ℝ)
    235 else if Incomparable s x i j then δ i j * ptime x.base i * weight s x j else 0)
    236
    237/-- The optimum of [CS-LP], a lower bound on the total weighted completion time
    238on one machine. -/
    239noncomputable def csLP (x : Inst _ s) : ℝ :=
    240 sInf (csValue s x '' {δ | CSFeasible s x δ})
    241
    242/-- `D − LP`: the threshold minus the optimum of [CS-LP], rounded up, and `0`
    243when negative. -/
    244noncomputable def gapLP : TParameter (problem _ s) := fun x D => ⌈(D : ℝ) - csLP s x⌉₊
    245
    246end Ops
    247
    248namespace Batch
    249
    250variable (s : Spec BatchFamily.family)
    251
    252/-- The number of jobs. -/
    253def n : Parameter (problem _ s) := fun x => x.base.jobs
    254
    255/-- The largest processing time. -/
    256def pmax : Parameter (problem _ s) := fun x => Finset.univ.sup x.base.p
    257
    258/-- The number of distinct processing times. -/
    259def numP : Parameter (problem _ s) := fun x => ZooParameters.distinct x.base.p
    260
    261/-- The number of distinct release dates. -/
    262def numR : Parameter (problem _ s) := fun x => ZooParameters.distinct x.base.r
    263
    264/-- The number of distinct weights. -/
    265def numW : Parameter (problem _ s) := fun x =>
    266 ZooParameters.weights BatchFamily.kernel s.objective x.base x.objectiveData
    267
    268/-- The number of distinct due dates. -/
    269def numD : Parameter (problem _ s) := fun x =>
    270 ZooParameters.dueDates BatchFamily.kernel s.objective x.base x.objectiveData
    271
    272/-- The weight of a job. -/
    273def weight (x : Inst _ s) (j : Fin x.base.jobs) : ℕ :=
    274 Objectives.weight (K := BatchFamily.kernel) s.objective x.objectiveData j
    275
    276/-- The largest weight. -/
    277def wmax : Parameter (problem _ s) := fun x => Finset.univ.sup (weight s x)
    278
    279/-- The total weight. -/
    280def totalW : Parameter (problem _ s) := fun x => ∑ j, weight s x j
    281
    282/-- The total processing time. -/
    283def totalP : Parameter (problem _ s) := fun x => ∑ j, x.base.p j
    284
    285/-- The due date of a job. -/
    286def due (x : Inst _ s) (j : Fin x.base.jobs) : ℕ :=
    287 Objectives.dueDate (K := BatchFamily.kernel) s.objective x.objectiveData j
    288
    289/-- The end of the time window of a job with the threshold `D`, as on the
    290operations family. -/
    291noncomputable def windowEnd (x : Inst _ s) (D : ℤ) (j : Fin x.base.jobs) : ℕ∞ :=
    292 min (Deadlines.view (K := BatchFamily.kernel) (s.module (.field .deadlines))
    293 (x.data (.field .deadlines)) j)
    294 (match s.objective with
    295 | .makespan => (D.toNat : ℕ∞)
    296 | .lmax => (((due s x j : ℤ) + D).toNat : ℕ∞)
    297 | _ => ⊤)
    298
    299/-- `pw(I)`: the largest number of time windows containing one instant, minus
    300one. -/
    301noncomputable def pw : TParameter (problem _ s) := fun x D =>
    302 overlap (fun j => (x.base.r j : ℕ∞)) (windowEnd s x D) - 1
    303
    304/-- The maximum slack: the largest window length minus processing time. -/
    305noncomputable def slackmax : TParameter (problem _ s) := fun x D =>
    306 Finset.univ.sup fun j => (windowEnd s x D j).toNat - x.base.p j - x.base.r j
    307
    308end Batch
    309
    310namespace Reject
    311
    312/-- The number of jobs. -/
    313def n : Parameter Rejection.problem := fun x => x.jobs
    314
    315/-- The number of distinct processing times. -/
    316def numP : Parameter Rejection.problem := fun x => ZooParameters.distinct x.p
    317
    318/-- The largest processing time. -/
    319def pmax : Parameter Rejection.problem := fun x => Finset.univ.sup x.p
    320
    321/-- The number of distinct rejection costs. -/
    322def numE : Parameter Rejection.problem := fun x => ZooParameters.distinct x.e
    323
    324/-- The largest rejection cost. -/
    325def emax : Parameter Rejection.problem := fun x => Finset.univ.sup x.e
    326
    327/-- The least number of jobs a feasible solution accepts: `n` minus the most
    328jobs whose rejection costs fit the budget. -/
    329noncomputable def accepted : Parameter Rejection.problem := fun x =>
    330 x.jobs - sSup {k | ∃ S : Finset (Fin x.jobs), S.card = k ∧ ∑ j ∈ S, x.e j ≤ x.budget}
    331
    332end Reject
    333
    334namespace Cover
    335
    336/-- The number of jobs. -/
    337def n : Parameter MachineCovering.problem := fun x => x.jobs
    338
    339/-- The number of machines. -/
    340def m : Parameter MachineCovering.problem := fun x => x.machines
    341
    342end Cover
    343
    344end Lax434175.ResultParameters
    345

    Discussion

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

    Loading discussion…