Probabilistically checkable proofs and inapproximability

The PCP theorem and Dinur's gap amplification, optimization classes (NPO, APX, MAXSNP), and hardness of approximation results such as Håstad's MAX-3SAT bound and the absence of a PTAS for MAX-CUT.

TheoremThe PCP theorem: NP = PCP(O(log n), O(1))#●ready to prove

A decision problem belongs to NP if and only if, for some natural numbers \(c\) and \(q\), it belongs to \(\mathrm{PCP}(r, s)\), where the randomness bound is \(r(n) = c \lfloor \log_2(n + 1) \rfloor\) and the query bound is the constant function \(s(n) = q\).

public theorem_wanted pcp_theorem :
    MetaMathlibExt.ComplexityTheory.NP =
      {L : MetaMathlibExt.ComplexityTheory.DecisionProblem |
        ∃ c q, L ∈ PCP (fun n => c * Nat.log 2 (n + 1)) (fun _ => q)}
Sources
  • S. Arora, C. Lund, R. Motwani, M. Sudan, and M. Szegedy, "Proof verification and the hardness of approximation problems", Journal of the ACM 45 (1998), 501-555 (FOCS 1992); S. Arora and S. Safra, "Probabilistic checking of proofs: a new characterization of NP", Journal of the ACM 45 (1998), 70-122.
Uses 4

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.