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.

  • $\begingroup$ Are $X,Y$ part of the input? If so, this is almost $\Sigma_2 SAT$ $\endgroup$ – Ariel Jun 18 '20 at 7:19
  • $\begingroup$ 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}$) $\endgroup$ – user109711 Jun 18 '20 at 7:39
  • $\begingroup$ $\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. $\endgroup$ – Ariel Jun 18 '20 at 8:05
  • 1
    $\begingroup$ @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. $\endgroup$ – D.W. Jun 20 '20 at 19:39
  • $\begingroup$ @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). $\endgroup$ – Ariel Jun 20 '20 at 21:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.