patternMinor
TQBF as interactive game
Viewed 0 times
gametqbfinteractive
Problem
My teacher describes true quantified boolean formula (TQBF) as an interactive game between two players $\exists$ and $\forall$, and asks us to show a winning strategy for the existential player $\exists$. Can someone describe what this game is? I feel like this is background knowledge I am missing.
Solution
Hint: Imagine the formula in some (prenex) normal form and consider the order of quantifiers: $\exists x_1 \forall x_2 \exists x_3 \exists x_4 \dots Q x_t \phi(\overline{x})$. Let the player corresponding to the first quantifier choose its valuation (true or false) and then continue the game with that variable $x \mapsto v$ where $v$ is the value chosen for $x$, and with the first quantifier removed from the formula, i.e., in the example, if $\exists$ chooses true, let $x_1 \mapsto \mathtt{true}$ and continue the game on $\forall x_2 \exists x_3 \exists x_4 \dots Q x_t \phi(\overline{x'})$.
Let $\exists$ be the winner (as usual) if and only if the end result is a quantifier-free true formula.
Let $\exists$ be the winner (as usual) if and only if the end result is a quantifier-free true formula.
Context
StackExchange Computer Science Q#11225, answer score: 4
Revisions (0)
No revisions yet.