HiveBrain v1.2.0
Get Started
← Back to all entries
patternMinor

TQBF as interactive game

Submitted by: @import:stackexchange-cs··
0
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.

Context

StackExchange Computer Science Q#11225, answer score: 4

Revisions (0)

No revisions yet.