Mahaney's theorem
DefinitionSparse decision problems#✓fully proved
A decision problem \(L\) is sparse when there is a polynomial \(p\) with natural-number coefficients such that, for every natural number \(n\), the set of bitstrings of length at most \(n\) accepted by \(L\) is finite and has at most \(p(n)\) elements.
def Sparse (L : MetaMathlibExt.ComplexityTheory.DecisionProblem) : Prop :=
∃ p : Polynomial ℕ, ∀ n,
Set.Finite {x : List Bool | x.length ≤ n ∧ L x = true} ∧
Set.ncard {x : List Bool | x.length ≤ n ∧ L x = true} ≤ p.eval nabbrev DecisionProblem := List Bool → BoolMathlibExt/Computability/Complexity.lean:170
Uses 1 · Used by 1
DefinitionNP-complete decision problems#✓fully proved
A decision problem \(L\) is NP-complete when \(L\) is in NP and every decision problem in NP has a polynomial-time many-one reduction to \(L\).
def NPComplete (L : MetaMathlibExt.ComplexityTheory.DecisionProblem) : Prop :=
L ∈ MetaMathlibExt.ComplexityTheory.NP ∧
∀ L' : MetaMathlibExt.ComplexityTheory.DecisionProblem,
L' ∈ MetaMathlibExt.ComplexityTheory.NP →
Cslib.CookLevin.PolyManyOneRed L' Labbrev DecisionProblem := List Bool → BoolMathlibExt/Computability/Complexity.lean:170
def NP : DecisionComplexityClass :=
{ L | ∃ (p : Polynomial ℕ), ∃ R : (List Bool × List Bool) → Bool,
IsPolyTime R ∧
∀ x, L x ↔ ∃ w : List Bool, w.length ≤ p.eval x.length ∧ R (x, w) }MathlibExt/Computability/Complexity.lean:200
def PolyManyOneRed (L₁ L₂ : MetaMathlibExt.ComplexityTheory.DecisionProblem) : Prop :=
∃ reduce : List Bool → List Bool,
MetaMathlibExt.ComplexityTheory.IsPolyTime reduce ∧ ∀ x, L₁ x = L₂ (reduce x)CSLibExt/Computability/CookLevin.lean:396
Uses 4 · Used by 1
TheoremMahaney's theorem: sparse NP-complete sets imply P = NP#●ready to prove
If some decision problem is both sparse and NP-complete, then the complexity classes \(\mathsf{P}\) and \(\mathsf{NP}\) are equal.
public theorem_wanted mahaney :
(∃ L : MetaMathlibExt.ComplexityTheory.DecisionProblem, Sparse L ∧ NPComplete L) →
MetaMathlibExt.ComplexityTheory.P = MetaMathlibExt.ComplexityTheory.NPabbrev DecisionProblem := List Bool → BoolMathlibExt/Computability/Complexity.lean:170
def Sparse (L : MetaMathlibExt.ComplexityTheory.DecisionProblem) : Prop :=
∃ p : Polynomial ℕ, ∀ n,
Set.Finite {x : List Bool | x.length ≤ n ∧ L x = true} ∧
Set.ncard {x : List Bool | x.length ≤ n ∧ L x = true} ≤ p.eval nWantedExt/Complexity/KeyTheorems/MahaneyWanted.lean:43
def NPComplete (L : MetaMathlibExt.ComplexityTheory.DecisionProblem) : Prop :=
L ∈ MetaMathlibExt.ComplexityTheory.NP ∧
∀ L' : MetaMathlibExt.ComplexityTheory.DecisionProblem,
L' ∈ MetaMathlibExt.ComplexityTheory.NP →
Cslib.CookLevin.PolyManyOneRed L' LWantedExt/Complexity/KeyTheorems/MahaneyWanted.lean:49
def P : DecisionComplexityClass :=
{ L | IsPolyTime L }MathlibExt/Computability/Complexity.lean:194
def NP : DecisionComplexityClass :=
{ L | ∃ (p : Polynomial ℕ), ∃ R : (List Bool × List Bool) → Bool,
IsPolyTime R ∧
∀ x, L x ↔ ∃ w : List Bool, w.length ≤ p.eval x.length ∧ R (x, w) }MathlibExt/Computability/Complexity.lean:200
Sources
- S. R. Mahaney, "Sparse complete sets for NP: solution of a conjecture of Berman and Hartmanis", Journal of Computer and System Sciences 25 (1982), 130-143.
Uses 6
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.