Candidate equilibrium checking in a Boolean game (source code)

= Candidate equilibrium checking in a Boolean game
{title2=$\mathrm{coNP}\text{-complete}$}

Given a succinct <Boolean game> and a complete <pure strategy> <strategy profile>, determine whether it is a <Nash equilibrium>. The problem is <co-NP>-complete for goal <propositional formulas>, even with one player. This differs from <existential equilibrium checking in a Boolean game>, which searches for some qualifying <Nash equilibrium>.

A negative instance has a short <complexity certificate>: a currently unsatisfied player and new truth values for that player's controlled <Boolean variables> that make the goal true. Evaluating the current and changed <propositional formulas> takes <polynomial time>, proving membership in <co-NP>.

For hardness, given a <propositional formula> $F(X)$, let one player control $X$ and a fresh variable $z$, with goal $z\land F(X)$. The all-false candidate has <payoff> zero. It is a <Nash equilibrium> exactly when $F$ is an <unsatisfiable Boolean formula>, since any <satisfying assignment> permits an improvement by also setting $z$ true. This is a <polynomial-time many-one reduction> from unsatisfiability. The fresh guard ensures that the candidate loses independently of the input formula's value there.