<p>Let <span class="math-container">$\phi$</span> be a CNF formula.  I'll show how to express a TQBF formula of polynomial size for your problem.</p>
<p>In particular, let <span class="math-container">$\psi_i(t,j)$</span> be a formula that is true if there are at most <span class="math-container">$j$</span> values <span class="math-container">$x$</span> such that (1) the first <span class="math-container">$i$</span> bits of <span class="math-container">$x$</span> are <span class="math-container">$t$</span>, and (2) <span class="math-container">$x$</span> satisfies <span class="math-container">$\phi$</span>.  Here <span class="math-container">$t \in \{0,1\}^i$</span> is a <span class="math-container">$i$</span>-bit string, and <span class="math-container">$j \in \{0,1\}^n$</span> is a number in <span class="math-container">$0 \le j &lt; 2^n$</span>, where <span class="math-container">$n$</span> counts the number of variables in <span class="math-container">$x$</span>.  I'll show how to construct all of the <span class="math-container">$\psi_i$</span>'s; and then <span class="math-container">$\psi_0(\epsilon,k-1)$</span> will be the formula you're looking for.</p>
<p>Notice that <span class="math-container">$\psi_n(t,j)$</span> is easy to express in TQBF: <span class="math-container">$\psi_n(t,1)$</span> is always true, and <span class="math-container">$\psi_n(t,0)$</span> is <span class="math-container">$\neg \phi(t)$</span>, so <span class="math-container">$\psi_n(t,j) = (j \ne 0) \lor \neg \phi(t)$</span>.</p>
<p>Also, we can express <span class="math-container">$\psi_i(t,j)$</span> as follows:</p>
<p><span class="math-container">$$\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)).$$</span></p>
<p>This can be re-expressed in the following equivalent form:</p>
<p><span class="math-container">$$\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').$$</span></p>
<p>Let <span class="math-container">$|\psi_i|$</span> denote the size of the formula <span class="math-container">$\psi_i$</span>.  We see that <span class="math-container">$|\psi_i| = |\psi_{i+1}| + \text{poly}(n)$</span>.  It follows that <span class="math-container">$|\psi_0| = \text{poly}(n)$</span>, so we have obtained the desired formula.</p>
<p>This is basically mimicing the standard proof that TQBF can express all of PSPACE, specialized to your particular problem.</p>

CC BY-SA 4.0
2024-07-11T19:48:23.073Z
That's very interesting! I'm not sure I get what you mean by $\exists j_0$ and then the subtraction $j-j_0$. As far as I understand, $j_0$ is a number? Over what are we quantifying here?
Nicola Gigante
CC BY-SA 4.0
2024-07-11T21:29:04.267Z
@NicolaGigante, I've updated my answer to add more clarification.  Yes, $j$ and $j_0$ are numbers.  See revised answer - hopefully it is clearer now?
D.W.
CC BY-SA 4.0
2024-07-12T06:02:42.047Z
Yes, thanks, so this means the formula has to express the arithmetic subtraction when you do $j - j_0$, right?
Nicola Gigante
CC BY-SA 4.0
2024-07-12T19:51:22.653Z
@NicolaGigante, yup!
D.W.
CC BY-SA 4.0
2024-07-11T19:27:00.630Z
2024-07-11T21:28:23.653Z
2024-07-11T21:28:23.653Z
D.W.
<p>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 <span class="math-container">$k$</span>), 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 <span class="math-container">$k$</span> of solutions.</p>
<p>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?</p>
<p>I don't mean necessarily something usable in practice to solve #SAT with QBF solvers, but at least some effective encoding.</p>

CC BY-SA 4.0
2024-07-11T19:15:01.350Z
What's wrong with applying the standard reduction to convert any algorithm into a TQBF formula, to this specific instance?
D.W.
<cc.complexity-theory><reference-request><sat><pspace>
Solving #SAT through TQBF
Nicola Gigante
# Solving #SAT through TQBF

(Asked by: username_0 on 2024-07-11)

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.

**Tags:** cc.complexity-theory, reference-request, sat, pspace
> **Comments:**
> **username_1**: What's wrong with applying the standard reduction to convert any algorithm into a TQBF formula, to this specific instance?  

---

## 1 answers

### Answer by username_1 on 2024-07-11. Score: 3 | Accepted answer

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.

> **Comments:**
> **username_0**: That's very interesting! I'm not sure I get what you mean by $\exists j_0$ and then the subtraction $j-j_0$. As far as I understand, $j_0$ is a number? Over what are we quantifying here?  
> **username_1**: @NicolaGigante, I've updated my answer to add more clarification.  Yes, $j$ and $j_0$ are numbers.  See revised answer - hopefully it is clearer now?  
> **username_0**: Yes, thanks, so this means the formula has to express the arithmetic subtraction when you do $j - j_0$, right?  
> **username_1**: @NicolaGigante, yup!  

---

