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

Scheduling problems as parameterized problems on words

Lax434175.WordProblems · concepts/Lax434175/WordProblems.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 parameterized problem on words consists of the words that encode an instance, the yes-instances among them, and a parameter read off the word. Fixed-parameter tractability, fpt-reductions and hardness for a class of such problems are those of the word RAM.

    A coding of a family of scheduling problems says, for every specification, which words encode which instance, such that a word encodes at most one instance of a specification and a word that encodes an instance also encodes it when the instance is read with a field-wise more general specification.

    Given a coding, a specification ss and a parameter κ\kappa of its problem, the decision version of the problem of ss becomes a parameterized problem on words. An instance xx with the integral threshold DD is encoded by a word of xx followed by two entries, 11 or 00 according to whether DD is negative, and ∣D∣|D|. The admissible words are these, the yes-instances are those for which some feasible schedule has cost at most DD, and the parameter of the word is κ(x)\kappa(x).

    Theorem. Let the fields of the family be sound, let ss be field by field a special case of tt, and let κs\kappa_s and κt\kappa_t be parameters with κt(x′)≤g(κs(x))\kappa_t(x') \le g(\kappa_s(x)) for a computable gg and every instance xx of ss read as an instance x′x' of tt. Then the parameterized problem of ss and κs\kappa_s fpt-reduces to that of tt and κt\kappa_t; the reduction is the identity on words. In particular this holds, with the same parameter on both sides, for every parameter of the kernel instance and for every invariant parameter of a constraint field. Consequently fixed-parameter tractability passes from the problem of tt to that of ss, and hardness for a class from the problem of ss to that of tt.

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

    Lean source view on GitHub

    1import Lax888481.ParameterizedComplexity
    2import Lax496464.WH_A2_FptReductions
    3import Lax434175.Parameters
    4
    5/-!
    6---
    7title: Scheduling problems as parameterized problems on words
    8type: theorem
    9---
    10A parameterized problem on words consists of the words that encode an
    11instance, the yes-instances among them, and a parameter read off the word.
    12Fixed-parameter tractability, fpt-reductions and hardness for a class of such
    13problems are those of the word RAM.
    14
    15A coding of a family of scheduling problems says, for every specification,
    16which words encode which instance, such that a word encodes at most one
    17instance of a specification and a word that encodes an instance also encodes
    18it when the instance is read with a field-wise more general specification.
    19
    20Given a coding, a specification ss and a parameter κ\kappa of its problem,
    21the decision version of the problem of ss becomes a parameterized problem on
    22words. An instance xx with the integral threshold DD is encoded by a word
    23of xx followed by two entries, 11 or 00 according to whether DD is
    24negative, and ∣D∣|D|. The admissible words are these, the yes-instances are
    25those for which some feasible schedule has cost at most DD, and the
    26parameter of the word is κ(x)\kappa(x).
    27
    28**Theorem.** Let the fields of the family be sound, let ss be field by field
    29a special case of tt, and let κs\kappa_s and κt\kappa_t be parameters with
    30κt(x′)≤g(κs(x))\kappa_t(x') \le g(\kappa_s(x)) for a computable gg and every instance xx
    31of ss read as an instance x′x' of tt. Then the parameterized problem of ss
    32and κs\kappa_s fpt-reduces to that of tt and κt\kappa_t; the reduction is
    33the identity on words. In particular this holds, with the same parameter on
    34both sides, for every parameter of the kernel instance and for every
    35invariant parameter of a constraint field. Consequently fixed-parameter
    36tractability passes from the problem of tt to that of ss, and hardness for
    37a class from the problem of ss to that of tt.
    38-/
    39
    40namespace Lax434175.WordProblems
    41open Lax434175.Problems Lax434175.Kernels Lax434175.Modules Lax434175.Assembly
    42open Lax434175.Parameters
    43open Lax496464.WH_A2_FptReductions
    44open scoped Lax496464.WH_A2_FptReductions
    45
    46/-- A coding of the instances of the problems of a family by words. -/
    47structure Coding {K : Kernel} (F : Family K) where
    48 /-- The word encodes the instance. -/
    49 Encodes : (s : Spec F) → List ℕ → Inst F s → Prop
    50 /-- A word encodes at most one instance. -/
    51 unique : ∀ (s : Spec F) (w : List ℕ) (x y : Inst F s), Encodes s w x → Encodes s w y → x = y
    52 /-- A word of an instance is a word of the instance read with a more
    53 general specification. -/
    54 lift : ∀ (hF : F.Sound) {s t : Spec F} (h : s.le t) (w : List ℕ) (x : Inst F s),
    55 Encodes s w x → Encodes t w ((lift F hF h).map x)
    56
    57variable {K : Kernel} {F : Family K}
    58
    59/-- The word presents the instance together with the threshold: a word of the
    60instance followed by the sign and the absolute value of the threshold. -/
    61def EncodesDecision (C : Coding F) (s : Spec F) (w : List ℕ) (x : Inst F s) (D : ℤ) : Prop :=
    62 ∃ y, w = y ++ [if D < 0 then 1 else 0, D.natAbs] ∧ C.Encodes s y x
    63
    64open Classical in
    65/-- The decision version of the problem of a specification, with a parameter,
    66as a parameterized problem on words. -/
    67noncomputable def wordProblem (C : Coding F) (s : Spec F) (κ : Parameter (problem F s)) :
    68 Lax888481.ParameterizedComplexity.Problem where
    69 Domain := {w | ∃ (x : Inst F s) (D : ℤ), EncodesDecision C s w x D}
    70 Yes w := ∃ (x : Inst F s) (D : ℤ), EncodesDecision C s w x D ∧ (problem F s).Decides x D
    71 param w := if h : ∃ (x : Inst F s) (D : ℤ), EncodesDecision C s w x D then κ h.choose else 0
    72
    73axiom fptReduces_of_le (C : Coding F) (hF : F.Sound) {s t : Spec F} (h : s.le t)
    74 (κs : Parameter (problem F s)) (κt : Parameter (problem F t)) (g : ℕ → ℕ)
    75 (hg : Computable g) (hκ : ∀ x, κt ((lift F hF h).map x) ≤ g (κs x)) :
    76 wordProblem C s κs ≤ᶠᵖᵗ wordProblem C t κt
    77
    78axiom fptReduces_of_le_kernel (C : Coding F) (hF : F.Sound) {s t : Spec F} (h : s.le t)
    79 (κ : K.Inst → ℕ) :
    80 wordProblem C s (ofKernel F κ s) ≤ᶠᵖᵗ wordProblem C t (ofKernel F κ t)
    81
    82axiom fptReduces_of_le_field (C : Coding F) (hF : F.Sound) {s t : Spec F} (h : s.le t)
    83 (i : F.ModuleName) (κ : FieldParameter (F.module i)) (hκ : κ.Invariant) :
    84 wordProblem C s (ofField F i κ s) ≤ᶠᵖᵗ wordProblem C t (ofField F i κ t)
    85
    86axiom fpt_of_le_kernel (C : Coding F) (hF : F.Sound) {s t : Spec F} (h : s.le t)
    87 (κ : K.Inst → ℕ) :
    88 IsParameterized (wordProblem C s (ofKernel F κ s)) →
    89 wordProblem C t (ofKernel F κ t) ∈ FPT → wordProblem C s (ofKernel F κ s) ∈ FPT
    90
    91axiom hard_of_le_kernel (C : Coding F) (hF : F.Sound) {s t : Spec F} (h : s.le t)
    92 (κ : K.Inst → ℕ) (𝒞 : Set Lax888481.ParameterizedComplexity.Problem) :
    93 Hard 𝒞 (wordProblem C s (ofKernel F κ s)) → Hard 𝒞 (wordProblem C t (ofKernel F κ t))
    94
    95end Lax434175.WordProblems
    96
    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…