Existential equilibrium checking in a Boolean game (source code)

= Existential equilibrium checking in a Boolean game

Given a <Boolean game> and a query <propositional formula> $\phi$, decide whether some <pure strategy> <Nash equilibrium> satisfies $\phi$. The problem is complete for the existential <second level of the polynomial hierarchy>.

For membership, existentially choose a <Boolean valuation> and universally check every player's every <unilateral deviation>. The goal must remain false under all such deviations for each player whose goal is currently false. Each individual check takes <polynomial time>.

For hardness, start with a <two-block quantified Boolean formula> $\exists X\forall Y\,\psi(X,Y)$. Give player 1 control of $X$ and the constant true goal. Give player 2 control of $Y$ and goal $\neg\psi$, and use $\psi$ as the query. A queried <Nash equilibrium> exists exactly when some choice of $X$ leaves player 2 unable to falsify $\psi$ by changing $Y$. This is precisely the input quantified statement, and the construction is a <polynomial-time reduction>.