Unbounded-error probabilistic time (PP)

DefinitionThe MAJSAT language#✓fully proved

MAJSAT is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of pairs, to a pair \((u, \varphi)\) of a bitstring \(u\) and a CNF formula \(\varphi\) such that, with \(n = |u|\), every literal of \(\varphi\) has variable index less than \(n\), and more than half of the \(2^n\) assignments \(a : \{0, \dots, n-1\} \to \{\mathrm{true}, \mathrm{false}\}\) satisfy \(\varphi\), that is, twice their number exceeds \(2^n\). Only the length of \(u\) matters, and a bitstring that does not decode is rejected.

noncomputable def majSatDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := List Bool × Cslib.Logic.PL.CNF) x with
  | some i => decide (
      (∀ clause ∈ i.2, ∀ l ∈ clause, l.1 < i.1.length) ∧
      2 * Set.ncard {a : Fin i.1.length → Bool |
        Cslib.Logic.PL.CNF.Satisfies
          (fun v => if h : v < i.1.length then a ⟨v, h⟩ else false) i.2} > 2 ^ i.1.length)
  | none => false

Uses 12 · Used by 1

Statement usesCNF formula · Satisfaction of a CNF formula · CNF clause · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Decision problems

Used byMAJSAT is PP-complete

TheoremMAJSAT is PP-complete#●ready to prove

The MAJSAT language is in PP, and every decision problem in PP has a polynomial-time many-one reduction to MAJSAT.

public theorem_wanted majsat_pp_complete :
    majSatDec ∈ PP ∧ ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
      L ∈ PP → Cslib.CookLevin.PolyManyOneRed L majSatDec

Sources

• J. Gill, "Computational complexity of probabilistic Turing machines", SIAM Journal on Computing 6 (1977), 675-695.

Uses 5

Statement usesProbabilistic polynomial time with unbounded error · Polynomial-time many-one reduction · The MAJSAT language · Complexity classes · Decision problems

TheoremNP is contained in PP#●ready to prove

Every decision problem in NP also belongs to PP, the class of decision problems decided in probabilistic polynomial time with unbounded error.

public theorem_wanted np_subset_pp :
    MetaMathlibExt.ComplexityTheory.NP ⊆ PP

Sources

• J. Gill, "Computational complexity of probabilistic Turing machines" (1977).

Uses 4

Statement usesProbabilistic polynomial time with unbounded error · Complexity classes · Decision problems · The complexity class NP

TheoremPP is contained in PSPACE#●ready to prove

Every decision problem in PP, the class of decision problems decided with unbounded error in probabilistic polynomial time, belongs to PSPACE.

public theorem_wanted pp_subset_pspace :
    PP ⊆ PSPACE

Sources

• J. Gill, "Computational complexity of probabilistic Turing machines" (1977); S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009 (PP ⊆ PSPACE).

Uses 4

Statement usesProbabilistic polynomial time with unbounded error · Polynomial space for decision problems · Complexity classes · Decision problems

1 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.