snippetMinor
Is there a known way to convert any $QBF_2$-formula into an equisatisfiable $QBF_2$-formula in CNF in polynomial time?
Viewed 0 times
qbf_2polynomialconvertintoanywaycnftimeequisatisfiableknown
Problem
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:
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$.
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.
$$
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:
- 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$.
- 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.
Solution
-
Yes, for exactly the reasons you listed.
-
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.
Yes, for exactly the reasons you listed.
-
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.
Context
StackExchange Computer Science Q#41587, answer score: 2
Revisions (0)
No revisions yet.