Quantified Boolean Formulas

Origin. Larry J. Stockmeyer and Albert R. Meyer, "Word Problems Requiring Exponential Time: Preliminary Report" (Proceedings of the 5th ACM Symposium on Theory of Computing, 1973, 1–9), proved the truth problem for quantified Boolean formulas PSPACE-complete; the encoding of a long computation by recursive halving follows the construction of Savitch's theorem (1970). Stockmeyer, "The Polynomial-Time Hierarchy" (Theoretical Computer Science 3, 1976, 1–22), fixed the bounded-alternation levels: with k alternating quantifier blocks beginning existentially, truth is Σᵖₖ-complete (Celia Wrathall, 1977, for CNF and DNF matrices). Q-resolution is from Hans Kleine Büning, Marek Karpinski and Andreas Flögel, "Resolution for Quantified Boolean Formulas" (Information and Computation 117, 1995, 12–18); the dependency-quantified extension descends from Gary L. Peterson and John H. Reif, "Multiple-Person Alternation" (FOCS 1979), completed in Peterson, Reif and Azhar (2001).

Models. Propositional logic with quantifiers over the propositions themselves: ∃p ranges over the two truth values, so a closed formula simply is true or false, and deciding which is the canonical PSPACE-complete problem. The semantics is a two-player game — the existential player assigns the ∃-variables and the universal player the ∀-variables, in prefix order, the existential player winning iff the matrix evaluates to true — and truth is the existence of a winning strategy, concretely a family of Skolem functions giving each existential variable as a function of the universal variables quantified before it. Alternation is the whole content: with no universal quantifiers the problem is SAT, each added alternation climbs one level of the polynomial hierarchy, and unbounded alternation is PSPACE. Propositional logic is the quantifier-free fragment; first-order logic is what results when the quantifiers range over a domain instead of over truth values.

Formalism.

Syntax: φ ::= p | ¬φ | φ ∧ ψ | φ ∨ ψ | ∃p.φ | ∀p.φ Quantifiers bind proposition letters; a closed formula has a truth value rather than models.

Semantics by expansion: ∃p.φ ≡ φ[⊤/p] ∨ φ[⊥/p] ∀p.φ ≡ φ[⊤/p] ∧ φ[⊥/p] Each expansion doubles the formula; n quantifiers give 2ⁿ propositional leaves.

Prenex CNF: Q₁p₁ … Qₙpₙ. ψ, ψ in conjunctive normal form — the solver input form.

Complexity: Truth: PSPACE-complete (Stockmeyer–Meyer 1973). Evaluation in linear space by recursion on the prefix. k blocks, outermost ∃: Σᵖₖ-complete; outermost ∀: Πᵖₖ-complete (Stockmeyer 1976; Wrathall 1977). ∃-only: SAT, NP-complete.

Q-resolution: Propositional resolution on existential pivots, plus universal reduction: delete a universal literal from a clause when every existential literal in the clause is quantified before it. Refutation-complete for false prenex CNF (Kleine Büning–Karpinski–Flögel 1995).

∀Exp+Res: Expand the universal variables, annotate the copies, refute by propositional resolution (Janota–Marques-Silva 2015). Simulates tree-shaped Q-resolution; does not simulate the unrestricted calculus.

Strategy extraction: From a Q-resolution refutation, a winning universal strategy — Herbrand functions — in linear time (Balabanov–Jiang 2012). Truth certifies by Skolem functions, falsity by Herbrand functions; the proof is the certificate.

QCDCL: Conflict-driven clause learning lifted to the quantified setting (Zhang–Malik 2002). Its learned clauses are long-distance Q-resolution derivations; solving and proof search coincide.

DQBF: Henkin prefixes: each existential variable names the universal variables it may depend on. NEXPTIME-complete (Peterson–Reif 1979; Peterson–Reif–Azhar 2001) — the level of the Bernays–Schönfinkel class, to which it translates by Skolemization. Exponentially more succinct than QBF on the problems both can state.

Symbols.

Metatheory. PSPACE-completeness (Stockmeyer–Meyer 1973) makes QBF truth the problem to which every polynomial-space computation reduces, and the correspondence is exact at every level below: k alternating blocks are Σᵖₖ- or Πᵖₖ-complete according to the outermost quantifier (Stockmeyer 1976; Wrathall 1977), so the polynomial hierarchy is readable off the prefix. Strategies are the analogue of models and they certify: substituting the Skolem functions of a true formula yields a propositional tautology, the Herbrand functions of a false one a contradiction, and Balabanov and Jiang (2012) extract these from Q-resolution refutations in linear time. Proof complexity separates the calculi: Q-resolution is refutation-complete (Kleine Büning–Karpinski–Flögel 1995), but the formulas introduced in the same paper require exponential-size Q-resolution refutations while admitting short long-distance ones, and ∀Exp+Res simulates tree Q-resolution but not the unrestricted calculus (Janota–Marques-Silva 2015). These lower bounds reach the solvers, since QCDCL traces long-distance Q-resolution (Zhang–Malik 2002) and expansion solvers trace ∀Exp+Res. Relaxing the linear prefix to Henkin dependency sets raises the complexity one exponential: DQBF is NEXPTIME-complete (Peterson–Reif 1979; Peterson–Reif–Azhar 2001), level with the Bernays–Schönfinkel class and connected through branching quantifiers to the team-semantic treatment of the same dependence pattern.

Applies to. Bounded model checking past the reach of SAT: the Savitch halving encodes an execution of exponential length in a polynomial-size QBF, where the SAT unrolling grows with the length. Two-player reachability and safety games, whose turn order is the quantifier prefix. Synthesis, through strategy extraction from proofs. Adversarial and conformant planning. Any problem at a fixed level of the polynomial hierarchy, as its canonical complete representative.

Limitations. Quantification is over truth values only — no individuals, no predicates, no domains — so a property of objects rather than of propositions needs a first-order fragment instead. PSPACE-completeness forecloses general-purpose efficiency, and the proof-complexity separations are solver facts: each calculus has formula families exponentially hard for it, so which solver family succeeds depends on the encoding. Prenexing and CNF conversion lose game structure: universal reduction sees only the linear prefix, so dependencies the original formula never had are imposed, which dependency schemes partially remove; DQBF removes them entirely and is NEXPTIME-complete. Certificates are functions rather than assignments: where SAT's witness is an assignment checked by one evaluation, a true QBF's witness is a strategy.

© 2026 Lingenic LLC