An optimization version of 2QBF: is it $\mathsf{NP}^{\mathsf{NP}}$-hard?

I am studying the computational complexity of the following decision problem related to 2QBF:

• Input: a 3-CNF formula $$\varphi$$ over $$X \cup Y$$, where $$X$$, $$Y$$ are disjoint sets of propositional variables, and an integer $$k \geq 0$$.
• Question: does there exists an assignment of the variables from $$X$$ such that all assignments of the variables from $$Y$$ satisfy at least $$k$$ clauses from $$\varphi$$?

Is this problem $$\mathsf{NP}^{\mathsf{NP}}$$-hard?

Despite the problem being in $$\mathsf{NP}$$ for the case where all clauses in $$\varphi$$ are required to be satisfied, to me the problem above seems to be $$\mathsf{NP}^{\mathsf{NP}}$$-hard. But while a number of works can be found when the two quantifiers are reversed (i.e., when the first quantifier is universal and the second quantifier is existential), I cannot manage to find the problem stated above studied in the literature.

• Are $X,Y$ part of the input? If so, this is almost $\Sigma_2 SAT$ – Ariel Jun 18 '20 at 7:19
• Isn't $\Sigma_2SAT$ the problem of deciding whether the QBF $\forall X \exists Y \varphi$ is valid? My point is precisely that in the problem I consider, the QBF is of the form $\exists X \forall Y \varphi$, and that at least $k$ clauses in $\varphi$ must be satisfied (not necessarily all clauses must be satisfied, otherwise the problem falls in $\mathsf{NP}$) – user109711 Jun 18 '20 at 7:39
• $\Sigma_2 SAT$ consists of true formulas of the form $\exists u_1 \forall u_2 \varphi(u_1,u_2)$ where $\varphi$ is a CNF and $u_1,u_2$ are vectors of boolean variables. – Ariel Jun 18 '20 at 8:05
• @Ariel, are you sure? user109711 has explained patiently to me that $\exists u_1 \forall u_2 \varphi(u_1,u_2)$ is in NP. Given a value of $u_1$ (the witness), one can check in polynomial time whether $\forall u_2 \varphi(u_1,u_2)$ holds, by checking one clause at a time. – D.W. Jun 20 '20 at 19:39
• @D.W. Got me there. I just checked Arora & Barak's book and they indeed mention that the formula is not necessarily a CNF (the same is obviously true of the language Tautology which is famously coNP complete). – Ariel Jun 20 '20 at 21:56