Math 2.0

Computer science Computational complexity: resources and classes Problem

True quantified Boolean formula

Builds on Decision problemSatisfiability

Problem

Let n≥1n \ge 1. A fully quantified Boolean formula has the form Q1x1 Q2x2⋯Qnxn  φ(x1,…,xn).Q_1 x_1 \, Q_2 x_2 \cdots Q_n x_n \; \varphi(x_1, \ldots, x_n). Here each QiQ_i is ∃\exists or ∀\forall, and the variables xix_i range over {0,1}\set{0, 1}. The body φ\varphi is a propositional formula in the variables x1,…,xnx_1, \ldots, x_n. Such a formula has no free variables, so it is either true or false. The decision problem TQBF asks, given a fully quantified Boolean formula, whether it is true.

Remarks

Larry Stockmeyer and Albert Meyer showed in 1973 that TQBF is complete for PSPACE under polynomial-time many-one reductions. It is in PSPACE because a recursive evaluation needs to store only one value per quantifier at a time, so it uses space polynomial in the length of the formula. When all quantifiers are ∃\exists, the problem is the satisfiability problem for φ\varphi, which is NP-complete. When the quantifier prefix has at most kk blocks and starts with ∃\exists, the restricted problem is complete for the level Σkp\Sigma_k^p of the polynomial hierarchy. TQBF can be seen as a game: one player chooses the existential variables and the other the universal ones. The formula is true when the first player has a winning strategy.

Reading path

To understand this page from the ground up, read these 3 pages in order. The foundations come first.

Show the path as a graph
Decision problem, concept, no evidence levelDecision problemconceptSatisfiability, concept, no evidence levelSatisfiabilityconceptTrue quantified Boolean formula, problem, no evidence levelTrue quantified Boole…problem
Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.
  • no evidence level
  1. Decision problem concept
  2. Satisfiability concept
  3. True quantified Boolean formula problem

Where this leads

1 page builds on this one.

Further reading

  1. Web https://en.wikipedia.org/wiki/True_quantified_Boolean_formula
About this page
TagWV2N01B4YV
URIm2://WV2N01B4YV
Kindproblem
WritingW0 stub
MSC68Q17, 68Q15, 03B70
StatusThis copy of the site has no build data. Run m2 status WV2N01B4YV.
AboutPSPACE
UsesDecision problem, Satisfiability
Same as
Changed3 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • an inventory row: the row of the inventory that the node accounts for (0 of 1)
  • a source with a locator (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

Used by