JOVANA
Explore Library Glossary Getting Started Three Levels Fields How it works Mission
Join the mission
All guides

PSPACE, Games, and Quantified Formulas

What happens when you stop budgeting time and start budgeting memory generously? You get PSPACE — the home of two-player games and fully quantified logic, where the real cost is not how long you think but how much you must remember at once.

From the time ladder to the space ladder

In the last two guides you swapped your measuring stick. Instead of counting clock ticks, you count the cells a Turing machine scribbles on. The trick that made this honest was the work-tape convention: the input sits on its own read-only tape that you do not charge for, and you only pay for the separate work tape you actually write on. That separation is what let L and NL mean something — a machine can read a huge input while keeping only a logarithmic scratch pad. Now we open the wallet wide and ask: what can you decide if you are allowed a work tape whose length is any polynomial in the input size?

That class is PSPACE: the set of problems decidable by a deterministic Turing machine using O(n^k) work-tape cells for some fixed k, where n is the input size. Notice what we have NOT bounded — the time. A machine with a polynomial amount of memory can run for an enormous while: it can visit up to roughly 2^(polynomial) distinct memory configurations before it must either repeat a configuration (and so loop) or halt. So PSPACE is generous about thinking time but strict about how much you may hold in mind at any single instant. That single shift in what is scarce turns out to capture a strikingly different flavour of problem.

Where PSPACE sits on the map

Let us pin PSPACE between the classes you already know. First, NP is inside PSPACE. A problem in NP has a short certificate you can check quickly; to decide it within polynomial space you simply loop over every candidate certificate one at a time, run the polynomial-time verifier, and reuse the same scratch space for each trial. You may try exponentially many certificates — that is fine, time is free here — but each trial needs only polynomial memory, so the whole search fits in PSPACE. By the same reasoning co-NP sits inside PSPACE too: just demand that ALL certificates fail instead of that one succeeds.

Going the other way, PSPACE is inside EXPTIME, the problems solvable in exponential TIME. The argument is the configuration count from a moment ago: a machine using polynomial space has only 2^(polynomial) possible configurations, and if it never repeats one it must halt within that many steps — which is an exponential time bound. Stacking everything we have gathered across this whole ladder gives one clean chain: L is in NL, NL is in P, P is in NP, NP is in PSPACE, and PSPACE is in EXPTIME. Each class is contained in the next; that part is solid theorem, not conjecture.

The signature problem: quantified boolean formulas

Every class has its emblematic hard problem. For NP it was satisfiability: does THERE EXIST an assignment making a Boolean formula true? That single existential question — 'is there a way?' — is exactly what a verifier checks against a guessed certificate. PSPACE's emblem turns the dial all the way up. A quantified boolean formula (QBF) lets you put BOTH kinds of quantifier in front of the variables, in any order: 'for ALL x, there EXISTS y, for all z, ...' followed by an ordinary Boolean formula. The question is whether the whole quantified sentence comes out true.

Why does adding the universal quantifier explode the difficulty so dramatically? Plain SAT only asks for existence, and a single lucky guess settles it. But 'for all x' forces you to confirm something for EVERY value of x — you cannot get lucky; you must, in effect, check both branches x = true and x = false and have both work out. And those alternate with 'there exists', which only needs one branch to work. To evaluate the formula you recurse: peel off the outermost quantifier, try both values of its variable, and inside each try peel off the next quantifier. The recursion tree is exponentially wide, but — and this is the PSPACE magic — you only ever walk ONE root-to-leaf path at a time, reusing the same stack frames as you back out. The depth of that recursion is just the number of variables, so the memory you hold is only polynomial.

QBF:   forall x.  exists y.   (x OR y)  AND  (NOT x OR NOT y)

Evaluate by recursion (one path live at a time, reuse the frame):

  x = FALSE :   exists y. (F OR y) AND (T OR ...)
                  y = TRUE  -> (F OR T)=T  AND (T)=T  -> TRUE   [y found]
  x = TRUE  :   exists y. (T OR y) AND (F OR NOT y)
                  y = FALSE -> (T) AND (F OR T)=T   -> TRUE     [y found]

  forall x needs BOTH x-branches true:  TRUE and TRUE  ->  whole QBF = TRUE

