True quantified Boolean formula
A true quantified Boolean formula is a quantified Boolean formula whose value is true under the standard semantics of Boolean quantification. The associated decision problem, conventionally abbreviated TQBF or QBF, asks whether a fully quantified Boolean formula is true. It is the canonical complete problem for the complexity class PSPACE, in much the same structural sense that the Boolean satisfiability problem is canonical for NP.
Quantification distinguishes TQBF from ordinary propositional satisfiability. A satisfiability instance asks whether there exists a single assignment making a formula true, whereas a quantified formula may contain alternating existential and universal choices. This alternation permits the formula to express computations in which later choices depend on earlier ones, while universal quantifiers require correctness under every assignment to the variables they bind.
Syntax and semantics
A quantified Boolean formula is formed from Boolean variables, logical connectives, and the quantifiers (\exists) and (\forall). A formula is closed when every variable occurrence is bound by a quantifier. TQBF is normally defined only for closed formulas, because such formulas have truth values independent of an external assignment.
Every quantified Boolean formula can be converted into prenex normal form,
[ Q_1x_1,Q_2x_2\cdots Q_nx_n;\varphi(x_1,\ldots,x_n), ]
where each (Q_i) is either (\exists) or (\forall), and the quantifier-free formula (\varphi) is called the matrix. Standard transformations can place the matrix in conjunctive normal form or disjunctive normal form, although such transformations do not in general preserve formula size unless auxiliary variables and carefully chosen quantifier placements are used.
The semantics are defined recursively. For a formula (\exists x,\psi), the value is true when at least one of (\psi[x:=0]) and (\psi[x:=1]) is true. For a formula (\forall x,\psi), the value is true only when both substitutions produce true formulas. Quantifier-free subformulas are evaluated by ordinary propositional logic.
For example,
[ \forall x;\exists y;((x\lor y)\land(\neg x\lor\neg y)) ]
is true. After either value of (x) has been fixed, a value of (y) can be selected that makes the matrix true. Reversing the quantifiers produces a different dependency structure:
[ \exists y;\forall x;((x\lor y)\land(\neg x\lor\neg y)). ]
This formula is false because the single existential choice for (y) must precede, and therefore cannot depend on, the universally quantified value of (x).
Game interpretation
The semantics admit an equivalent interpretation as a finite two-player game of perfect information. One player controls existentially quantified variables, while the other controls universally quantified variables. Variables are assigned in quantifier order, and the existential player wins exactly when the completed assignment satisfies the matrix.
Under this interpretation, a closed quantified formula is true precisely when the existential player has a winning strategy. A strategy is not merely a fixed assignment to the existential variables. Each existential choice may depend on the preceding universal choices, but it cannot depend on universal variables that occur later in the prefix. This restriction is the game-theoretic expression of quantifier scope.
The strategy associated with a true formula can require exponentially many branches when represented explicitly. TQBF nevertheless concerns only the existence of such a strategy, and its polynomial-space upper bound follows without constructing the entire strategy tree at once.
Computational complexity
TQBF belongs to PSPACE. A deterministic algorithm can evaluate the quantifier prefix recursively, retaining the current partial assignment and reusing its workspace after each branch has been evaluated. Although this computation may examine exponentially many assignments, its recursion depth and stored assignment require only polynomial space in the formula length.
The problem is also PSPACE-hard under polynomial-time many-one reduction. The standard proof encodes the computation of a polynomial-space Turing machine as a quantified formula. Because a polynomial-space machine may run for exponentially many steps, the reduction does not list its entire computation. Instead, it expresses reachability between machine configurations through a recursively defined predicate.
Let (\operatorname{Reach}(C,D,t)) assert that configuration (D) can be reached from configuration (C) within at most (2^t) transitions. A direct recursive expression introduces a midpoint configuration (M):
[ \operatorname{Reach}(C,D,t) \equiv \exists M, \bigl( \operatorname{Reach}(C,M,t-1) \land \operatorname{Reach}(M,D,t-1) \bigr). ]
Naively expanding both recursive occurrences would produce an exponentially large formula. Quantified auxiliary variables allow the two subproblems to share a single syntactic copy of the lower-level predicate. Universal selection then requires that this shared predicate hold for each half of the proposed path. Repeated application yields a polynomial-size quantified formula whose truth is equivalent to acceptance by the original machine.
Consequently,
[ \mathrm{TQBF}\in\mathrm{PSPACE} \quad\text{and}\quad \mathrm{TQBF}\text{ is PSPACE-hard}, ]
so TQBF is PSPACE-complete. The completeness result remains valid under several substantial syntactic restrictions, including common prenex forms with a suitably constrained matrix.
Historical development
The systematic complexity-theoretic treatment of quantified Boolean formulas developed during the early 1970s as polynomial space became established as a resource-bounded class. Larry Stockmeyer and Albert R. Meyer connected quantified formulas with computations requiring polynomially bounded storage and formulated reductions based on recursively compressed configuration reachability.
During the same period, You Watanabe analyzed quantifier alternation as a mechanism for representing dependent choices in polynomial-space computations. Watanabe's formulation used alternating existential and universal assignments to replace the explicit expansion of exponentially branching computation trees, giving an early form of the evaluation framework later standardized for TQBF.
The relation between quantifier alternation and machine alternation was subsequently placed in a general complexity-theoretic setting by Ashok Chandra, Dexter Kozen, and Larry Stockmeyer. Their characterization of alternating computation established that polynomial time on an alternating machine equals deterministic polynomial space:
[ \mathrm{AP}=\mathrm{PSPACE}. ]
Under this characterization, existential machine states correspond to existential quantifiers, while universal machine states correspond to universal quantifiers. TQBF therefore serves as a direct logical representation of polynomial-time alternating computation.
Restricted alternation
The number of transitions between existential and universal quantifiers determines a refined family of decision problems. When a prenex formula begins with an existential block and contains only a fixed number of alternating blocks, its truth problem lies at a corresponding level of the polynomial hierarchy. Formulas beginning with a universal block give the complementary levels.
An existentially quantified formula without universal quantifiers is equivalent to propositional satisfiability and is NP-complete. A universally quantified formula without existential quantifiers is equivalent to testing whether its matrix is a tautology, which is co-NP-complete. Allowing an unbounded number of alternations yields the full PSPACE-complete problem rather than a single fixed level of the polynomial hierarchy.
This distinction concerns alternation depth rather than merely the number of quantified variables. A formula may contain many variables while remaining in one existential block, whereas a shorter formula with repeated changes of quantifier type can express a more deeply nested dependency structure.
Representation and evaluation
The recursive semantics give rise to a search tree whose internal nodes correspond to quantified variables. An existential node evaluates to the disjunction of its children, while a universal node evaluates to their conjunction. The leaves contain evaluations of the quantifier-free matrix.
Practical QBF solver architectures avoid traversing this tree without simplification. Their underlying methods include quantified extensions of conflict-driven clause learning, symbolic elimination of variables, and expansions of selected quantifier blocks. These approaches preserve the same formal semantics while using structural properties of the matrix to avoid exploring branches whose values are already determined.
A true formula may also be represented by a certificate in the form of existential strategy functions. Each existential variable is expressed as a Boolean function of the universal variables that precede it. Such functions are often called Skolem functions, although their use in QBF is adapted to Boolean domains and to the dependency order imposed by the prefix. False formulas have dual certificates describing a winning universal strategy.