P39 · TQBF → Geography

🔊 Listen

1 · TQBF → Generalised Geography · the reduction

Sipser §8.3, Theorem 8.11: TQBF ≤_p GG. Given a TQBF₃ instance, build a graph G whose Geography game has Player 1 winning iff the QBF is true.

Three gadget types

Variable gadgets (one per x_i): a small diamond with two outgoing branches labeled "x_i = T" and "x_i = F." For ∃-quantified x_i, the token arrives at a player-1-controlled node; for ∀-quantified x_i, at a player-2-controlled node. The current mover picks the branch — encoding that player's choice of truth value.

Sequencing: after the x_n variable gadget, the path leads to the clause-selection node.

Clause selection (player 2's last move): player 2 chooses a clause C and forces the token there. Inside C's sub-gadget, player 1 chooses a literal; the literal connects to the previously-chosen-true side of its variable gadget. If that literal is false under the chosen assignment, the connection leads to an already-visited vertex — player 1 has no move and loses. If true, player 1 escapes and the game continues to player 1's win.

So Player 1 wins ⇔ for every clause player 2 could pick, there's a true literal player 1 can use ⇔ every clause has a true literal under the QBF assignment ⇔ the QBF is true.

Graph size: O(n) for variable gadgets, O(m) for clauses, O(nm) for literal-to-variable connections. Polynomial.

🔊 Listen

2 · Animated demo · auto-plays · loops

🔊 Listen

3 · Pitfalls

The QBF must be in alternating prenex form (TQBF₃). Strict ∃∀∃∀ alternation aligns with the game's turn structure. Use Problem 37's normalisation first.
"No vertex repeats" is what makes the literal-to-variable connection trap player 1. If the literal is false, the connection target was already visited at the variable gadget — player 1 can't reuse it.
The reduction is poly-time, not the game itself. Building the graph is poly. Playing the game optimally is still PSPACE-hard.

🔊 Listen

4 · Q&A defence notes

Q1. Why is the move-direction tied to the quantifier?
At ∃-quantified variable gadgets, player 1 is to move — encoding "∃-player picks the value." At ∀-quantified gadgets, player 2 moves — encoding "∀-player picks." The strict ∃∀∃∀ alternation in TQBF₃ ensures players alternate moves naturally.
Q2. How does the propositional matrix get encoded?
After all variable choices, player 2 picks a clause. Inside the clause gadget, player 1 picks a literal. The literal's outgoing edge connects to the variable's earlier-chosen-true vertex. If the literal is false (the variable's other value was chosen), that vertex is already visited — player 1 has no move and loses. So player 1 needs every player-2-chosen clause to contain a true literal.
Q3. Size of the reduction?
O(n) nodes for variable gadgets, O(m) for clause selection, O(nm) for literal-to-variable edges. Total O(nm) — polynomial in formula size.

🔊 Listen

5 · Where to read more

Sipser: Theorem 8.11, Figure 8.13. Lecture notes: Module 6 slide 3. Companion problems: P36 (TQBF), P38 (geography), P40 (chess hardness).