P37 · TQBF₃

🔊 Listen

1 · TQBF₃ · the standardised PSPACE-complete form

TQBF₃ is the restriction of TQBF to QBFs in prenex form with alternating quantifiers and a 3-CNF matrix:

Normal form

∃x₁ ∀x₂ ∃x₃ ∀x₄ … Q x_n. φ(x₁, …, x_n)

where φ is 3-CNF and quantifiers strictly alternate ∃∀∃∀….

The normalisation has two steps, each polynomial.

Step 1 · Enforce alternation by padding

If two same-flavor quantifiers appear consecutively, e.g. ∃x ∃y, insert a dummy: ∃x ∀d ∃y, where d doesn't appear in the matrix. Since the matrix doesn't mention d, the value of d is irrelevant — the dummy quantifier is a no-op semantically but creates the alternation pattern.

Step 2 · Convert matrix to 3-CNF

Apply the SAT → 3SAT splitting rule (Problem 26) to the propositional kernel. The auxiliary variables introduced by splitting are existentially quantified at the innermost layer (or handled with dummy padding to maintain alternation).

TQBF₃ remains PSPACE-complete. The restriction matters for reductions: many PSPACE-completeness proofs target this specific form, including the famous reduction to generalised geography (Problem 39).

🔊 Listen

2 · Animated demo · auto-plays · loops

🔊 Listen

3 · Pitfalls

Prenex form means all quantifiers at the front. ∃x. (P(x) ∧ ∀y. Q(x,y)) is not prenex. To move ∀y outside, use scope rules: ∃x ∀y. (P(x) ∧ Q(x,y)).
Dummy quantifiers don't change the formula's truth. They're padding for alternation, not part of the semantic content.
3-CNF means the matrix only. The quantifier prefix is independent of the matrix's CNF structure.

🔊 Listen

4 · Q&A defence notes

Q1. How to enforce strict alternation?
Insert dummy variables that don't appear in the matrix. Two consecutive ∃ become ∃x ∀d ∃y, where d is fresh. Since d doesn't constrain anything, the dummy quantifier has no semantic effect.
Q2. How to convert matrix to 3-CNF?
Apply the SAT → 3SAT splitting rule from Problem 26. Wide clauses split with auxiliary variables; those auxiliaries become innermost existential. Linear blowup in matrix size.
Q3. What's the total size blowup?
Polynomial. Quantifier alternation adds at most n dummies. 3-CNF conversion adds at most O(|matrix|) auxiliary variables and clauses. Both linear.
Q4. Is the normal form used in proofs?
Yes — the famous TQBF → GEOGRAPHY reduction (Sipser §8.3) starts from a TQBF₃ instance. The strict alternation enables the game-tree-to-graph encoding.

🔊 Listen

5 · Where to read more

Sipser: §8.3 (TQBF reductions). Lecture notes: Module 6 slide 3. Companion problems: P26 (SAT → 3SAT), P36 (TQBF game tree), P39 (TQBF → geography).