Universal Quantifiers in QBFs

Question

I've been looking into reductions to/from the TQBF language and have managed to get stuck on something that is almost certainly not true (or, if it is true I'm missing a significant computational cost associated with it) with respect to simplifying TQBF instances.

For the sake of simplicity, let's restrict attention to TQBF instances in prenex normal form and CNF with no free variables. My hypothesis (which I strongly suspect is wrong, but have been unable to find a counter-example) is that such a TQBF is satisfiable if and only if the TQBF that results from removing all instances of universally quantified variables from the sentence is satisfiable. For example, take the following instance:

$\exists a \forall b \exists c \forall d$ $\psi(a,b,c,d)$

$\psi(a,b,c,d) = (\neg a \vee b \vee c)\wedge (\neg b \vee \neg c \vee d)\wedge (a \vee c \vee \neg d)$

First, I contend that this instance is not satisfiable (easily verifiable by hand). If we apply the method I describe above, we get the following "core":

$\exists a \exists c$ $\phi(a,c)$,

$\phi (a,c) = (\neg a \vee c)\wedge (\neg c) \wedge (a \vee c)$

which is clearly not satisfiable. If instead of this example we look at this:

$\exists a \forall b \exists c \forall d$ $\psi(a,b,c,d)$

$\psi(a,b,c,d) = (\neg a \vee b \vee \neg c)\wedge (\neg b \vee c \vee d)\wedge (a \vee c \vee \neg d)$

which clearly is satisfiable (set c to true, a to false) and which has a "core" of

$\exists a \exists c$ $\phi(a,c)$,

$\phi (a,c) = (\neg a \vee \neg c)\wedge (c) \wedge (a \vee c)$

that is also satisfiable with the same variable settings.

If this method always works, that would seem to imply that there is a reduction from TQBF to SAT in time linear in the number of universal quantifiers and the number of occurrences of the universally quantified variables in the formula, showing that TQBF is NP-Complete (it is already known to be PSPACE-Complete and thus NP-Hard, so if it is in NP it is NP-Complete) and furthermore that NP=PSPACE. I would be utterly stunned if this is the case, but I have been unable to find a counterexample (or a missing computational cost in the reduction that makes it not polynomial time). What am I missing?

Answer 1

Your intuition was right. It doesn't work. Here is a counterexample.

Consider $\forall a \exists b \varphi(a,b)$ where $\varphi(a,b) = (a \lor \neg b) \land (\neg a \lor b)$. This statement evaluates to true.

However, if we remove $a$ following your procedure, we get $\exists b \psi(b)$ where $\psi(b) = ((\neg b) \land (b))$; and that statement evaluates to false.

One way to understand why your method doesn't work is that $\forall a \exists b \varphi(a,b)$ isn't equivalent to $\exists b \forall a \varphi(a,b)$. At most your method might work if all of the $\forall$'s are on the inside, i.e., for a sentence of the form $\exists \cdots \exists \forall \cdots \forall$, but not for any other pattern of $\exists$ and $\forall$.