About: (SAT, ε-UNSAT)

In computational complexity theory, (SAT, ε-UNSAT) is a language that is used in the proof of the PCP theorem, which relates the language NP to probabilistically checkable proof systems. For a given 3-CNF formula, Φ, and a constant, ε < 1, Φ is in (SAT, ε-UNSAT) if it is satisfiable and not in (SAT, ε-UNSAT) if the maximum number of satisfiable clauses (MAX-3SAT) is less than or equal to (1-ε) times the number of clauses in Φ. If neither of these conditions are true, the membership of Φ in (SAT, ε-UNSAT) is undefined.