PSPACE — Quantified Boolean Formula: Visual walkthrough

We assume you know only what a Boolean value is: a wire that is either 0 (false) or 1 (true). Everything else is built below.

Step 1 — Two symbols, two players

WHAT. We meet the only two "quantifier" symbols we ever need. $\exists x$ is read "there exists a value of $x$ "; $\forall x$ is read "for all values of $x$ ". A variable can only be $0$ or $1$ , so "all values" means the two-element set ${0, 1}$ .

WHY these two and nothing else. Ordinary SAT only has the first one: "does some assignment work?" That is a single player hunting for one lucky choice. To model a contest, we need an opponent who is forced on us — a value we do not get to choose. $\forall$ is exactly that: whatever it picks, we must still win. So $\exists$ and $\forall$ are the minimal pair that turns a search into a two-player game.

PICTURE. Two boxes, one bit flowing out of each. The Prover's box has a happy "I only need one" tag; the Spoiler's has "I attack all of them".

Step 2 — A quantifier prefix is a sequence of moves

WHAT. Write the quantifiers in a row, then a plain Boolean formula $ϕ$ at the end: $Prover moves \exists x_{1} Spoiler moves \forall x_{2} Prover moves \exists x_{3} \dots ϕ (x_{1}, x_{2}, x_{3}, \dots)$ Term by term: $\exists x_{1}$ means Prover fixes $x_{1}$ first; $\forall x_{2}$ means Spoiler then fixes $x_{2}$ knowing $x_{1}$ ; $\exists x_{3}$ means Prover then fixes $x_{3}$ knowing both. $ϕ$ is the referee — after all bits are set, it outputs one truth value.

WHY read left-to-right as time. Order encodes information. A later player has already seen the earlier picks. This is why $\exists x \forall y$ and $\forall y \exists x$ differ (Step 8): who-moves-first decides who-can-react.

WHY no free variables. Every $x_{i}$ is claimed by some quantifier, so nothing is left dangling. With no inputs, the whole thing collapses to a single true/false — there is nothing to plug in.

PICTURE. A turn-order timeline: alternating Prover/Spoiler tokens placed left to right, an arrow labelled "time / information", and the referee $ϕ$ at the far right reading all the placed bits.

Step 3 — Unfold the moves into a game tree

WHAT. Each quantifier is a variable with two possible values, so it becomes a node with two children (the $0$ -branch and the $1$ -branch). Stacking the quantifiers stacks the levels. For $n$ variables we get a binary tree of depth $n$ with $2^{n}$ leaves; each leaf is one complete assignment, and $ϕ$ stamps it $0$ or $1$ .

WHY a tree and not a list. The Spoiler's choice branches the future: after $x_{1}$ there are two possible worlds for $x_{2}$ , and we must survive both. A list can't hold "both futures at once"; a tree can. The tree is the space of all plays.

PICTURE. A depth-3 tree: level-1 an $\exists$ -node (blue), level-2 two $\forall$ -nodes (orange), level-3 four $\exists$ -nodes, and eight leaves each carrying a $0$ / $1$ from $ϕ$ .

Step 4 — How each node combines its two children

WHAT. Give every node a value by folding its two children with one Boolean operation: $\exists -node = (left child) \lor (right child), \forall -node = (left child) \land (right child) .$ Symbol by symbol: $\lor$ (OR) is $1$ if at least one input is $1$ — that is the Prover, who needs only one good branch. $\land$ (AND) is $1$ only if both inputs are $1$ — that is the Spoiler, whom you must beat everywhere.

WHY OR for $\exists$ , AND for $\forall$ . Match the players' win-conditions from Step 1. "There exists a good child" is literally "child $_{0}$ OR child $_{1}$ ". "Good for all children" is literally "child $_{0}$ AND child $_{1}$ ". The logic connective is the quantifier, once the domain is ${0, 1}$ .

PICTURE. One $\exists$ -node showing $0 \lor 1 = 1$ next to one $\forall$ -node showing $1 \land 0 = 0$ , arrows pointing from children up into the parent with the operation labelled on the merge.

