Is 2QBF in P^NP?

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.)

• 2QBF is complete for the 2nd level of the polynomial hierarchy ($NP^{NP}$). So, if it is shown to be in ($P^{NP}$), wouldn't the polynomial hierarchy collapse (which is considered unlikely)? – skankhunt42 Feb 22 '17 at 19:18

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}$.
• user109711 has explained to me that $\exists \forall \phi$ formulas are in NP if $\phi$ is in CNF: you can check the validity of $\forall \phi$ by checking separately for each clause if it holds universally. – D.W. Jun 20 '20 at 19:38
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.