Introduction

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: ∃x1x_{1} ∀x2x_{2} ∃x3x_{3} … Now the formula no longer asks "can it be satisfied?" but something richer: "can I pick x1x_{1} so that for every x2x_{2} there is an x3x_{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.

Play the Formula

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">The prefix <b>∃a ∀b ∃c</b> sets the turn order. <b>You</b> pick a (∃), the <b>opponent</b> picks b (∀), then <b>you</b> pick c (∃). The formula <b>φ = (¬a ∨ ¬c) ∧ (b ∨ ¬c) ∧ (¬b ∨ c)</b> at each leaf decides the winner — true means you win. The QBF is true iff you have a winning strategy.</p>
<div class="prefix" id="prefix"></div>
<div class="tree" id="tree"></div>
<div class="status" id="status">Pick a value for a to start playing.</div>
<div class="btns">
  <button id="solve" type="button">Solve (minimax)</button>
  <button id="reset" type="button" class="ghost">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; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// QBF: ∃a ∀b ∃c . φ(a,b,c), with
//   φ = (¬a ∨ ¬c) ∧ (b ∨ ¬c) ∧ (¬b ∨ c)
// The formula is TRUE (you have a winning strategy) iff:
//   OR over a ( AND over b ( OR over c ( φ ) ) )
// because ∃ = OR (your move, you pick the best) and ∀ = AND (opponent move,
// it must hold for every choice). Depth-first evaluation keeps only the
// current a,b,c on the stack -> polynomial space, even with 2^n leaves.
// Here the QBF is TRUE: play a = F, then answer b with c = b. (a = T loses.)
function phi(a,b,c){ return (!a||!c) && (b||!c) && (!b||c); }

// Player's partial choices: null until chosen.
let pick = { a: null, b: null, c: null };

function render(){
  const tree = document.getElementById('tree'); tree.innerHTML = '';
  document.getElementById('prefix').textContent =
    '∃a  ∀b  ∃c .  φ = (¬a ∨ ¬c) ∧ (b ∨ ¬c) ∧ (¬b ∨ c)';
  addLevel('you', '∃ a  (you)',   'a', pick.a, true);
  addLevel('opp', '∀ b  (opp)',   'b', pick.b, pick.a !== null);
  addLevel('you', '∃ c  (you)',   'c', pick.c, pick.b !== null);
  const leaf = document.createElement('div');
  leaf.className = 'level';
  const tag = document.createElement('span'); tag.className = 'tag'; tag.textContent = 'φ =';
  leaf.appendChild(tag);
  if (pick.a !== null && pick.b !== null && pick.c !== null){
    const v = phi(pick.a, pick.b, pick.c);
    const lf = document.createElement('span');
    lf.className = 'leaf ' + (v ? 'win' : 'lose');
    lf.textContent = v ? 'TRUE  → you win this leaf' : 'FALSE → you lose this leaf';
    leaf.appendChild(lf);
  } else {
    const lf = document.createElement('span'); lf.className = 'leaf'; lf.textContent = '?';
    leaf.appendChild(lf);
  }
  tree.appendChild(leaf);
}

function addLevel(side, label, key, chosen, active){
  const tree = document.getElementById('tree');
  const row = document.createElement('div'); row.className = 'level';
  const tag = document.createElement('span'); tag.className = 'tag ' + side; tag.textContent = label;
  row.appendChild(tag);
  [false, true].forEach(val => {
    const o = document.createElement('div');
    o.className = 'opt ' + side + (chosen === val ? ' sel' : '') + (active ? '' : ' dim');
    o.textContent = key + ' = ' + (val ? 'T' : 'F');
    o.addEventListener('click', () => {
      pick[key] = val;
      if (key === 'a') { pick.b = null; pick.c = null; }
      if (key === 'b') { pick.c = null; }
      render(); judge();
    });
    row.appendChild(o);
  });
  tree.appendChild(row);
}

function setStatus(t, cls){ const s = document.getElementById('status'); s.textContent = t; s.className = 'status ' + cls; }

function judge(){
  if (pick.a === null) { setStatus('Pick a value for a to start playing.', ''); return; }
  if (pick.b === null) { setStatus('Opponent (∀) now picks b — and must lose for EVERY b.', ''); return; }
  if (pick.c === null) { setStatus('Now pick c (∃) to try to make φ true.', ''); return; }
  const v = phi(pick.a, pick.b, pick.c);
  setStatus(v ? '✓ This leaf is TRUE — you survived this line.'
              : '✗ This leaf is FALSE — this line loses. Try another c.', v ? 'ok' : 'bad');
}

// Full minimax: ∃ = OR, ∀ = AND. Returns boolean truth of the QBF.
function solve(){
  let leaves = 0;
  const existsA = [false,true].some(a =>      // ∃a
    [false,true].every(b =>                   // ∀b
      [false,true].some(c => { leaves++; return phi(a,b,c); })  // ∃c
    )
  );
  // Find a winning 'a' to display, if any.
  let winA = null;
  for (const a of [false,true]) {
    const ok = [false,true].every(b => [false,true].some(c => phi(a,b,c)));
    if (ok) { winA = a; break; }
  }
  if (existsA) {
    setStatus(fmt('QBF is TRUE. Winning first move: a = %v%. Evaluated %leaves% leaves (≤ 2³ = 8).', { v: winA?'T':'F', leaves: leaves }), 'ok');
    console.log('QBF true; winning a =', winA, '| leaves checked =', leaves);
  } else {
    setStatus(fmt('QBF is FALSE. No first move wins against every b. Leaves: %leaves%.', { leaves: leaves }), 'bad');
    console.log('QBF false | leaves checked =', leaves);
  }
}

document.getElementById('solve').addEventListener('click', solve);
document.getElementById('reset').addEventListener('click', () => {
  pick = { a: null, b: null, c: null }; render(); judge();
});
render(); judge();
Result
Console

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.

The Real Complexity

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 2n2^{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.

Where It Matters

"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.

Conclusion

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.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/qbf-pspace/Content licensed under CC BY-NC 4.0.