Step 5 — Walk a true formula: $\exists x \forall y (x \lor y)$

WHAT. Evaluate leaves first, then fold upward. The referee is $ϕ = x \lor y$ .

$x = 0$ subtree ( $\forall y$ ): leaf $y = 0 \to 0 \lor 0 = 0$ ; leaf $y = 1 \to 0 \lor 1 = 1$ . Fold with $\land$ : $0 \land 1 = 0$ .
$x = 1$ subtree ( $\forall y$ ): leaf $y = 0 \to 1$ ; leaf $y = 1 \to 1$ . Fold with $\land$ : $1 \land 1 = 1$ .
Root is $\exists x$ : fold with $\lor$ : $0 \lor 1 = 1$ . TRUE.

WHY it's true. The Prover ignores the losing $x = 0$ world and commits to $x = 1$ ; there the Spoiler is helpless because $x \lor y$ is already $1$ regardless of $y$ . One winning branch is all $\lor$ demands.

PICTURE. The depth-2 tree fully coloured: the $x = 0$ subtree glows red (value $0$ ), the $x = 1$ subtree green (value $1$ ), the root green with the winning $x = 1$ edge thick.

Step 6 — Walk a false formula: $\forall x \exists y (x \land y)$

WHAT. Referee $ϕ = x \land y$ .

$x = 0$ subtree ( $\exists y$ ): leaf $y = 0 \to 0 \land 0 = 0$ ; leaf $y = 1 \to 0 \land 1 = 0$ . Fold with $\lor$ : $0 \lor 0 = 0$ .
The root is $\forall x$ , an $\land$ . As soon as one child is $0$ , we can stop: $0 \land (anything) = 0$ . FALSE.

WHY we stop early. $\forall$ = AND, and AND dies on a single $0$ . The Spoiler already found the killer move $x = 0$ : no matter what $y$ the Prover then picks, $0 \land y = 0$ . We never even expand the $x = 1$ subtree — a first taste of not needing the whole tree in view.

PICTURE. Same tree; the $x = 0$ subtree evaluated to red $0$ , the root stamped red $0$ , and the entire $x = 1$ subtree drawn faded/greyed with a "not expanded — already lost" tag.

Step 7 — The key trick: reuse the same memory for both branches

WHAT. To fold a node we need two child values. But we don't need them simultaneously. Do the left branch fully; it returns a single bit; record that one bit; then erase the left branch's entire workspace and reuse it to compute the right branch; finally combine the two bits with $\lor$ or $\land$ .

Here $∣ ψ ∣$ denotes the ==length of the formula $ψ$ == — how many symbols it takes to write down (variables, quantifiers, connectives). One stack frame stores the current variable, its quantifier, and a pointer into $ϕ$ , all bounded by $∣ ψ ∣$ .

WHY this is the whole PSPACE result. The tree has $2^{n}$ leaves (Step 3) — that's the time. But memory only ever holds one root-to-current-node path plus a handful of returned bits. The path is length $n$ . So space grows one level at a time, not one leaf at a time: $S (n) = deepest active branch S (n - 1) + this level’s frame O (∣ ψ ∣), S (0) = O (∣ ψ ∣) \Rightarrow S (n) = O (n \cdot ∣ ψ ∣) .$ Term by term: $S (n)$ = space to evaluate a formula with $n$ quantifiers; $S (n - 1)$ is the space its child (one fewer quantifier) needs; we add just one stack frame $O (∣ ψ ∣)$ for the current variable; the recursion bottoms out at the referee $ϕ$ , also $O (∣ ψ ∣)$ . No factor of $2$ ever appears because the two subtrees share the same reused memory. Result: polynomial space, exponential time.

PICTURE. Left: the full $2^{n}$ tree faded, with a single bold path from root to a leaf highlighted (the "active memory"). A left subtree greyed with a small saved chip "bit = 1", the right subtree currently active. Caption: memory = one path, not one tree.

Step 8 — Degenerate & edge cases you must see

