TQBF is PSPACE-complete
TQBF is in PSPACE
"On input , a fully quantified Boolean formula:
If contains no quantifiers, then it is an expression with only constants, so evaluate and if it is true; otherwise, . If equals , recursively call on , first with 0 substituted for and then with 1 substituted for . If either result is accept, then ; otherwise, . If equals , recursively call on , first with 0 substituted for and then with 1 substituted for If both results are accept, then ; otherwise, ."
The depth of the recursion is at most the number of variables. At each level we need only store the value of one variable, so the total space used is where is the number of variables that appear in Therefore, runs in linear space.
TQBF is PSPACE-hard
Let be a language decided by a TM in space for some constant We give a polynomial time reduction from to . The reduction maps a string to a quantified Boolean formula that is true iff accepts
Using two collections of variables denoted and representing two configurations and a number we construct a formula If we assign and to actual configurations, the formula is true iff can go from to in at most steps. Then we can let be the formula where for a constant , chosen so that has no more than possible configurations on an input of length Here, let For convenience, we assume that is a power of 2.
The formula encodes the contents of configuration cells as in the proof of the Cook-Levin theorem. Each cell has several variables associated with it, one for each tape symbol and state, corresponding to the possible settings of that cell. Each configuration has cells and so is encoded by variables.
If we can easily construct We design the formula to say that either equals or follows from in a single step of We express the equality by writing a Boolean expression saying that each of the variables representing contains the same Boolean value as the corresponding variable representing We express the second possibility by using the technique presented in the proof of the Cook-Levin theorem. That is, we can express that yields in a single step of by writing Boolean expressions stating that the contents of each triple of 's cells correctly yields the contents of the corresponding triple of 's cells.
If , we construct recursively. Let
The introduction of the new variables representing the configurations and allows us to "fold" the two recursive subformulas into a single subformula, while preserving the original meaning. By writing we indicate that the variables representing the configurations and may take the values of the variables of and or of and respectively, and that the resulting formula is true in either case. We may replace the construct with the equivalent construct to obtain a syntactically correct quantified Boolean formula.
To calculate the size of the formula where we note that each level of the recursion adds a portion of the formula that is linear in the size of the configurations and is thus of size The number of levels of the recursion is or Hence the size of the resulting formula is .