Is 2QBF in P^NP?

Question

2QBF is the following problem: given a CNF formula $\psi$ on $2n$ variables, determine the truth value of

$$\forall x \in \{0,1\}^n . \exists y \in \{0,1\}^n . \psi(x,y).$$

Question: Is 2QBF in $P^{NP}$ (or, expected to be in $P^{NP}$, under standard conjectures)?

Motivation: If the answer were yes, it would suggest a way to solve 2QBF, using multiple invocations of a SAT solver. Given that SAT solvers are surprisingly effective on some problems, that might be of interest in situations where we need to solve 2QBF.

(2QBF is a version of QBF restricted to two alternating quantifiers. QBF is known to be PSPACE-complete, but 2QBF seems easier than QBF.)

Answer 1

Determining the truth of $\exists \forall. \phi$ formulas is $\Sigma_2^P$-complete whereas determining the truth of $\forall \exists. \phi$ formulas are $\Pi_2^P$-complete. Therefore, unless $\Sigma_2^P=P^{NP}$ (resp., $\Pi_2^P=P^{NP}$) neither of these problems can be solved in $P^{NP}$.

Answer 2

2QBF (in the form presented in the question) is $\Pi_2^P$-complete. Also, $P^{NP} = \Delta_2^P = P^{coNP}$ and $\Pi_2^P = coNP^{coNP}$.

Therefore, if 2QBF is in $P^{NP}$, then $\Pi_2^P = \Delta_2^P$, from which it follows that $\Pi_2^P = \Pi_3^P$ (since $P^{coNP} = coNP^{coNP}$ implies $\Pi_3^P = coNP^{coNP^{coNP}} = coNP^{P^{coNP}} = coNP^{coNP} = \Pi_2^P$), which means that the polynomial hierarchy collapses -- something that is conjectured not to happen.

Therefore, under standard conjectures (that the polynomial hierarchy doesn't collapse), 2QBF is not in $P^{NP}$. In other words, there is no general way to solve 2QBF using polynomially invocations of a SAT solver.