Solving #SAT through TQBF

Question

I'm not extremely proficient with counting complexity classes, but since #SAT is #P-complete, its decision version, let's call it #SAT(D) (is the number of solutions less than some $k$), is in PSPACE. So there is a reduction from #SAT(D) to TQBF. This reduction should produce a QBF sentence that is true iff a given SAT instance has less than a given number $k$ of solutions.

But is there any known concrete translation to obtain such a QBF sentence? That is, a direct algorithm to encode #SAT(D) instances as equivalente QBF sentences?

I don't mean necessarily something usable in practice to solve #SAT with QBF solvers, but at least some effective encoding.

Answer 1

Let $\phi$ be a CNF formula. I'll show how to express a TQBF formula of polynomial size for your problem.

In particular, let $\psi_i(t,j)$ be a formula that is true if there are at most $j$ values $x$ such that (1) the first $i$ bits of $x$ are $t$, and (2) $x$ satisfies $\phi$. Here $t \in \{0,1\}^i$ is a $i$-bit string, and $j \in \{0,1\}^n$ is a number in $0 \le j < 2^n$, where $n$ counts the number of variables in $x$. I'll show how to construct all of the $\psi_i$'s; and then $\psi_0(\epsilon,k-1)$ will be the formula you're looking for.

Notice that $\psi_n(t,j)$ is easy to express in TQBF: $\psi_n(t,1)$ is always true, and $\psi_n(t,0)$ is $\neg \phi(t)$, so $\psi_n(t,j) = (j \ne 0) \lor \neg \phi(t)$.

Also, we can express $\psi_i(t,j)$ as follows:

$$\psi_i(t,j) = \exists j_0 \in \{0,1\}^n . (0 \le j_0 \le j \land \psi_{i+1}(t0,j_0) \land \psi_{i+1}(t1,j-j_0)).$$

This can be re-expressed in the following equivalent form:

$$\psi_i(t,j) = \exists j_0 . (0 \le j_0 \le j) \land \forall t' . \forall j' . ((t'=t0 \land j'=j_0) \lor (t'=t1 \land j'=j-j_0)) \implies \psi_{i+1}(t',j').$$

Let $|\psi_i|$ denote the size of the formula $\psi_i$. We see that $|\psi_i| = |\psi_{i+1}| + \text{poly}(n)$. It follows that $|\psi_0| = \text{poly}(n)$, so we have obtained the desired formula.

This is basically mimicing the standard proof that TQBF can express all of PSPACE, specialized to your particular problem.