NP-Hardness of a Problem on Words of Numbers
Lax496464.WH_F3_NPHard · concepts/Lax496464/WH_F3_NPHard.lean · lax-496464
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A problem is NP-hard if every language in NP reduces to its yes-instances by a map computable in polynomial time: a map from binary words to words of numbers such that if and only if is a yes-instance, for every .
Concept map
Lean source view on GitHub
| 1 | import Lax888481.ParameterizedComplexity |
| 2 | import Lax434930.NondeterministicPolynomialTime |
| 3 | import Lax759944.TuringPolytime |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: NP-Hardness of a Problem on Words of Numbers |
| 8 | type: definition |
| 9 | --- |
| 10 | A problem is **NP-hard** if every language in NP reduces to its yes-instances by a map computable |
| 11 | in polynomial time: a map from binary words to words of numbers such that if and only |
| 12 | if is a yes-instance, for every . |
| 13 | |
| 14 | # Formalization Notes |
| 15 | |
| 16 | **Machines.** The map is computed by a Turing machine in polynomial time |
| 17 | (`Turing.TM2ComputableInPolyTime`). The machine reads the binary word and writes the canonical |
| 18 | binary encoding of the resulting word of numbers (`Lax759944.BinaryWordEncoding.encode`), each |
| 19 | number a separator followed by its bits. By the equivalence proved in `Lax759944`, this is |
| 20 | polynomial time on the word RAM in the bit size of the word. |
| 21 | |
| 22 | **Words outside the domain.** The condition is is a yes-instance. A word |
| 23 | that maps to a word presenting no instance is therefore a non-member of . `NPHardIn` asks |
| 24 | in addition that no word is mapped outside the domain. |
| 25 | -/ |
| 26 | |
| 27 | namespace Lax496464.WH_F3_NPHard |
| 28 | |
| 29 | open Lax434930.PolynomialTime Lax434930.NondeterministicPolynomialTime |
| 30 | open Lax888481.ParameterizedComplexity |
| 31 | |
| 32 | /-- `P` is **NP-hard**: every language in NP reduces to it in polynomial time by a Turing |
| 33 | machine writing the canonical encoding of the resulting word. -/ |
| 34 | def NPHard (P : Problem) : Prop := |
| 35 | ∀ A : Language, A ∈ NP → |
| 36 | ∃ f : Word → List ℕ, |
| 37 | Nonempty (Turing.TM2ComputableInPolyTime id Lax759944.BinaryWordEncoding.encode f) ∧ |
| 38 | ∀ x, x ∈ A ↔ P.Yes (f x) |
| 39 | |
| 40 | /-- `P` is **NP-hard on its domain**: as `NPHard`, and in addition the reduction always outputs a |
| 41 | word of the domain, that is a word presenting an instance of `P`. This is the form a reduction that |
| 42 | is correct only on instances can be composed with. -/ |
| 43 | def NPHardIn (P : Problem) : Prop := |
| 44 | ∀ A : Language, A ∈ NP → |
| 45 | ∃ f : Word → List ℕ, |
| 46 | Nonempty (Turing.TM2ComputableInPolyTime id Lax759944.BinaryWordEncoding.encode f) ∧ |
| 47 | ∀ x, f x ∈ P.Domain ∧ (x ∈ A ↔ P.Yes (f x)) |
| 48 | |
| 49 | end Lax496464.WH_F3_NPHard |
| 50 |
Formalization Notes
Machines. The map is computed by a Turing machine in polynomial time (). The machine reads the binary word and writes the canonical binary encoding of the resulting word of numbers (), each number a separator followed by its bits. By the equivalence proved in , this is polynomial time on the word RAM in the bit size of the word.
Words outside the domain. The condition is is a yes-instance. A word that maps to a word presenting no instance is therefore a non-member of . asks in addition that no word is mapped outside the domain.
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.
0 comments