If boolean formula $f$ is in CNF it is known that:$$\forall x \exists y_1 \exists y_2 .. \exists y_n : f(x, y_1, y_2..y_n) :\iff \exists y_1 \exists y_2 .. \exists y_n : f(0, y_1, y_2..y_n) \land f(1, y_1, y_2..y_n) :\iff \exists y_1 \exists y_2 .. \exists y_n : f(y_1, y_2..y_n) :\iff f(y_1, y_2..y_n)$$ Last formula is non-quantified CNF. For multiple $\forall$-quantified variables same reduction is also possible. SAT is NP problem, QSAT is PSPACE-complete (even in CNF). Does this involve that NP = PSPACE?
1 Answers
Each of your purported equivalences is problematic:
In the first one, you seem to be moving $\forall x$ willy-nilly inside the $\exists$s. This does not preserve meaning: $$ \forall x\exists y (x=y) \qquad\text{and}\qquad \exists y(0=y\land 1=y) $$ are not equivalent -- the first one is obviously true and the second one just as obviously false.
In the second one, $f$ inexplicably changes from having $n+1$ parameters to having only $n$. What is going on there? Is it even the same $f$?
In the third one, where do the quantifiers suddenly go? You seem to be asserting that the formula $\exists y_1\cdots \exists y_n(f(y_1,\ldots,y_n))$ which has no free variables is equivalent to $f(y_1,\ldots,y_n)$ which has $n$ of them. Unless you imagine that the truth value of $f$ does not depend on its variables at all (which you don't seem to have any reason to), this can't be true.
Finally, your plan seems to be to prove that PSPACE${}\subseteq{}$NP by reducing QSAT to SAT. However, even if your equivalences worked, if you have $n$ universal quantifiers repeating your first rewrite for each of them would blow up the formula by a factor of $2^n$, so it is not a polynomial-time reduction and would not say anything about QSAT being in NP.
- 286,031
-
First. (x = y) is not in CNF. It's CNF: (not x + y) (x + not y). With my rule it is y + not y = 0. Second. They are not the same but equisatisfiable. Third. SAT problem is TQBF with all existence quantifiers. Finally. Remove variables is linear time task. – rus9384 May 04 '17 at 17:59
-
I can't understand why ∀x∃y (x = y) is true. Does it differ from ∃y∀x (x = y)? – rus9384 May 04 '17 at 18:19
-
Now I understood. (x = y) has solution 1001. First half of formula (10) is satisfiable, second (01) too, so, TQBF is true. – rus9384 May 04 '17 at 19:51