Initializing non-deterministic variables in QBF I'm trying to translate the following pseudocode to QBF. The integers are encoded as simple fixed-width bitvectors, and the entire procedure runs in polynomial space ensuring QBF has enough representational power for a compact formula.

The following formula is nested to a linear depth in n, producing 2^n increments when unrolled. Using QBF allows for an exponentially more compact encoding than SAT. QBF solvers can typically handle thousands of variables, SAT solvers handle millions. For even modest values of n, such as n=30, unrolling to SAT would produce billions of variables (impractical), while a QBF encoding would be extremely practical with only tens of variables.

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 &gt; 0)


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

This suggests a QBF implementation (although missing initialization) utilizing an adder circuit with its output fed back in as input:

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

How can I add clauses or auxiliary variables to simulate sequential counter initialization?
It looks to me like there is some confusion here about what QBF is and when it is needed.  You don't need QBF for this problem; SAT is fine.

Here's how to solve this using a SAT solver. Notice that the condition counter &gt; 0 is true at the end if and only if there was at least one loop iteration where f output 1.  In other words, the assertion will be true if and only if

$$\exists \mathtt{loop\_aux\_0},\dots,\mathtt{loop\_aux\_n} . \mathtt{f}(\mathtt{loop\_aux\_0},\dots,\mathtt{loop\_aux\_n})=1.$$

That can be expressed as a SAT instance.  There are no nested/alternating quantifiers; the formula has the form $\exists x. \varphi(x)$, so it can be solved by SAT.  Simply express the condition f(loop_aux_0, ..., loop_aux_n)=1 in CNF form, and then use a SAT solver to check whether that condition can ever be true (for any value of the loop variables).



QBF is useful when you have nested quantifiers, e.g., $\exists x . \forall y . \exists z . \varphi(x,y,z)$.  The result will be either true or false.

It's also worth knowing about #SAT.  #SAT is useful when you want to count the number of satisfying assignments to some formula $\varphi(x)$.  In other words, instead of checking whether $\exists x . \varphi(x)$ is true, suppose we want to know the number of values $x$ such that $\varphi(x)$ is true; then this is an instance of #SAT.

QBF and #SAT are not the same thing.  They're different problems.  And QBF isn't some kind of magic wand that lets you compress any SAT instance by some enormous factor; QBF is for a specific type of logical formula.