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?


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

  • $\begingroup$ I knew I was missing something obvious, thank you for the simple counterexample. I am still curious if this method always works for sentences of the form $\exists \exists ... \forall \forall$ but that's a separate question. Thanks again! $\endgroup$ Commented Sep 15, 2020 at 14:02
  • $\begingroup$ Uh.. unless there's a typo there, yes it does? That reduces to $(a)\wedge (a)$ which is trivially satisfiable, as is the original sentence with the same variable setting. $\endgroup$ Commented Sep 15, 2020 at 20:10
  • $\begingroup$ @nick.schachter, you're right, sorry, I guess I wasn't thinking straight. My mistake. Thank you. $\endgroup$
    – D.W.
    Commented Sep 16, 2020 at 3:04
  • $\begingroup$ No problem. I was able to find a counterexample. In the original sentence I posted, if you set the quantifies as $\exists a \exists b \forall c \forall d$ the method fails. I believe I can characterize exactly when it will/won't work: if there is a fixed setting of the universally quantified variables such that no clause in the sentence is satisfied before the existentially quantified variables are set, then this method will work. Otherwise it might well fail. $\endgroup$ Commented Sep 16, 2020 at 3:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.