WHAT. Corner situations that could break intuition:

All $\exists$ (this is SAT). Every node is an $\lor$ ; the whole tree is one giant OR over $2^{n}$ leaves — "does some assignment satisfy $ϕ$ ?" Confirms $SAT \subseteq TQBF$ .
All $\forall$ . Every node is an $\land$ ; the tree is one giant AND — "is $ϕ$ a tautology?" (true on all inputs).
Order matters. Compare $\forall y \exists x (x \lor \neg y)$ with the swapped $\exists x \forall y (x \lor \neg y)$ , still over ${0, 1}$ . In $\forall y \exists x$ the Prover picks $x$ after seeing $y$ , so it can copy $y$ ( $x = y$ ) and win every time → TRUE. Swap to $\exists x \forall y$ : now $x$ is fixed first; the Spoiler then picks the worst $y$ . No single $x$ satisfies $x \lor \neg y$ for both $y = 0$ and $y = 1$ (try $x = 0$ : $y = 1$ gives $0 \lor 0 = 0$ ) → FALSE. The binary tree has the same branching shape both ways; only which player owns which level — i.e. the OR/AND labels on the nodes — flips, and that alone flips the verdict.
Empty prefix. No quantifiers, $ϕ$ constant. Depth-0 tree = a single leaf; $EVAL$ just reads $ϕ$ . Base case, cost $O (∣ ψ ∣)$ .

WHY include these. They show the machinery is complete: pure- $\exists$ , pure- $\forall$ , mixed-and-order-sensitive, and the zero-variable base all fall out of the same fold-the-tree rule with no special casing.

PICTURE. Four mini-trees side by side: (a) all-blue OR-tree "SAT", (b) all-orange AND-tree "tautology", (c) two identically-shaped trees with swapped OR/AND labels and opposite truth values, (d) a lone leaf "empty prefix".

The one-picture summary

WHAT. One diagram compresses the derivation: prefix → tree → fold with OR/AND → one reused path → verdict. Time is the $2^{n}$ leaf-fan; space is the thin $n$ -long spine.

Recall Feynman retelling — say it back in plain words

Two players take turns setting bits: the Prover ( $\exists$ ) who wants "true" and only needs one lucky line of play, and the Spoiler ( $\forall$ ) who wants "false" and must be beaten on every line. Line them up left to right — that order is time, so a later mover has seen the earlier bits. Unfold all possible plays into a binary tree: each Prover node is an OR (one good child suffices), each Spoiler node is an AND (all children must be good). Evaluate the leaves with the referee formula, then fold upward. The formula is true exactly when the Prover has a winning strategy — a green root. The tree has $2^{n}$ leaves, so brute time is exponential — but to fold any node you only need its two children one at a time: compute the left, keep just its one-bit answer, wipe the workspace, compute the right in the same memory, combine. Memory therefore only ever holds a single root-to-leaf path of length $n$ , giving $O (n \cdot ∣ ψ ∣)$ space. That single reused spine, riding under an exponential fan of leaves, is the whole reason $TQBF \in PSPACE$ .

Recall Self-test

$\exists$ folds children with which operation, and why? ::: OR — the Prover needs only one good branch. $\forall$ folds children with which operation, and why? ::: AND — the Spoiler must be beaten on every branch. Why is the space only $O (n \cdot ∣ ψ ∣)$ despite $2^{n}$ leaves? ::: The two subtrees are computed one after another in the same reused memory, so depth ( $n$ ), not leaf count, sets the space. Does swapping the outer two quantifiers change the tree's shape? ::: No — same binary shape; only the OR/AND labels on the levels flip, which can flip the verdict. In $\forall y \exists x (x \lor \neg y)$ over ${0, 1}$ , is it true or false, and the swap? ::: True (Prover sets $x = y$ after seeing $y$ ); the swap $\exists x \forall y$ is false.

Related: SAT and NP-completeness · Savitch's Theorem · PSPACE and Polynomial Space · Two-Player Games and Game Trees · NP vs PSPACE · Polynomial Hierarchy