3
$\begingroup$

It is easy to turn any boolean formula and any quantified boolean formula into an equisatisfiable formula in CNF using Tseitin transformation:

$$ Q_1 z_1 Q_2 z_2 \ldots Q_n z_n \Phi \Rightarrow Q_1 z_1 Q_2 z_2 \ldots Q_n z_n \exists x ((\neg{x} \vee \Psi) \wedge \Phi[x/\Psi] ),\ Q_i \in \{ \exists, \forall \} $$

(For details, see for example here). My two questions are:

  1. Can any formula of the form $\forall z_1 \ldots \forall z_n \exists z_{n+1} \ldots \exists z_m \Phi$ be turned into an equisatisfiable formula of the same form (so beginning with $\forall$ and with just one alternation of quantifiers) in CNF using Tseitin transformation? I'm assuming Yes, since Tseitin transformation only adds existential quantifiers ($\exists$) right before $\Phi$.
  2. Can any formula of the form $\exists z_1 \ldots \exists z_n \forall z_{n+1} \ldots \forall z_m \Phi$ also be converted into an equisatisfiable formula of the same form (so beginning with $\exists$ and with just one alternation of quantifiers) in CNF in polynomial time? I'm assuming No since Tseitin transformation would give us the form $\exists z_1 \ldots \exists z_n \forall z_{n+1} \ldots \forall z_m \exists x_1 \ldots \exists x_l \Phi'$ and I'm not aware of any other polynomial time transformation useful in this case.
$\endgroup$
1
$\begingroup$
  1. Yes, for exactly the reasons you listed.

  2. I don't know of any way to do what you want. However, it is possible to convert it to a formula of the form $\neg \forall x \exists y \Psi$ (negate it, then convert $\neg \Phi$ to CNF via the Tseitin transform and let $\Psi$ be the result), so if you have an oracle that will solve QBF2-CNF queries, it can be used to solve QBF2 queries.

$\endgroup$

Your Answer

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

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