1
$\begingroup$

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 > 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) & (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?

$\endgroup$
  • $\begingroup$ 1. See my edit of the pseudocode. Does it correspond to what you actually have in mind? 2. Please update the formula you have at the end to match the pseudocode, as it never got updated by your edits. 3. I suspect you are confusing QBF with #SAT. They are not the same thing. $\endgroup$ – D.W. Jun 9 '16 at 5:51
0
$\begingroup$

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 > 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.

$\endgroup$
  • $\begingroup$ @JoelSnyder, as far as I know, I don't think you can encode #QBF in QBF (I think #PSPACE is different from PSPACE, as far as we know). If that's what you want to do, I suggest asking a new question about whether that can be done. $\endgroup$ – D.W. Jun 9 '16 at 17:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy