How is $\overline{SAT}$ not obviously in NP?

Question

First of all, I do know that it is not known whether or not $\overline{SAT}$ is in NP. But to me, it clearly looks like it is in NP. Given a Boolean formula φ with n variables, we nondeterministically go through all 2ドル^n$ possible assignments. If any one of them is satisfying, reject, else accept.

So what is the problem with this logic? What am I missing?

Answer 1

The problem is that you have to convince that NO assignment can satisfy the formula, and that cannot be done easily non-deterministically.

For the problem $\mathsf{SAT}$, a certificate can be a satisfying assignment. Once the non-deterministic algorithm returns an assignment, you can verify deterministically that the assignment is indeed satisfying.

However, for the problem $\mathsf{UNSAT}$, you have to return a certificate for a NON-SATISFIABLE formula, not for a satisfiable one.

What you describe:

we nondeterministically go through all 2ドル^n$ possible assignments

is not possible: you can non-deterministically go through one of the possible assignments (for example a satisfying one), but not through all of them at once. When writing a non-deterministic algorithm, the added operation is

choose non-deterministically a bit 0ドル$ or 1ドル$

not

explore non-deterministically both bits 0ドル$ and 1ドル$.

Answer 2

The algorithm you describe runs in $P^{NP}$, not in $NP$. (And yes, $\overline{SAT}\in P^{NP}$)

A nondeterministic Turing-machine $M$ accepts an input $x$ iff there is a sequence of nondeterministic choices such that the according computation starting with $x$ reaches an accepting state. However, it only rejects if every sequence of nondeterministic choices leads to a computation that does not reach an accepting state.

It is heavily biased towards acceptance.