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

Standard words into high-multiplicity words

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

    A high-multiplicity word lists every distinct job once, with its record, release date, weight and due date, preceded by the number of jobs that have them (StandardReadingStandardReading). It does not say which job is which, and it has no facts on pairs of jobs.

    Theorem. The standard reading determines the answer for every specification with high multiplicity. Two instances written by one high-multiplicity word have the same numbers of jobs and machines and the same global facts, and a bijection between their jobs keeps every record, release date, weight and due date; renaming the jobs along it maps the feasible schedules of one instance to those of the other, at the same cost.

    A program reads the standard word of an instance without facts on pairs of jobs and writes the high-multiplicity word of the same instance: for every job it counts the jobs with the same record, release date, weight and due date, and it writes the distinct tuples in increasing order. It runs in polynomial time on every word.

    Theorem. Let s≤ts \le t, where ss has the standard encoding, no precedence constraints and no communication delays, and tt has high multiplicity. Then NP-hardness goes up from ss to tt, and so does W[t]-hardness for parameters κs\kappa_s of ss and κt\kappa_t of tt, if on every instance written by a high-multiplicity word of the lift of an instance xx of ss, κt\kappa_t is at most a computable function of κs(x)\kappa_s(x). Being in P goes down from tt to ss, and so does fixed-parameter tractability under the same bound, for a parameter of ss computable in polynomial time.

    Strong NP-hardness is not carried: a high-multiplicity word can be much shorter than the standard word of the same instance, so numbers that are small for the standard word can be large for the high-multiplicity word.

    Theorem. Along P∣∣Cmax⁡→P∣HM∣Cmax⁡P \mid\mid C_{\max} \to P \mid HM \mid C_{\max}, NP-hardness and W[t]-hardness for the number of machines go up, and fixed-parameter tractability for the number of distinct processing times goes down. Here the number of distinct processing times of P∣∣Cmax⁡P \mid\mid C_{\max} is computed in polynomial time by writing the high-multiplicity word and computing it there, which fixed-parameter tractability of P∣HM∣Cmax⁡P \mid HM \mid C_{\max} includes.

    Concept map
    62 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 encodingsStandard words into high-multiplicity wordsInterruption 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 embeddingsResults along special casesSingle-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 schedulingThe standard reading of scheduling instancesand schedulesThreshold reductions between objectivesTransportation delays and a transport robotScheduling problems as parameterizedproblems on wordsThe Scheduling Zoo, non-preemptiveproblems on parallel machinesParameters 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 A
    Evidence

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

    Lean source view on GitHub

    1import Lax434175.Propagation
    2import Lax434175.ZooParallel
    3
    4/-!
    5---
    6title: Standard words into high-multiplicity words
    7type: theorem
    8---
    9A high-multiplicity word lists every distinct job once, with its record, release
    10date, weight and due date, preceded by the number of jobs that have them
    11(`StandardReading`). It does not say which job is which, and it has no facts on
    12pairs of jobs.
    13
    14**Theorem.** The standard reading determines the answer for every specification
    15with high multiplicity. Two instances written by one high-multiplicity word have
    16the same numbers of jobs and machines and the same global facts, and a bijection
    17between their jobs keeps every record, release date, weight and due date;
    18renaming the jobs along it maps the feasible schedules of one instance to those
    19of the other, at the same cost.
    20
    21A program reads the standard word of an instance without facts on pairs of jobs
    22and writes the high-multiplicity word of the same instance: for every job it
    23counts the jobs with the same record, release date, weight and due date, and it
    24writes the distinct tuples in increasing order. It runs in polynomial time on
    25every word.
    26
    27**Theorem.** Let s≤ts \le t, where ss has the standard encoding, no precedence
    28constraints and no communication delays, and tt has high multiplicity. Then
    29NP-hardness goes up from ss to tt, and so does W[t]-hardness for parameters
    30κs\kappa_s of ss and κt\kappa_t of tt, if on every instance written by a
    31high-multiplicity word of the lift of an instance xx of ss, κt\kappa_t is at
    32most a computable function of κs(x)\kappa_s(x). Being in P goes down from tt to
    33ss, and so does fixed-parameter tractability under the same bound, for a
    34parameter of ss computable in polynomial time.
    35
    36Strong NP-hardness is not carried: a high-multiplicity word can be much shorter
    37than the standard word of the same instance, so numbers that are small for the
    38standard word can be large for the high-multiplicity word.
    39
    40**Theorem.** Along P∣∣Cmax⁡→P∣HM∣Cmax⁡P \mid\mid C_{\max} \to P \mid HM \mid C_{\max}, NP-hardness
    41and W[t]-hardness for the number of machines go up, and fixed-parameter
    42tractability for the number of distinct processing times goes down. Here the
    43number of distinct processing times of P∣∣Cmax⁡P \mid\mid C_{\max} is computed in
    44polynomial time by writing the high-multiplicity word and computing it there,
    45which fixed-parameter tractability of P∣HM∣Cmax⁡P \mid HM \mid C_{\max} includes.
    46-/
    47
    48namespace Lax434175.HighMultiplicity
    49open Lax434175 Lax434175.Problems Lax434175.Assembly Lax434175.Results Lax434175.ResultParameters
    50open Lax434175.Propagation
    51
    52/-- The standard reading determines the answer for every specification with high
    53multiplicity. -/
    54axiom determined {t : Spec OperationsFamily.family}
    55 (ht : t.module .encoding = .highMultiplicity) : Determined StandardReading.ops t
    56
    57/-- The arrow `s ≤ t` from a specification with the standard encoding and without
    58facts on pairs of jobs to one with high multiplicity. -/
    59structure Step (s t : Spec OperationsFamily.family) : Prop where
    60 le : s.le t
    61 standard : s.module .encoding = .standard
    62 highMultiplicity : t.module .encoding = .highMultiplicity
    63 noPrecedence : (s.module .precedence).order = .none
    64 noDelays : s.module .communicationDelays = .none
    65
    66variable {s t : Spec OperationsFamily.family}
    67
    68/-- On every instance `y` with threshold `D'` written by a high-multiplicity word of the
    69lift of an instance `x` of `s` with threshold `D`, `κt y D'` is at most `g (κs x D)`. -/
    70def ParamBound (hF : OperationsFamily.family.Sound) (h : s.le t) (κs : TParameter (problem _ s))
    71 (κt : TParameter (problem _ t)) (g : ℕ → ℕ) : Prop :=
    72 ∀ u x D y D', EncodesDecision (StandardReading.ops.at t) u ((Assembly.lift _ hF h).map x) D →
    73 EncodesDecision (StandardReading.ops.at t) u y D' → κt y D' ≤ g (κs x D)
    74
    75open Lax496464.WH_A2_FptReductions Lax496464.WH_B4_Hierarchies
    76
    77/-- NP-hardness goes up from the standard encoding to high multiplicity. -/
    78axiom npHard_up (hst : Step s t) :
    79 NPHard (StandardReading.ops.at s) → NPHard (StandardReading.ops.at t)
    80
    81/-- W[t]-hardness goes up from the standard encoding to high multiplicity. -/
    82axiom wHard_up (hst : Step s t) (hF : OperationsFamily.family.Sound) (w : ℕ)
    83 {κs : TParameter (problem _ s)} {κt : TParameter (problem _ t)} (g : ℕ → ℕ) (hg : Computable g)
    84 (hκ : ParamBound hF hst.le κs κt g) :
    85 WHard (StandardReading.ops.at s) w κs → WHard (StandardReading.ops.at t) w κt
    86
    87/-- Being in P goes down from high multiplicity to the standard encoding. -/
    88axiom inP_down (hst : Step s t) :
    89 InP (StandardReading.ops.at t) → InP (StandardReading.ops.at s)
    90
    91/-- Fixed-parameter tractability goes down from high multiplicity to the standard
    92encoding. -/
    93axiom isFPT_down (hst : Step s t) (hF : OperationsFamily.family.Sound)
    94 {κs : TParameter (problem _ s)} {κt : TParameter (problem _ t)}
    95 (g : ℕ → ℕ) (hg : Computable g) (hκ : ParamBound hF hst.le κs κt g)
    96 (hps : IsParameterized (parameterized (StandardReading.ops.at s) κs)) :
    97 IsFPT (StandardReading.ops.at t) κt → IsFPT (StandardReading.ops.at s) κs
    98
    99/-- NP-hardness goes up along `P||Cmax → P|HM|Cmax`. -/
    100axiom npHard_makespan :
    101 NPHard (StandardReading.ops.at ZooParallel.p0) → NPHard (StandardReading.ops.at ZooParallel.p254)
    102
    103/-- W[t]-hardness for the number of machines goes up along `P||Cmax → P|HM|Cmax`. -/
    104axiom wHard_m_makespan (w : ℕ) :
    105 WHard (StandardReading.ops.at ZooParallel.p0) w (Results.lift (Ops.m ZooParallel.p0)) →
    106 WHard (StandardReading.ops.at ZooParallel.p254) w (Results.lift (Ops.m ZooParallel.p254))
    107
    108/-- Fixed-parameter tractability for the number of distinct processing times goes down
    109along `P||Cmax → P|HM|Cmax`. -/
    110axiom isFPT_numP_makespan :
    111 IsFPT (StandardReading.ops.at ZooParallel.p254) (Results.lift (Ops.numP ZooParallel.p254)) →
    112 IsFPT (StandardReading.ops.at ZooParallel.p0) (Results.lift (Ops.numP ZooParallel.p0))
    113
    114end Lax434175.HighMultiplicity
    115
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    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…