Solving 2-CNF TQBF with #SAT solver?

Question

We clearly know that 2-QCNF is in $\mathsf{P}$. Since that, if I understand it right, it is possible to solve it with #SAT solver (because $\mathsf{P} \subseteq \mathsf{\#P}$). But how can we only knowing amount of positive assignments for some non-quantified formulae solve 2-QCNF? And why this doesn't hold (at least, assumed so) for general case of TQBF?

Answer 1

First of all, it is a bit misleading to say that $\mathsf{P} \subseteq \mathsf{\#P}$, since $\mathsf{P}$ is a class of decision problems, while $\mathsf{\#P}$ is a class of counting problems. However, we can think of a decision problem as a counting problem in which the answer is 0 (no) or 1 (yes), and in that sense it is certainly true that $\mathsf{P} \subseteq \mathsf{\#P}$.

The problem $\mathsf{\#SAT}$ is $\mathsf{\#P}$-complete. This means that for any problem $A \in \mathsf{\#P}$ there exists a polynomial time reduction $f$ such that for any instance $x$ of $A$, we have $$ A(x) = \mathsf{\#SAT}(f(x)), $$ where $A(x)$ is the value of the counting problem $A$ on instance $x$.

Since $\mathsf{2QCNF} \in \mathsf{P}$, there is a trivial reduction from $\mathsf{2QCNF}$ to $\mathsf{\#SAT}$: if the $\mathsf{2QSAT}$ is satisfiable, we output the formula $x$, and otherwise we output the formula $x \land \lnot x$. This reduction runs in polynomial time since $\mathsf{2QCNF} \in \mathsf{P}$.