Definition. Decision problem A is PSPACE-complete if both of the following are true.
A ∈ PSPACE.
For every X ∈ PSPACE, X ≤p A.
A quantified boolean formula is a clausal formula where all of the variables are explicitly quantified, using either ∀ or ∃.
For example, ∀x∃y(x ∨ ¬y) is true if for every value of x (either true or false) there is a value of y (also true or false) so that formula (x ∨ ¬y) is true. That is correct. If x is true, choose any y. If x is false, choose y = false.
Compare the following two quantified boolean formulas.
∀x∃y((x ∨ y) ∧ (¬x ∨ ¬y))
∃y∀x((x ∨ y) ∧ (¬x ∨ ¬y))
Formula (1) is true. If x = true, choose y = false. If x = false, choose y = true.
Formula (2) is false. It says that you can select one value of y so that (x ∨ y) ∧ (¬x ∨ ¬y) is true for that y and every x. But there is no such y.
TQBF is the following problem.
Input. A quantified boolean formula φ
Question. Is φ true?
Notice that SAT is a special case of TQBF where all quantifiers must be ∃. But TQBF is much tougher than SAT.
Theorem. TQBF is PSPACE-complete.
The proof has two parts: (1) show that TQBF ∈ PSPACE and (2) for every problem X ∈ PSPACE, X ≤p TQBF. Part (1) is shown below. Part (2) is by a generic reduction that is too long to duplicate here.
The practical import of PSPACE-completeness is that TQBF is very time-consuming to solve for smaller lengths than SAT.
To see if quantified boolean formula φ is true, just run tqbf(φ, {}), where the set parameter gives a list of variable bindings.
tqbf(φ, bindings)
if φ has the form ∃x(φ′), then
if tqbf(φ′, bindings ∪ {x = false}) or
tqbf(φ′, bindings ∪ {x = true}) then
answer true
else
answer false
end if
else if φ has the form ∀x(φ′), then
if tqbf(φ′, bindings ∪ {x = false}) and
tqbf(φ′, bindings ∪ {x = true}) then
answer true
else
answer false
end if
else
evaluate φ using the variable
values given in bindings.
If φ is true
answer true
else
answer false
end if
Suppose that φ has length n. Then φ has fewer than n quantifiers. Computing tqbf(φ, {}) requires recursion to a depth of less than n.
Each frame only needs to store a small amount of information, namely where it is in the program.
So the total amount of space is O(n).
If NP = PSPACE, then for every true quantified boolean formula φ, there must be some short, easy to check evidence that φ is true.
What would that evidence look like?
It is partly the apparent lack of such evidence that leads people to conjecture that NP ≠ PSPACE.