The following problem has made me ask this question:

Given a boolean formula $\varphi(X)$ decide if there exists a quantification of $\varphi(X)$ with $k$ $\forall$ quantifiers that holds true. Assume that $k$ is bounded with $\mathcal O(\log n)$.

To clarify, the order of the quantifiers is arbitrary. I.e. the resulting formula is of the form $Q_{a_1}x_{b_1}\ Q_{a_2}x_{b_2}\cdots Q_{a_n}x_{b_n}:\varphi(x_1,x_2,\cdots,x_n)$ where each $Q$ is either $\exists$ or $\forall$, and there is no connection between $a_i$ and $b_j$ for any $i,j$.

This problem is clearly in $\mathsf{NP}$: first the proof would show the QBF with $k$ $\forall$-quantified variables, then it would expand it into an unquantified formula with at most polynomial ($2^k$) blowup and show that this new formula is satisfiable.

However, in the worst case there are $\omega(poly(n)\cdot n^{\log n})$ candidate quantifications of $\varphi(X)$ and therefore it seems non-trivial to find a poly-time reduction.

But maybe there is an easier method? Is it possible to find a poly-time reduction to SAT based solely on the proof verification algorithm?

  • $\begingroup$ @D.W. The reduction from SAT is easy: just set $k$ at $0$. What I mean is that every certificate from this problem must somehow translate to a certificate for some instance of SAT problem, and there must be a deterministic poly-time construction for it. So I'm trying to think how such a translation is possible. But I guess what Steven has suggested technically would work. $\endgroup$
    – rus9384
    Jan 16 at 22:54
  • $\begingroup$ @D.W. Sure! I have turned my comment into an answer. $\endgroup$
    – Steven
    Jan 16 at 23:25

1 Answer 1


Finding a reduction to SAT is easy but tedious. Write down a description of polynomial-time Turing machine $T$ that checks the certificate (as you have argued in your question, such a Turing machine exists), then encode $T$ into a SAT formula $\psi$ that has a variable for each input symbol of the certificate (plus additional variables as needed) such that $\psi$ admits a satisfying assignment iff there is a way to chose the symbols of the certificate and a corresponding valid computation path that causes $T$ to accept.

This can be done following the construction used by the proof of the Cook–Levin theorem.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.