Question

Show that TQBF restricted to formulas where the part following the quantifiers is in conjunctive normal form is still PSPACE-complete.

Short answer

The view of the preceding reasoning, the reduction maps in polynomial time formula $Q\varphi$to the equivalent t.q.b.f. with c.n.f. unquantified portion$Q\left(\exists x\right)x\wedge C_{\varphi ,x}$.

Step-by-step solution

Step-1: To PSPACE collect the problems

PSPACE is the collection of all decision problems that a Turing machine can answer using a polynomial space in computational complexity theory.

It turns out that allowing the turing machine to be nondeterministic does not add any extra power. Because of Savitch’s theorem.

Step-2: To explain TQCNF PSPACE

The limited version's language should be TQCNF. PSPACE is unmistakably home to TQCNF. Then, to show that it is PSPACE-complete, provide a polynomial time reduction from TQBF to TQCNF. Let's say $\phi$is the symbol for t.q.b.f.

It can assume that all quantifiers are at the beginning and that their scope is everything that follows using a simple polynomial time translation. Let $Q$indicate the formula's string of quantifiers $\phi$, and let $\varphi$be the formula's unquantified component, so that $\phi =Q\varphi$.

The logical approach of adding $\varphi$in c.n.f. using distributivity and de Morgan's laws does not work since, in the worst-case scenario, it generates an exponentially large formula. A formula role="math" localid="1663222782552" $A\vee \left(x\wedge y\right)$containing a subformula $A$becomes role="math" localid="1663222830747" $\left(A\vee x\right)\wedge \left(A\vee y\right)$with $A$appearing twice.

To construct the CNF formula

We can get around this by using supplementary variables, equivalence, and quantifiers, and substituting $A\vee \left(x\wedge y\right)$with the equivalent formula role="math" localid="1663223949181" $\left(\exists z\right)\left(z\equiv A\right)\wedge \left(z\vee x\right)\wedge \left(z\vee y\right)$, where $A$only appears once. The formula role="math" localid="1663223717280" $\left(\overline{A}\vee B\right)\wedge \left(\overline{B}\vee A\right)$for logical equivalence can be found here $A\equiv B$as a shortcut. We need to find a CNF formula that is equivalent $x\equiv A$to conclude the argument. Construct a CNF formula role="math" localid="1663223682135" $C_{A,x}$with an extra free variable $x$that is equivalent to $x\equiv A$. given a boolean formula $A$without quantifiers $x\equiv A$. We'll show how to implement it in a recursive manner:

• If $A$is a variable $y$, then role="math" localid="1663223847409" $C_{A,x}$is $\left(\overline{x}\vee y\right)\wedge \left(\overline{y}\vee x\right)$. (CNF has been expanded as $x\equiv y$)

• If $A$is $\overline{B}$, then role="math" localid="1663224265355" $C_{A,x}$is $\left(\exists z\right)C_{B,z}\wedge \left(z\vee y\right)\wedge \left(\overline{y}\vee \overline{z}\right)$. (CNF has been expanded as $(\exists z)(z\equiv B)\wedge (\overline{z}\equiv x)$)

• If $A$is $B\vee D$, then $C_{A,x}$is role="math" localid="1663224692220" $\left(\exists z,w\right)C_{B,z}\wedge C_{D,w}\wedge \left(\overline{w}\vee x\right)\wedge \left(\overline{z}\vee x\right)\wedge \left(\overline{x}\vee z\vee w\right)$. (CNF has been expanded as role="math" localid="1663224800188" $\left(\exists z,w\right)\left(z\equiv B\right)\wedge \left(w\equiv D\right)\wedge \left(\left(z\wedge w\right)\equiv x\right)$)

• If $A$is $B\wedge D$, then $C_{A,x}$is role="math" localid="1663224829130" $\left(\exists z,w\right)C_{B,z}\wedge C_{D,w}\wedge \left(\overline{x}\vee w\right)\wedge \left(\overline{x}\vee z\right)\wedge \left(x\vee \overline{z}\vee \overline{w}\right)$. (CNF has been expanded as $\left(\exists z,w\right)\left(z\equiv B\right)\wedge \left(w\equiv D\right)\wedge \left(\left(z\wedge w\right)\equiv x\right)$)

Therefore, The view of the preceding reasoning, the reduction maps in polynomial time formula role="math" localid="1663225059953" $Q\varphi$ to the equivalent t.q.b.f. with c.n.f. unquantified portion role="math" localid="1663225034062" $Q\left(\exists x\right)x\wedge C_{\varphi ,x}$.