Lax Lean Archive

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

Strong and plain hardness

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

proven

Loading review…

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 problem is strongly NP-hard, W[t]-hard or para-NP-hard when it is hard already on the words whose numbers are at most a fixed polynomial in the length of the word, as when the numbers are written in unary. Plain hardness asks the same of all words, the numbers written in binary. The words with small numbers form a subproblem, and the identity reduces it to the whole problem.

    Theorem. Strong NP-hardness implies NP-hardness, strong W[t]-hardness implies W[t]-hardness, and strong para-NP-hardness implies para-NP-hardness, for every parameter.

    The algorithmic counterpart of strong hardness: a problem is pseudo-polynomially fixed-parameter tractable in κ\kappa when, for every polynomial bound on the numbers, it is fixed-parameter tractable in κ\kappa on the words whose numbers obey the bound. A problem that is W[t]-hard and pseudo-polynomially fixed-parameter tractable is weakly W[t]-hard: its hardness needs large numbers.

    Theorem. If a problem is strongly W[t]-hard and pseudo-polynomially fixed-parameter tractable for the same parameter, then W[t] ⊆ FPT.

    Concept map
    26 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 exclusive_weak proven

    2 npHard_of_strongly proven

    3 paraNPHard_of_strongly proven

    4 wHard_of_strongly proven

    Lean source view on GitHub

    1import Lax434175.Results
    2
    3/-!
    4---
    5title: Strong and plain hardness
    6type: theorem
    7---
    8A problem is *strongly* NP-hard, W[t]-hard or para-NP-hard when it is hard already on
    9the words whose numbers are at most a fixed polynomial in the length of the word, as
    10when the numbers are written in unary. Plain hardness asks the same of all words,
    11the numbers written in binary. The words with small numbers form a subproblem, and
    12the identity reduces it to the whole problem.
    13
    14**Theorem.** Strong NP-hardness implies NP-hardness, strong W[t]-hardness implies
    15W[t]-hardness, and strong para-NP-hardness implies para-NP-hardness, for every
    16parameter.
    17
    18The algorithmic counterpart of strong hardness: a problem is *pseudo-polynomially
    19fixed-parameter tractable* in κ\kappa when, for every polynomial bound on the
    20numbers, it is fixed-parameter tractable in κ\kappa on the words whose numbers obey
    21the bound. A problem that is W[t]-hard and pseudo-polynomially fixed-parameter
    22tractable is *weakly* W[t]-hard: its hardness needs large numbers.
    23
    24**Theorem.** If a problem is strongly W[t]-hard and pseudo-polynomially
    25fixed-parameter tractable for the same parameter, then W[t] ⊆ FPT.
    26-/
    27
    28namespace Lax434175.StrongHardness
    29open Lax434175.Problems Lax434175.Results
    30open Lax496464.WH_A2_FptReductions Lax496464.WH_B4_Hierarchies
    31
    32variable {P : Problem} (R : PReading P)
    33
    34/-- Fixed-parameter tractable in `κ` on the words with numbers at most any fixed
    35polynomial in their length. -/
    36def PseudoFPT (κ : TParameter P) : Prop :=
    37 ∀ c d, restrict (parameterized R κ) (Small c d) ∈ FPT
    38
    39/-- W[t]-hard, and pseudo-polynomially fixed-parameter tractable for the same
    40parameter. -/
    41def WeaklyWHard (t : ℕ) (κ : TParameter P) : Prop := WHard R t κ ∧ PseudoFPT R κ
    42
    43variable {R}
    44
    45axiom npHard_of_strongly : StronglyNPHard R → NPHard R
    46
    47axiom wHard_of_strongly {t : ℕ} {κ : TParameter P} : StronglyWHard R t κ → WHard R t κ
    48
    49axiom paraNPHard_of_strongly {κ : TParameter P} : StronglyParaNPHard R κ → ParaNPHard R κ
    50
    51axiom exclusive_weak {t : ℕ} {κ : TParameter P} :
    52 StronglyWHard R t κ → PseudoFPT R κ → W t ⊆ FPT
    53
    54end Lax434175.StrongHardness
    55
    Show 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…