True Quantified Boolean Formula

A True Quantified Boolean Formula (TQBF) is a logical expression built from Boolean variables bound by universal (∀) and existential (∃) quantifiers that evaluates to true under all valid interpretations of those quantifiers. Unlike standard Boolean satisfiability (SAT), which only asks whether some assignment of variables makes a formula true, TQBF interleaves quantifiers — asking, for example, whether for every choice of one set of variables there exists a choice of another set that satisfies the formula. This richer structure makes TQBF strictly harder than SAT and places it at the canonical complete problem for the complexity class PSPACE.

The decision procedure for TQBF works by recursively evaluating the formula from the innermost quantifier outward. For an existentially quantified variable, the algorithm checks whether setting it to true or false yields a satisfiable subformula; for a universally quantified variable, both assignments must succeed. This recursive evaluation requires only polynomial space, since each level of recursion reuses memory, but it may require exponential time in the worst case. The PSPACE-completeness of TQBF means that any problem solvable in polynomial space can be reduced to it, making it a theoretical benchmark for the hardest tractable problems in formal reasoning.

In AI and machine learning, TQBF serves as a foundational model for problems involving adversarial or multi-agent reasoning. Two-player games with perfect information — such as chess or Go — can be encoded as TQBF instances, where existential quantifiers represent one player's moves and universal quantifiers represent the opponent's. This connection motivates minimax search and alpha-beta pruning algorithms used in game-playing AI. TQBF also underpins automated planning under uncertainty, model checking in formal verification, and the analysis of reactive systems where a controller must respond correctly to all possible environments.

For machine learning researchers, TQBF provides a complexity-theoretic lens for understanding the limits of learned models in strategic or adversarial settings. Robustness verification of neural networks — asking whether any adversarial perturbation can fool a classifier — shares structural similarities with TQBF, connecting deep learning safety research to classical complexity theory.