the quantified boolean formula problem

SAT, the boolean satisfiability problem, asks a single existential question: is there some assignment of true/false to the variables that makes the formula true? TQBF turns the volume all the way up by allowing both 'there exists' and 'for all' quantifiers, layered in any order. It is like the difference between 'is there a move that works?' and the full strategic question 'is there a move such that for every reply there is a move such that ...?'. That alternation of exists and for-all is what makes TQBF the prototypical hard space problem.

Formally, a quantified boolean formula is a sentence like Q1 x1 Q2 x2 ... Qk xk . phi, where each Qi is either there-exists or for-all and phi is an ordinary boolean formula over the variables x1...xk. TQBF is the language of all such sentences that are TRUE. You evaluate it recursively: 'there exists x . psi' is true if psi holds for x=true OR x=false; 'for all x . psi' is true if psi holds for x=true AND x=false. This recursion can be carried out reusing memory: peel off the outermost quantifier, recurse on each value, and reuse the same work space for each branch, so the whole evaluation runs in polynomial space.

TQBF is the canonical PSPACE-complete problem; it is to PSPACE what SAT is to NP. The reason it captures all of PSPACE is that a polynomial-space computation's accept/reject can be encoded as exactly this kind of alternating-quantifier reachability statement (using the Savitch midpoint trick to keep the formula polynomial). SAT is just TQBF with only existential quantifiers, which is why SAT is in NP while TQBF reaches up to PSPACE. Caveat: if you cap the number of quantifier alternations at a fixed constant, you do NOT get all of PSPACE; you climb the polynomial hierarchy instead. It is the UNBOUNDED alternation that gives TQBF its full PSPACE power.