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

Problems on parallel machines in three-field notation

Lax434175.ParallelProblems · concepts/Lax434175/ParallelProblems.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

    The family of problems of a machine model on parallel machines has the constraint fields machine environment, number of machines, number of jobs, processing times, machine sets, release dates, deadlines, precedence constraints with time lags, communication delays, a server, forbidden times and the input encoding, and the completion-time objectives.

    A problem α∣β∣γ\alpha \mid \beta \mid \gamma of the three-field notation is one specification of this family: α\alpha is the machine environment and count, β\beta lists the values of the constraint fields, and γ\gamma is the objective. The entry pmtn\mathrm{pmtn} of β\beta selects the preemptive machine model, and the entry restarts the model with restarts; the concept on one family for parallel machines joins the three models into a single family with an interruption field. For example 1∣∣∑Cj1 \mid\mid \sum C_j, 1∣rj∣∑Cj1 \mid r_j \mid \sum C_j, P∣pj=1,chains∣Cmax⁡P \mid p_j = 1, \mathrm{chains} \mid C_{\max} and R∣rj,prec∣∑wjTjR \mid r_j, \mathrm{prec} \mid \sum w_j T_j are the specifications below.

    Theorem. In every machine model, a specification that is field by field a special case of another describes a special case of the other's problem, and a specification that reduces to another describes a problem whose decision version reduces to that of the other. The same holds for reductions through flow time in every machine model in which jobs start no later than they complete. In particular 1∣∣∑Cj1 \mid\mid \sum C_j is a special case of R∣rj,prec∣∑wjTjR \mid r_j, \mathrm{prec} \mid \sum w_j T_j.

    Concept map
    21 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

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

    Lean source view on GitHub

    1import Lax434175.Assembly
    2import Lax434175.Counts
    3import Lax434175.ReleaseDates
    4import Lax434175.Deadlines
    5import Lax434175.Precedence
    6import Lax434175.Thresholds
    7import Lax434175.MachineSets
    8import Lax434175.CommunicationDelays
    9import Lax434175.Servers
    10import Lax434175.ForbiddenTimes
    11import Lax434175.Restarts
    12import Lax434175.Nonpreemptive
    13import Lax434175.Preemptive
    14
    15/-!
    16---
    17title: Problems on parallel machines in three-field notation
    18type: theorem
    19---
    20The family of problems of a machine model on parallel machines has the
    21constraint fields machine environment, number of machines, number of jobs,
    22processing times, machine sets, release dates, deadlines, precedence
    23constraints with time lags, communication delays, a server, forbidden times
    24and the input encoding, and the
    25completion-time objectives.
    26
    27A problem α∣β∣γ\alpha \mid \beta \mid \gamma of the three-field notation is one
    28specification of this family: α\alpha is the machine environment and count,
    29β\beta lists the values of the constraint fields, and γ\gamma is the
    30objective. The entry pmtn\mathrm{pmtn} of β\beta selects the preemptive
    31machine model, and the entry restarts the model with restarts; the concept on
    32one family for parallel machines joins the three models into a single family
    33with an interruption field. For example 1∣∣∑Cj1 \mid\mid \sum C_j, 1∣rj∣∑Cj1 \mid r_j \mid \sum C_j,
    34P∣pj=1,chains∣Cmax⁡P \mid p_j = 1, \mathrm{chains} \mid C_{\max} and
    35R∣rj,prec∣∑wjTjR \mid r_j, \mathrm{prec} \mid \sum w_j T_j are the specifications below.
    36
    37**Theorem.** In every machine model, a specification that is field by field a
    38special case of another describes a special case of the other's problem, and
    39a specification that reduces to another describes a problem whose decision
    40version reduces to that of the other. The same holds for reductions through
    41flow time in every machine model in which jobs start no later than they
    42complete. In
    43particular 1∣∣∑Cj1 \mid\mid \sum C_j is a special case of
    44R∣rj,prec∣∑wjTjR \mid r_j, \mathrm{prec} \mid \sum w_j T_j.
    45-/
    46
    47namespace Lax434175.ParallelProblems
    48open Lax434175.Problems Lax434175.Kernels Lax434175.Modules Lax434175.Assembly
    49open Lax434175
    50
    51/-- The constraint fields of the family. -/
    52inductive FieldName
    53 | environment
    54 | machineCount
    55 | jobCount
    56 | processingTimes
    57 | machineSets
    58 | releaseDates
    59 | deadlines
    60 | precedence
    61 | communicationDelays
    62 | server
    63 | forbiddenTimes
    64 | encoding
    65 deriving DecidableEq
    66
    67instance : Fintype FieldName where
    68 elems := {.environment, .machineCount, .jobCount, .processingTimes, .machineSets, .releaseDates,
    69 .deadlines, .precedence, .communicationDelays, .server,
    70 .forbiddenTimes, .encoding}
    71 complete x := by cases x <;> decide
    72
    73/-- The problems of a machine model on parallel machines. -/
    74abbrev family (M : ParallelMachines.Model) : Family M.kernel :=
    75 Thresholds.family FieldName fun
    76 | .environment => ParallelMachines.environment M
    77 | .machineCount => Counts.module _ (ParallelMachines.machines M) 1
    78 | .jobCount => Counts.module _ M.kernel.jobs
    79 | .processingTimes => ParallelMachines.processingTimes M
    80 | .machineSets => MachineSets.module M
    81 | .releaseDates => ReleaseDates.module _
    82 | .deadlines => Deadlines.module _
    83 | .precedence => Precedence.module _ (ParallelMachines.machines M)
    84 | .communicationDelays => CommunicationDelays.module M
    85 | .server => Servers.parallel M
    86 | .forbiddenTimes => ForbiddenTimes.module _
    87 | .encoding => ForbiddenTimes.encoding _
    88
    89instance (M : ParallelMachines.Model) : Fintype (family M).ModuleName :=
    90 inferInstanceAs (Fintype FieldName)
    91
    92/-- The specification `α | β | γ` in a machine model. -/
    93def spec (M : ParallelMachines.Model) (environment : ParallelMachines.Environment)
    94 (machineCount : Counts.Bound := .any)
    95 (jobCount : Counts.Bound := .any)
    96 (machineSets : MachineSets.Value := .none)
    97 (processingTimes : ParallelMachines.ProcessingTimes := .arbitrary)
    98 (release : ReleaseDates.Value := .none)
    99 (deadline : Deadlines.Value := .none)
    100 (precedence : Precedence.Value := .none)
    101 (communicationDelays : CommunicationDelays.Value := .none)
    102 (server : Servers.Value := .none)
    103 (forbiddenTimes : ForbiddenTimes.Value := .none)
    104 (encoding : ForbiddenTimes.Encoding := .standard)
    105 (objective : Objectives.Value) : Spec (family M) where
    106 module
    107 | .environment => environment
    108 | .machineCount => machineCount
    109 | .jobCount => jobCount
    110 | .processingTimes => processingTimes
    111 | .machineSets => machineSets
    112 | .releaseDates => release
    113 | .deadlines => deadline
    114 | .precedence => precedence
    115 | .communicationDelays => communicationDelays
    116 | .server => server
    117 | .forbiddenTimes => forbiddenTimes
    118 | .encoding => encoding
    119 objective := objective
    120
    121/-- The non-preemptive problems. -/
    122abbrev nonpreemptive := family Nonpreemptive.model
    123
    124/-- The preemptive problems. -/
    125abbrev preemptive := family Preemptive.model
    126
    127/-- The problems with restarts. -/
    128abbrev restarts := family Restarts.model
    129
    130/-- `1 || ΣC_j` -/
    131def single_sumC : Spec nonpreemptive :=
    132 spec _ (environment := .identical) (machineCount := .atMost 1) (objective := .sumC)
    133
    134/-- `1 | r_j | ΣC_j` -/
    135def single_release_sumC : Spec nonpreemptive :=
    136 spec _ (environment := .identical) (machineCount := .atMost 1) (release := .releaseDates)
    137 (objective := .sumC)
    138
    139/-- `P | p_j = 1, chains | C_max` -/
    140def identical_unit_chains_makespan : Spec nonpreemptive :=
    141 spec _ (environment := .identical) (processingTimes := .unit) (precedence := ⟨.chains, .zero⟩)
    142 (objective := .makespan)
    143
    144/-- `R | r_j, prec | Σw_jT_j` -/
    145def unrelated_release_prec_sumWT : Spec nonpreemptive :=
    146 spec _ (environment := .unrelated) (release := .releaseDates) (precedence := ⟨.prec, .zero⟩)
    147 (objective := .sumWT)
    148
    149/-- `P | pmtn, r_j | L_max` -/
    150def identical_pmtn_release_lmax : Spec preemptive :=
    151 spec _ (environment := .identical) (release := .releaseDates) (objective := .lmax)
    152
    153axiom family_sound (M : ParallelMachines.Model) : (family M).Sound
    154
    155axiom specialCase_of_le (M : ParallelMachines.Model) {s t : Spec (family M)} :
    156 s.le t → SpecialCase (problem (family M) s) (problem (family M) t)
    157
    158axiom reducible_of_reduces (M : ParallelMachines.Model) {s t : Spec (family M)} :
    159 Thresholds.Reduces s t → Reducible (problem (family M) s) (problem (family M) t)
    160
    161axiom reducible_of_reducesThroughFlow (M : ParallelMachines.Model)
    162 (h : M.kernel.StartsBeforeCompletion) {s t : Spec (family M)} :
    163 Thresholds.ReducesThroughFlow s t → Reducible (problem (family M) s) (problem (family M) t)
    164
    165axiom single_sumC_specialCase :
    166 SpecialCase (problem nonpreemptive single_sumC)
    167 (problem nonpreemptive unrelated_release_prec_sumWT)
    168
    169end Lax434175.ParallelProblems
    170
    Show 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…