World's most popular travel blog for travel bloggers.

# [Answers] Is there a known way to convert any $QBF_2$-formula into an equisatisfiable $QBF_2$-formula in CNF in polynomial time?

, ,
Problem Detail:

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.

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.