= Solution
The succinct input is the players' variable-control sets, their goal <propositional formulas>, and a complete candidate <Boolean valuation>; an exponentially expanded <payoff matrix> is not part of the input. This representation is essential to <candidate equilibrium checking in a Boolean game>.
For membership in <co-NP>, consider the complement: the candidate is not a <Nash equilibrium>. A <complexity certificate> consists of a player $i$ and an alternative <Boolean valuation> of that player's controlled <Boolean variables>. Evaluate the current goal and the goal after this <unilateral deviation>, keeping every other player's variables fixed. A profitable <unilateral deviation> exists precisely when the current goal is false and the new goal is true. The certificate has at most the number of input variables plus the player index, and both <propositional formula> evaluations take <polynomial time>. Thus the complement belongs to <NP>, and the original <decision problem> belongs to <co-NP>.
For hardness, start with a <propositional formula> $F(X)$ and introduce a fresh <Boolean variable> $z$. Construct a one-player <Boolean game> in which that player controls $X\cup\{z\}$ and has goal
$$
\gamma=z\land F(X).
$$
Choose the candidate <pure strategy> assigning every variable false. Its <payoff> is zero because $z$ is false, regardless of $F$. If $F$ has a <satisfying assignment>, changing $X$ to that assignment and $z$ to true is a profitable <unilateral deviation>. If $F$ is an <unsatisfiable Boolean formula>, no <unilateral deviation> can satisfy the goal. Therefore
$$
F\text{ is unsatisfiable}\quad\Longleftrightarrow\quad
\text{the constructed candidate is a Nash equilibrium}.
$$
The construction increases the formula length by only a constant and writes a candidate of linear length, so it is a <polynomial-time many-one reduction>. Unsatisfiability is <co-NP>-complete; combining hardness and membership proves that \b[candidate <Nash equilibrium> checking for <Boolean games> is <co-NP>-complete]. If a convention requires at least two players, add a player controlling a fresh unused variable and having the always-true goal; this changes neither direction of the proof.
Back to article page
