Scheduling problems as parameterized problems on words
Lax434175.WordProblems · concepts/Lax434175/WordProblems.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural 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 and a parameter of its problem, the decision version of the problem of becomes a parameterized problem on words. An instance with the integral threshold is encoded by a word of followed by two entries, or according to whether is negative, and . The admissible words are these, the yes-instances are those for which some feasible schedule has cost at most , and the parameter of the word is .
Theorem. Let the fields of the family be sound, let be field by field a special case of , and let and be parameters with for a computable and every instance of read as an instance of . Then the parameterized problem of and fpt-reduces to that of and ; 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 to that of , and hardness for a class from the problem of to that of .
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax888481.ParameterizedComplexity |
| 2 | import Lax496464.WH_A2_FptReductions |
| 3 | import Lax434175.Parameters |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Scheduling problems as parameterized problems on words |
| 8 | type: theorem |
| 9 | --- |
| 10 | A parameterized problem on words consists of the words that encode an |
| 11 | instance, the yes-instances among them, and a parameter read off the word. |
| 12 | Fixed-parameter tractability, fpt-reductions and hardness for a class of such |
| 13 | problems are those of the word RAM. |
| 14 | |
| 15 | A coding of a family of scheduling problems says, for every specification, |
| 16 | which words encode which instance, such that a word encodes at most one |
| 17 | instance of a specification and a word that encodes an instance also encodes |
| 18 | it when the instance is read with a field-wise more general specification. |
| 19 | |
| 20 | Given a coding, a specification and a parameter of its problem, |
| 21 | the decision version of the problem of becomes a parameterized problem on |
| 22 | words. An instance with the integral threshold is encoded by a word |
| 23 | of followed by two entries, or according to whether is |
| 24 | negative, and . The admissible words are these, the yes-instances are |
| 25 | those for which some feasible schedule has cost at most , and the |
| 26 | parameter of the word is . |
| 27 | |
| 28 | **Theorem.** Let the fields of the family be sound, let be field by field |
| 29 | a special case of , and let and be parameters with |
| 30 | for a computable and every instance |
| 31 | of read as an instance of . Then the parameterized problem of |
| 32 | and fpt-reduces to that of and ; the reduction is |
| 33 | the identity on words. In particular this holds, with the same parameter on |
| 34 | both sides, for every parameter of the kernel instance and for every |
| 35 | invariant parameter of a constraint field. Consequently fixed-parameter |
| 36 | tractability passes from the problem of to that of , and hardness for |
| 37 | a class from the problem of to that of . |
| 38 | -/ |
| 39 | |
| 40 | namespace Lax434175.WordProblems |
| 41 | open Lax434175.Problems Lax434175.Kernels Lax434175.Modules Lax434175.Assembly |
| 42 | open Lax434175.Parameters |
| 43 | open Lax496464.WH_A2_FptReductions |
| 44 | open scoped Lax496464.WH_A2_FptReductions |
| 45 | |
| 46 | /-- A coding of the instances of the problems of a family by words. -/ |
| 47 | structure 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 | |
| 57 | variable {K : Kernel} {F : Family K} |
| 58 | |
| 59 | /-- The word presents the instance together with the threshold: a word of the |
| 60 | instance followed by the sign and the absolute value of the threshold. -/ |
| 61 | def 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 | |
| 64 | open Classical in |
| 65 | /-- The decision version of the problem of a specification, with a parameter, |
| 66 | as a parameterized problem on words. -/ |
| 67 | noncomputable 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 | |
| 73 | axiom 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 | |
| 78 | axiom 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 | |
| 82 | axiom 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 | |
| 86 | axiom 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 | |
| 91 | axiom 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 | |
| 95 | end Lax434175.WordProblems |
| 96 |
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments