QBF and PSPACE

Ordinary SAT asks a single question: does there exist an assignment of true/false to the variables that makes a Boolean formula true? That hidden word — there exists — is one quantifier, ∃.

Quantified Boolean Formulas (QBF) add the other quantifier, for all (∀), and let them alternate: ∃$x_{1}$ ∀$x_{2}$ ∃$x_{3}$ … Now the formula no longer asks "can it be satisfied?" but something richer: "can I pick $x_{1}$ so that for every $x_{2}$ there is an $x_{3}$ so that …?"

Read it out loud and you hear a game. Every ∃ is a move you make, trying to win; every ∀ is a move your opponent makes, trying to stop you. The formula is true exactly when you have a winning strategy. That single shift — from "find an assignment" to "win against all replies" — is the jump from NP up to PSPACE.

Here is a small quantified formula. The quantifier prefix ∃a ∀b ∃c sets the turn order: you choose a, then the opponent chooses b, then you choose c. The formula at the bottom decides the winner — if it ends up true, you win that leaf.

<p class="hint">{{hint}}</p>
<div class="prefix" id="prefix"></div>
<div class="tree" id="tree"></div>
<div class="status" id="status">{{status_start}}</div>
<div class="btns">
  <button id="solve" type="button">{{btn_solve}}</button>
  <button id="reset" type="button" class="ghost">{{btn_reset}}</button>
</div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .9rem; color: #444; margin: 0 0 .7rem; line-height: 1.45; }
.prefix { font: 700 15px ui-monospace, monospace; color: #1d3557; margin: .2rem 0 .6rem; }
.tree { display: flex; flex-direction: column; gap: .55rem; margin: .3rem 0; }
.level { display: flex; align-items: center; gap: .5rem; flex-wrap: wrap; }
.tag { font: 700 13px ui-monospace, monospace; width: 86px; flex: 0 0 86px; }
.tag.you { color: #0a7d33; }
.tag.opp { color: #c92f3c; }
.opt { font: 700 14px system-ui, sans-serif; padding: .35rem .8rem; border-radius: 8px;
       border: 1px solid #adb1b8; background: #eef1f4; cursor: pointer; user-select: none; }
.opt:hover { background: #e2e6eb; }
.opt.sel.you { background: #0a7d33; color: #fff; border-color: #086628; }
.opt.sel.opp { background: #c92f3c; color: #fff; border-color: #a8222e; }
.opt.dim { opacity: .4; pointer-events: none; }
.leaf { font: 700 15px ui-monospace, monospace; padding: .35rem .8rem; border-radius: 8px;
        border: 1px solid #cdd9e3; background: #e8eef3; color: #1d3557; }
.leaf.win { background: #0a7d33; color: #fff; border-color: #086628; }
.leaf.lose { background: #c92f3c; color: #fff; border-color: #a8222e; }
.status { font-size: 1rem; font-weight: 600; margin: .6rem 0; min-height: 1.4em; }
.status.ok { color: #0a7d33; }
.status.bad { color: #c92f3c; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; }
button { font: 600 14px system-ui, sans-serif; padding: .45rem .9rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }

// Code not found

Try to find a move for a such that whatever the opponent does with b, you can still answer with c to make the formula true. If such a move exists, the QBF is true and the tree lights up green. Press Solve (minimax) and the computer evaluates the whole tree the way the definition demands: OR over your moves, AND over the opponent's. Notice it never has to store more than one root-to-leaf path at a time — that is exactly why the problem lives in polynomial space even though the tree is exponentially wide.

How hard is QBF, really?

• SAT is the ∃-only case. Drop every ∀ and QBF collapses back to SAT, the canonical NP-complete problem. The ∀ quantifiers are what make it harder.
• Evaluating the tree is a recursive minimax: OR at ∃ levels, AND at ∀ levels. With n variables the tree has up to $2^{n}$ leaves — exponential time in the worst case.
• But only polynomial space. Depth-first recursion explores one branch at a time and keeps just the current path plus a counter, so it runs in PSPACE. That is the whole point.
• It is PSPACE-complete. In 1973 Larry Stockmeyer and Albert Meyer proved that deciding whether a QBF is true — written TQBF — is complete for PSPACE: every problem solvable in polynomial space reduces to it. It is to PSPACE what SAT is to NP.

So TQBF sits one level of difficulty above SAT. Whether that level is genuinely higher is the open P vs PSPACE question, a cousin of P vs NP: we know P ⊆ NP ⊆ PSPACE, but proving any of those containments strict has resisted every attempt.

"Can I act so that no matter what happens next, I still win?" is the shape of an enormous number of real problems, and QBF is their pure form:

• Two-player games: deciding the winner in generalized chess, Go, checkers and many puzzles is PSPACE-complete (or harder) for exactly this reason — your move, their move, your move.
• AI planning under uncertainty: a plan that must succeed against every adversarial or random response is an ∃/∀ alternation.
• Hardware and software verification: "for all inputs, does there exist a run that reaches a bad state?" is a quantified query that modern QBF solvers attack directly.
• Synthesis: building a controller that satisfies a spec against all environments is naturally a quantified formula.

Learn why QBF is hard and you have met the whole world of adversarial reasoning — the engine behind game-playing, SAT-based verification and robust planning.

QBF hides a beautiful idea in plain sight: a single quantifier separates searching from winning. With only ∃, you are hunting for one good assignment — that is SAT and NP. Add an alternating ∀ and the same formula becomes a two-player game, and deciding who wins is PSPACE-complete (Stockmeyer and Meyer, 1973).

So the next time you reason about a game, a plan, or a system that must hold up against every possible reply, remember that you are speaking the language of QBF. The whole zoo of games and planning collapses onto one tidy question — is this quantified formula true? — and that question is as hard as anything that fits in polynomial space. Whether it is truly harder than P vs NP allows is still, beautifully, unknown.