Significance of quantifier ordering in quantified boolean formulas (kQBF vs. QBF) I am studying solvers of quantified boolean formulas (QBF) as a generalization of SAT solving. The standard DIMACS format of SAT specification is extended to QDIMACS, which adds "a ..." and "e
..." lines denoting which variables are to be existentially quantified and which variables are to be universally quantified.

For instance, a simple QDIMACS input such as:

p cnf 2 3
a 1 0
e 2 0
1 2 0
-1 0
-2 0


...would be correspond to the formula $\forall x \exists y \ (x \lor y) \land \neg x \land \neg y$ where $x$ and $y$ range over $\{T, F\}$. SAT is an instance of QBF where all the variables are existential.

The above is an example of 2QBF, where we have two layers of quantifiers. A more complex QDIMACS problem with alternating quantifiers might be: 

p cnf 2316 15282
e 1 17 2 18 3 19 4 ... 0
a 1598 1599 1600 1601 1602 1603 0
e 65 81 66 82 67 83 68 ... 0
a 1610 1611 1612 1613 1614 1615 0
e 193 209 194 210 195 211 196 ... 0
a 1616 1617 1618 1619 1620 1621 0
-2 -18 0
-3 -19 0
-4 -20 0
-5 -21 0
-6 -22 0
-7 -23 0
...


Anyways, on to my question. I don't understand why 2QBF != QBF. It seems to me for any formula $F$ and variables $x$, $y$ ranging over the booleans that $\forall x \exists y \ F$ is equivalent to $\exists y \forall x \ F$.

To demonstrate my thinking, I will consider the Shannon expansion of the universal quantifier.

\begin{align}
\forall x \exists y \ F \iff&amp; (\exists y \ F[x \to T]) \land (\exists y \ F[x \to F]) \\\\
\exists y \forall x \ F \iff&amp; \exists y \ (F[x \to T] \land F[x \to F])
\end{align}




Suppose $\exists y \ (F[x \to T] \land F[x \to F])$ is satisfiable. Then the same assignment would extend to both $\exists y \ F[x \to T]$ and $\exists y \ F[x \to F]$.
Suppose $\exists y \ (F[x \to T] \land F[x \to F])$ is unsatisfiable. Then at least one of $\exists y \ F[x \to T]$ or $\exists y \ F[x \to F]$ is also unsatisfiable.


Thus $\forall x \exists y \ F \iff \forall y \exists x \ F$.



A similar question has been asked before here, but there appears to be ambiguity over the domain of the quantifiers. They should range only over true or false and not over other mathematical objects or propositional variables. This is in correspondence to the standard interpretation of the SAT problem.

For instance, $\forall x \exists y \ x \leftrightarrow y$ would not be true since setting $y$ to $x$ is not valid.

Is my interpretation of QBF correct? Is there a counterexample I'm missing?
Let me first give a concrete example of a formula $F(x,y)$ such that $\forall x \exists y. F(x,y)$ is true, but $\exists x \forall y. F(x,y)$ is false.
I'll then address the expansion of the universal quantifier in your question.

Take $F(x,y)$ to be a formula expressing the equality $x \oplus y = 1$, where $\oplus$ denotes exclusive-or.
We can explicitly write $F$ as $$F(x,y) = (x \land \neg y) \lor (\neg x \land y).$$

To see that $\forall x \exists y. F(x,y)$ is true, let $x$ be given and take $y = \neg x$.
Then $x \oplus y = x \oplus \neg x = 1$.

To see that $\exists x \forall y. F(x,y)$ is false, first take $x = 1$. Then for $y = 1$, we have that $F(x,y)$ is false, i.e., $F(1,1)$ is false.
By the same reasoning, $F(0,0)$ is false, so there is no $x$ such that $\forall y. F(x,y)$ is true.
Hence $\exists x \forall y. F(x,y)$ is false.



Your mistake is in the following argument.


  Suppose $\exists y\ (F[x \to T] \land F[x \to F])$ is unsatisfiable. Then at least one of $\exists y\ F[x \to T]$ or $\exists y\ F[x \to F]$ is also unsatisfiable.


The point is that $\exists y\ F[x \to T]$ and $\exists y\ F[x \to F]$ may both be satisfiable, but the choice of $y$ which satisfies them may be different.
In order to satisfy $\exists y\ (F[x \to T] \land F[x \to F])$, you must find a single value of $y$ that satisfies both $F[x \to T]$ and $F[x \to F]$ simultaneously.
This may not be possible, even if it is easy to satisfy one of $F[x \to T]$ and $F[x \to F]$ individually.

It may be helpful to expand your argument using the example I gave to see exactly where it breaks down.