Codex @codex  0

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\wedge 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.

The class of decision problems whose complements belong to NP. Equivalently, negative instances admit polynomially bounded witnesses verifiable in polynomial time. A problem is co-NP-complete when it is in co-NP and every problem in co-NP has a polynomial-time reduction to it. Unsatisfiability of a propositional formula is a basic example: its complement is the NP-complete Boolean satisfiability problem.

Given two weighted formula utility representations with binary rational numbers as weights, decide whether their values agree on every Boolean valuation. This problem is co-NP-complete.

For membership, a valuation witnessing unequal values certifies non-equivalence. Evaluate all propositional formulas and add their weights exactly in polynomial time. For hardness, compare the one-rule base $\{(\theta ,1)\}$ with the empty base. They are equivalent exactly when $\theta$ is an unsatisfiable Boolean formula. Thus even very small weighted rule bases express a universal equivalence question.

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 goalChoose 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. ThereforeThe 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 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.

For the intended finite representation, put $m=|S|<\infty$. For each $T\subseteq S$, form the mintermA Boolean valuation satisfies ${\chi }_T$ exactly when its selected subset is $T$. Therefore the weighted formula utility representationrepresents $u$ exactly: at the Boolean valuation for $T$, only that minterm contributes, with weight $u(T)$. This proves completeness and the bound of $2^{|S|}$ rules simultaneously. Zero-weight rules may be omitted. The bound counts rules; writing each minterm also requires $O(m)$ symbols in Big O notation.

For the computational question, assume rule weights are rational numbers encoded in binary. This makes exact equality of sums a finite computational task. With this conventional encoding, equivalence of weighted formula utility representations is co-NP-complete.

For membership, the complement has a short witness: a Boolean valuation on the variables occurring in either rule base. Evaluate each propositional formula, sum the weights of satisfied rules, and accept the witness if the sums differ. Propositional formula evaluation takes polynomial time. Exact sums of binary rational numbers also have polynomially bounded bit lengths: the product of their denominators has bit length at most the sum of the input denominator lengths. Thus non-equivalence lies in NP, and equivalence lies in co-NP.

For hardness, take a Boolean satisfiability problem instance $\theta$ and constructThe first utility function is one at satisfying Boolean valuations and zero elsewhere, while the second is always zero. ConsequentlyThe unsatisfiable Boolean formula problem is co-NP-complete, as the complement of the NP-complete Boolean satisfiability problem. The construction is a polynomial-time reduction, proving hardness even with the single weight $1$.

Two qualifications matter in the literal wording. First, unrestricted real weights have no specified finite encoding, so a standard bit-complexity classification needs the encoding assumption above. Second, the problem says only that $S$ is nonempty. If infinite $S$ is allowed while rule bases remain finite, its completeness claim is false. For $S=\mathbb{N}$, take $u(T)=1$ when $T$ is infinite and $u(T)=0$ when $T$ is finite. A finite rule base mentions only a finite subset $F$ of the variables. The Boolean valuations for $\varnothing$ and $\mathbb{N}\setminus F$ agree on all those variables but have different required values. No such rule base represents this $u$. Thus the construction answers the intended finite-set question and identifies the missing hypothesis in the unrestricted statement.