Lax Lean Archive

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

NP-hardness of a scheduling problem, and on a class of instances

Lax470956.NPHardness · concepts/Lax470956/NPHardness.lean · lax-470956

definition

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

    Definition

    A scheduling problem is NP-hard if every language in NP has a polynomial-time many-one reduction to it, the reduction's output being an instance in the binary encoding.

    It is NP-hard on a class C\mathcal C of instances if such a reduction exists whose output always lies in C\mathcal C. When C\mathcal C is a slice on which some parameter is bounded by an absolute constant, this is para-NP-hardness for that parameter: it rules out an algorithm running in f(k)⋅poly(n)f(k)\cdot\mathrm{poly}(n) time for every function ff, unless P=NP\mathrm{P} = \mathrm{NP} — a stronger and unconditional-in-ff conclusion than W[1]-hardness, which rules out fixed-parameter tractability only under W[1]≠FPT\mathrm{W}[1] \ne \mathrm{FPT}.

    Concept map
    6 concepts; 2 descendants hidden
    100%
    Proven claimOpen claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax470956.BinaryEncoding
    2import Lax434930.NondeterministicPolynomialTime
    3
    4/-!
    5---
    6title: NP-hardness of a scheduling problem, and on a class of instances
    7type: definition
    8---
    9A scheduling problem is *NP-hard* if every language in NP has a polynomial-time many-one
    10reduction to it, the reduction's output being an instance in the binary encoding.
    11
    12It is *NP-hard on a class* C\mathcal C of instances if such a reduction exists whose
    13output always lies in C\mathcal C. When C\mathcal C is a slice on which some parameter
    14is bounded by an absolute constant, this is *para-NP-hardness* for that parameter: it
    15rules out an algorithm running in f(k)⋅poly(n)f(k)\cdot\mathrm{poly}(n) time for *every* function
    16ff, unless P=NP\mathrm{P} = \mathrm{NP} — a stronger and unconditional-in-ff conclusion
    17than W[1]-hardness, which rules out fixed-parameter tractability only under
    18W[1]≠FPT\mathrm{W}[1] \ne \mathrm{FPT}.
    19
    20# Formalization notes
    21
    22Hardness is defined by quantifying over NP, not against a fixed complete problem. NP is
    23available — `Lax434930` defines it — so the definition a textbook gives can be written
    24down, and there is no reason to substitute a reference problem for it as the
    25parameterized definition of this submission has to.
    26
    27The reduction's target is an instance rather than a word, with the encoding applied by
    28the definition. This keeps a statement about a problem from also being a statement about
    29which words are well-formed, and it matches how graph problems are stated elsewhere in
    30the archive.
    31
    32"NP-hard on a class" is one definition covering both a plain hardness claim, where the
    33class is everything, and a para-NP-hardness claim, where it is a bounded slice. Stating
    34the slice as a predicate on instances rather than as a bound on a parameter function
    35keeps it readable — "every emitted instance has pmax⁡≤25p_{\max} \le 25 and unit weights" is
    36what the reduction actually guarantees, and what a reader checks it against.
    37-/
    38
    39namespace Lax470956.NPHardness
    40
    41open Lax470956.Scheduling Lax470956.BinaryEncoding
    42open Lax434930.PolynomialTime Lax434930.NondeterministicPolynomialTime
    43
    44/-- A property of scheduling instances: a decision problem on them. -/
    45abbrev Problem := Instance → Prop
    46
    47/-- `Q` is **NP-hard**: every language in NP reduces to it in polynomial time. -/
    48def NPHard (Q : Problem) : Prop :=
    49 ∀ A : Language, A ∈ NP →
    50 ∃ f : Word → Instance,
    51 Nonempty (Turing.TM2ComputableInPolyTime id encodeInstance f) ∧
    52 ∀ x, x ∈ A ↔ Q (f x)
    53
    54/-- `Q` is **NP-hard on `C`**: every language in NP reduces to it in polynomial time by a
    55reduction all of whose outputs lie in `C`. -/
    56def NPHardOn (Q : Problem) (C : Instance → Prop) : Prop :=
    57 ∀ A : Language, A ∈ NP →
    58 ∃ f : Word → Instance,
    59 Nonempty (Turing.TM2ComputableInPolyTime id encodeInstance f) ∧
    60 ∀ x, C (f x) ∧ (x ∈ A ↔ Q (f x))
    61
    62end Lax470956.NPHardness
    63
    Formalization notes

    Hardness is defined by quantifying over NP, not against a fixed complete problem. NP is available — Lax434930Lax434930 defines it — so the definition a textbook gives can be written down, and there is no reason to substitute a reference problem for it as the parameterized definition of this submission has to.

    The reduction's target is an instance rather than a word, with the encoding applied by the definition. This keeps a statement about a problem from also being a statement about which words are well-formed, and it matches how graph problems are stated elsewhere in the archive.

    "NP-hard on a class" is one definition covering both a plain hardness claim, where the class is everything, and a para-NP-hardness claim, where it is a bounded slice. Stating the slice as a predicate on instances rather than as a bound on a parameter function keeps it readable — "every emitted instance has pmax⁡≤25p_{\max} \le 25 and unit weights" is what the reduction actually guarantees, and what a reader checks it against.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…