5
$\begingroup$

TQBF(Totally Quantified Boolean Formula) is a PSPACE-complete question. I wonder that if it restricted to CNF is still PSPACE-complete. TQBF-CNF means that the part following the quantifier is a CNF.
I tried to prove that TQBF can be reduced to TQBF-CNF but failed as it need an exponential time to change a formula into CNF.
I would much appreciate an answer or an idea

$\endgroup$

1 Answer 1

5
$\begingroup$

Yes, it is still PSPACE-complete. Let $Q_1 x_i \cdots Q_k x_k . \varphi(x_1,\dots,x_k)$ be a TQBF problem, where each $Q_i$ is a quantifier. Apply the Tseytin transform to $\varphi(x_1,\dots,x_k)$ to get an equisatisfiable CNF formula $\Psi(x_1,\dots,x_k,x_{k+1})$, so that $\varphi(x_1,\dots,x_k) \Leftrightarrow \exists x_{k+1} . \Psi(x_1,\dots,x_k,x_{k+1})$. Then the original TQBF problem is equivalent to $$Q_1 x_1 \cdots Q_k x_k \exists x_{k+1} .\Psi(x_1,\dots,x_k,x_{k+1}),$$ which is an instance of TQBF-CNF. Therefore, any algorithm to solve TQBF-CNF can be used to solve TQBF.

As explained in Wikipedia, the size of $\Psi$ is polynomial in the size of $\varphi$. Note that $x_{k+1}$ might represent multiple variables. The number of added variables is also polynomial in the size of $\varphi$.

See also Is there a known way to convert any $QBF_2$-formula into an equisatisfiable $QBF_2$-formula in CNF in polynomial time?.

$\endgroup$
3
  • $\begingroup$ Thanks for the answer! But I'm confused abut of the number of variables in $\Psi$, why do we need to add exactly one variable? In wikipedia, the example has the same number of variables after Tseytin transform. $\endgroup$
    – ywang22THU
    Commented May 4 at 5:11
  • $\begingroup$ @ywang22THU, see revised answer. It certainly doesn't have the same number of variables: the Tseytin transform adds more variables. If you're not clear how the Tseytin transform works, I suggest spending some time studying up on it -- search for other expositions of it, try working through a few simple examples with pencil and paper, etc. -- and if you're still stuck, ask a new question about whatever specific aspect you can't figure out. $\endgroup$
    – D.W.
    Commented May 4 at 5:18
  • $\begingroup$ Got it! I tried some examples just know. The number of extra variables is equivalent with the subformulas expect literals. Thanks! $\endgroup$
    – ywang22THU
    Commented May 4 at 5:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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