# Is it possible to find reductions from problems in $\mathsf{NP}$ to SAT based solely on the certificate verification algorithm?

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?

• @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. Jan 16 at 22:54
• @D.W. Sure! I have turned my comment into an answer. Jan 16 at 23:25

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.