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
MetaMathlibExt.Complexity.KeyTheorems.PCPTheorem.pcp_theorem
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)}
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
abbrev DecisionProblem := List Bool → Bool
MathlibExt/Computability/Complexity.lean:170
def PCP (rbound qbound : ℕ → ℕ) : DecisionComplexityClass :=
{L | ∃ queries : List Bool × List Bool → List ℕ,
∃ decide : List Bool × List Bool × List Bool → Bool,
IsPolyTime queries ∧ IsPolyTime decide ∧
(∀ x rand, (queries (x, rand)).length ≤ qbound x.length) ∧
∀ x,
(L x = true →
∃ proof : ℕ → Bool,
3 * Set.ncard {rand : Fin (rbound x.length) → Bool |
decide (x, List.ofFn rand,
(queries (x, List.ofFn rand)).map proof) = true} ≥
2 * 2 ^ (rbound x.length)) ∧
⋯
CSLibExt/Computability/Complexity/Classes.lean:391
Sources
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
Statement usesProbabilistically checkable proofs · Complexity classes · Decision problems · The complexity class NP
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.