Depth of recursion = number of variables  ->  memory is polynomial.
Width of the tree   = 2^(variables)        ->  time is exponential.
Evaluating a QBF. The 'for all' node insists both children succeed; the 'there exists' node is happy with one. Only the current path is in memory, so the cost is the tree's DEPTH (polynomial), not its WIDTH (exponential).

QBF is the PSPACE counterpart of what SAT is to NP: it is PSPACE-complete. That means QBF is in PSPACE (the recursion above is the polynomial-space algorithm) AND every problem in PSPACE reduces to it in polynomial time. So QBF is among the hardest problems in PSPACE, and by being PSPACE-complete it plays the same anchoring role here that SAT plays for NP — a single hard problem the whole class can be translated into. Indeed plain SAT is exactly the special case of QBF where every quantifier happens to be 'there exists', which is a tidy way to see NP nestling inside PSPACE.

Why QBF is really a game

Here is the vivid way to feel what PSPACE-completeness means: a quantified formula is a TWO-PLAYER GAME written in logic. Read 'there exists y' as a move by a player we will call Prover, who is trying to make the formula true, and 'for all x' as a move by Adversary, who is trying to make it false. The quantifier order is the turn order. The sentence 'for all x, there exists y, ...' literally says: no matter what Adversary plays for x, Prover has a reply y, and so on down the line. The whole QBF is true exactly when Prover has a winning STRATEGY — a way to respond to every possible attack.

This is why so many real two-player board games are PSPACE-complete (or close to it) once you generalize them to an n-by-n board: generalized Geography, generalized Hex, and many others. 'Does the first player have a forced win from this position?' is exactly the alternating for-all / there-exists question QBF poses — I have a move (there exists) such that for all your replies (for all) I still have a move, and so on. Evaluating who wins means exploring the game tree, and the game tree is precisely the recursion tree we just drew, walked one path at a time with a polynomial-deep stack.

Be careful, though, with the slogan 'games are PSPACE-complete'. It holds for two-player games of PERFECT INFORMATION with a polynomially-bounded number of moves, generalized to arbitrary board size. Standard 8-by-8 chess and 19-by-19 Go are FINITE objects — a fixed board has only finitely many positions — so as stated they are not even meaningfully in a complexity class; complexity needs a growing input. The PSPACE results are about the n-by-n FAMILIES. And games whose plays can run exponentially long (some chess generalizations) can climb past PSPACE into EXPTIME — the clean PSPACE story needs the move count to stay polynomial.

Above NP: the polynomial hierarchy and a peek ahead

QBF also hands you a natural way to climb the gap between NP and PSPACE in graded steps. NP is the formulas with a single block of 'there exists' quantifiers; co-NP is a single block of 'for all'. What if you allow exactly two alternations — 'there exists ... for all ...'? Or three? Each fixed number of alternations defines a level, and the whole tower of levels is the polynomial hierarchy. Its first floor is NP and co-NP; higher floors allow more quantifier switches. QBF with UNBOUNDED alternations sits above the entire tower, which is why it captures all of PSPACE rather than any single floor.

A subtle point worth getting right: co-NP is NOT 'the problems not in NP'. The 'co' means complement — you swap yes and no. The classic NP problem is 'is this formula satisfiable?'; its co-NP twin is 'is this formula UNsatisfiable?', equivalently 'does it stay false for ALL assignments?'. Whether NP and co-NP are actually different classes is yet another famous OPEN question; we believe they differ (most experts doubt there are short certificates for unsatisfiability) but nobody has proved it. If NP turned out to equal co-NP, the whole polynomial hierarchy would collapse to its first floor.

One last surprise to set up the next guide. We defined PSPACE with a DETERMINISTIC machine. What if we let the machine be nondeterministic but still cap its space at a polynomial — call that NPSPACE? Astonishingly, Savitch's theorem proves PSPACE equals NPSPACE: for SPACE, nondeterminism buys you nothing more than a quadratic squeeze (any nondeterministic computation in space s can be simulated deterministically in space s-squared). That is wildly unlike the time world, where we suspect P is very far from NP. The next guide unpacks how Savitch's clever recursive halving of a reachability problem pulls this off — and a companion surprise, Immerman-Szelepcsenyi, showing that NL even equals its own complement co-NL.