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.

## Complexity

It can be shown that (SAT, ε-UNSAT) characterizes PCP(O(log n), O(1)).

Let each bit in the proof *y* be

First, it is necessary to encode when the verifier accepts in 3CNF clauses
*r*, construct a sub-formula
*r*, its possible to determine all the variables queried, Enumerate each random string *r*, and add a clause
*r*. There are at most

If
*y* such that is accepted for every random string *r*. Therefore,

If
*r*. For each *r* that is rejected one of the clauses in

Therefore,

For

(SAT, ε-UNSAT) is an NP-hard language. As part of the proof of the PCP theorem, (SAT, ε-UNSAT) has also been shown to be in PCP(O(log n), O(1)).