Quantified Boolean formula

A quantified Boolean formula (QBF) is a Boolean formula augmented with universal and existential quantifiers over its variables. Where SAT asks whether there exists an assignment that makes a formula true, QBF asks whether there exists an assignment of the existentially quantified variables such that for all assignments of the universally quantified variables, the formula holds. QBF is the canonical PSPACE-complete problem, capturing the complexity of adversarial reasoning, game solving, and planning under incomplete information.

The computational jump from SAT to QBF is dramatic. While SAT asks about existence, QBF asks about strategic interaction — about whether one player can force a win regardless of the opponent's moves. Modern QBF solvers extend the conflict-driven clause learning paradigm of SAT solvers with quantifier-aware reasoning, though the additional complexity means that QBF solvers handle thousands of variables where SAT solvers handle millions.

QBF is where satisfiability stops being a logic problem and becomes a game theory problem. The quantifier alternation introduces adversarial structure that Boolean logic alone cannot express. Any system that must reason about an opponent — a security protocol, a market mechanism, a predator-prey interaction — is doing QBF under the hood, whether it knows it or not.