Can QBF encode #QBF?

Question

In another question Initializing non-deterministic variables in QBF, I was interested about translating assertion-based pseudocode to QBF in order to have an exponentially more compact encoding compared to unrolling deeply nested loops into SAT.

While some misunderstandings in the pseudocode for that question ultimately led to several answers adding in 'cheating' simplifications not in the spirit of the original question, D.W. clarified that a full answer depends on the relationship between PSPACE and #PSPACE.

Formally PSPACE and #PSPACE are "incompatible" for comparison in a sense of being a decision problem versus a counting problem, but this artifact can be made consistent in analogy to PH versus #P. Decision classes such as PP and ⊕P find the most-significant bit of the #P counting problem and least-significant bit respectively. Reductions filling in the rest of the bits of #P output should be rather straightforward given a powerful PSPACE-complete oracle, since P^#P ⊂ PH ⊂ PSPACE.

Looking at the following assertion pseudocode, it's obvious that counting solutions to either SAT (#SAT) or QBF (#QBF) is trivially possible using polynomial-space. For example, the following pseudocode would naively run in exponential time, but never uses more than a linear O(n) amount of memory. This renders, via abuse of notation, #PSPACE ⊂ PSPACE.

counter = 0
for loop_aux_0 in {0,1}:
  for loop_aux_1 in {0,1}:
    for loop_aux_2 in {0,1}:
      .
        .
          .
            for loop_aux_n in {0,1}: 
              counter += f(loop_aux_0, loop_aux_1, .., loop_aux_n)
assert(counter != UINT_MAX)

Here f is an arbitrary PSPACE function that outputs 0 or 1.

If there are no objections that #PSPACE ⊂ PSPACE, how can I actually encode #QBF as part of a QBF instance?

I suggested a QBF implementation (although missing initialization) utilizing an adder circuit for counter with its output fed back in as input alongside f_ouput being the carry-in of the LSB:

∃ counter[n] ∀ loop_aux[n] ∃ f_output[1] (counter += f_output) & (f_output == f(loop_aux_0, loop_aux_1, .., loop_aux_n))

The problem with this encoding is that the counter is incremented non-deterministically without initialization, rendering any value of counter satisfiable. Can this encoding be saved with additional clauses or auxiliary variables to initialize the counter? Or is there a better way to encode #QBF in QBF?

Answer 1

Strictly speaking, this is a category confusion: it's an apples-vs-pears comparison. You can't compare SAT to #SAT; SAT is a decision problem (determine whether a formula $\varphi$ has a satisfying instance), #SAT is a counting problem (count the number of satisfying assignments to $\varphi$). They have a different API: they both take a formula $\varphi$ as input, but SAT outputs either "satisfiable" or "not satisfiable", while #SAT outputs a number. They're not the same, and you can't encode a #SAT instance as a SAT instance.

The same is true for counting the number of values of $x$ that satisfy a formula $\varphi(x)$, where $\varphi$ contains nested quantifiers (e.g., $\varphi(x) = \exists y . \forall z . \psi(x,y,z)$ or something). It's a category error: one is a decision problem, the other is a counting problem.

---

However, you might be interested in the following paper:

Richard E. Ladner. Polynomial Space Counting Problems. SIAM Journal of Computing, vol 18 no 6, pp.1087--1097, December 1989.

See, for instance, the discussion of $\natural$QBF, $\natural$PSPACE, and FPSPACE(poly).

Definitions:

• $\natural$QBF is the following problem: given a QBF instance like $\varphi(x,y,z) = \exists x \forall y \exists z \psi(x,y,z)$, count the number of values $x$ such that $\forall y \exists z \psi(x,y,z)$ is true (except that is for an arbitrary number of quantifiers, not limited to just 3).

• A function $f:\{0,1\}^* \to \mathbb{N}$ is in $\natural$PSPACE if there's a polynomial-space nondeterministic Turing machine $x$ such that $f(x)$ counts the number of accepting computations of $M$ on input $x$, and $M$ makes only a polynomial number of nondeterministic choices.

• A function $f:\{0,1\}^* \to \mathbb{N}$ is in FPSPACE(poly) if $f(x)$ is bounded by a polynomial in the length of $x$ and there's a deterministic polynomial-space algorithm (Turing machine) that computes $f$.

The paper proves that $\natural$PSPACE = FPSPACE(poly) and that $\natural$QBF is complete for $\natural$PSPACE and that there is a polynomial-space algorithm for computing $\natural$QBF.

We could consider the following problem:

BIT_OF_COUNT: Input: an index $i$ and a QBF instance $\varphi$
Desired output: the $i$th bit of the solution to this QBF instance.

This is one way to build a decision problem associated with a $\natural$QBF instance.

By the above remarks, BIT_OF_COUNT is in FPSPACE(poly) (since $\natural$QBF is). Since its output is in 0 or 1, that means BIT_OF_COUNT is actually in PSPACE. Since QBF is complete for PSPACE, that it must be possible to reduce BIT_OF_COUNT to QBF, i.e., to translate an instance for BIT_OF_COUNT into an instance for QBF, by chaining all the reductions.

It sounds like this might be what you want. So, if you study that paper and chain all the reductions together, you might get what you want. It looks a bit intimidating on first glance, but perhaps if you understand the meat of the reductions you'll be able to simplify somehow. The key trick in the paper seems to be the one used on pages 1091--1092, using ann algorithm to compute the product or sum of two $b$-bit numbers in $O(\lg b)$ space as a subroutine.

I hope someone will be able to give you a better answer.