Answer: \(\mathrm{coNP}\)-complete under polynomial-time many-one reductions; polynomial-time solvable iff \(\mathrm{P}=\mathrm{NP}\). NP-hard under polynomial-time Turing reductions, and many-one NP-hard iff \(\mathrm{NP}=\mathrm{coNP}\).
Theorem 3 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateIS-NASH is coNP-complete. Hardness holds even for n = 1 and d1 = 0. PROOF. (Membership) Consider a social environment G and a profile Π. The complementary problem is in NP: (a) Guess an agent i ∈[n] and an interpretation I ∈space(i); (b) Check that ui(Π) < ui(Π−i ∪{i 7→I}).
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite variable set \(V\), a goalbase \(G^0\), and an explicitly listed profile \((I,x_I)\) of Boolean interpretations \(I\in\{0,1\}^V\) with positive rational masses \(x_I\) summing to \(1\), decide whether every interpretation with positive mass maximizes \(G^0\)'s utility over all interpretations in \(\{0,1\}^V\).
Let \(V\) be a finite set of \(m\) Boolean variables. A goalbase \(G^0\) is a finite set of pairs \((\varphi,w)\), where \(\varphi\) is an explicitly encoded propositional formula over \(V\) and \(w\) is a signed binary rational. Define \(U(I)=\sum_{(\varphi,w)\in G^0:I\models\varphi}w\).
A society is given by its support: a nonempty list of \(\tau\) distinct interpretations \(I\in\{0,1\}^V\), each with positive binary rational mass \(x_I\), with \(\sum_I x_I=1\). Here \(\tau\) is the support size, not the number of possible interpretations. Let \(L\) be the total input bit length; state running times in \(m,\tau,L\).
The decision problem asks whether \(U(I)\ge U(J)\) for every listed \(I\) and every \(J\in\{0,1\}^V\); tied maximizers are permitted.
Is this decision problem solvable in polynomial time in \(m,\tau,L\), or is it NP-hard?
For finite societies, checking Nash stability is coNP-complete, even with one autonomous agent whose utility is given by a goalbase. Autonomous agents may choose any interpretation over their variables.
The problem is coNP-complete under polynomial-time many-one reductions, even when \(\tau=1\) and the goalbase contains a single formula of weight \(1\).
Consequently, it is polynomial-time solvable if and only if \(\mathrm{P}=\mathrm{NP}\). The distinction in the question matters: under many-one reductions, calling this problem NP-hard would be equivalent to asserting \(\mathrm{NP}=\mathrm{coNP}\). Under polynomial-time Turing reductions, it is NP-hard.
Write the goalbase weights as \(w_i=a_i/b_i\), with integers \(a_i\) and positive integers \(b_i\). Define
\[ D=\prod_i b_i, \qquad c_i=a_i(D/b_i). \]
For an empty goalbase, take \(D=1\). Since the total encoding length is \(L\), the integers \(D\), \(c_i\), and every sum of the \(c_i\) have \(O(L)\) bits. In particular,
\[ D\,U(K)=\sum_{i:K\models\varphi_i}c_i \]
is an integer of polynomial bit length. Because \(D>0\), comparing these integers gives exact utility comparisons.
Using elementary integer arithmetic, computing all \(c_i\) takes \(O(L^3)\) bit operations. Evaluating all formulas at one interpretation and summing the corresponding integers takes at most \(O((m+L)^2)\) bit operations; this conservative bound also allows direct lookup of variable values.
The society’s masses do not affect the decision: only its listed interpretations matter.
Let \(S\) be the nonempty listed support, and define
\[ u_{\min}=\min_{I\in S}U(I). \]
The required condition is equivalent to
\[ U(J)\le u_{\min} \quad\text{for every }J\in\{0,1\}^{V}. \]
Indeed, this condition implies \(U(J)\le U(I)\) for every listed \(I\). Conversely, the original condition applies to an interpretation attaining \(u_{\min}\).
Thus a certificate for a no instance consists of an interpretation \(J\) satisfying
\[ U(J)>u_{\min}. \]
The certificate has \(m\) bits. A verifier computes the listed utilities, their minimum, and \(U(J)\), using exact arithmetic as above. Its running time is
\[ O\!\left(L^3+(\tau+1)(m+L)^2\right). \]
Therefore the complement belongs to NP, and the stated problem belongs to coNP. The strict inequality in the certificate correctly accounts for the permission to have tied maximizers.
We reduce propositional UNSAT, which is coNP-complete under polynomial-time many-one reductions.
Let \(F\) be an arbitrary propositional formula over variables \(X\). Introduce a fresh Boolean variable \(q\), and construct
\[ V=X\cup\{q\}, \qquad G^0=\{(q\land F,1)\}. \]
The society has a single listed interpretation \(I_0\), assigning every variable the value \(0\), with mass \(x_{I_0}=1\). This is a valid society, and the construction has polynomial size.
Since \(I_0(q)=0\),
\[ U(I_0)=0. \]
We check both cases.
\[
U(J)=1>0=U(I_0).
\]
Therefore the constructed instance is a no instance.
Consequently,
\[ F\in\mathrm{UNSAT} \quad\Longleftrightarrow\quad \text{the constructed instance satisfies the required condition}. \]
This proves coNP-hardness. Together with membership, it proves coNP-completeness.
Let \(\mathcal D\) denote the decision problem.
Polynomial time. If \(\mathcal D\in\mathrm P\), the reduction above puts UNSAT, and therefore SAT, in \(\mathrm P\). Since SAT is NP-complete, \(\mathrm P=\mathrm{NP}\). Conversely, if \(\mathrm P=\mathrm{NP}\), closure of \(\mathrm P\) under complement gives \(\mathrm{coNP}=\mathrm P\), so \(\mathcal D\in\mathrm P\).
Many-one NP-hardness. If \(\mathcal D\) were NP-hard under polynomial-time many-one reductions, its membership in coNP would imply \(\mathrm{NP}\subseteq\mathrm{coNP}\): coNP is closed under polynomial-time preimages. Taking complements then gives the reverse inclusion. Conversely, if \(\mathrm{NP}=\mathrm{coNP}\), coNP-hardness immediately implies NP-hardness. Hence
\[ \mathcal D\text{ is many-one NP-hard} \quad\Longleftrightarrow\quad \mathrm{NP}=\mathrm{coNP}. \]
Turing NP-hardness. A SAT instance can be decided by constructing the instance above, making one query to \(\mathcal D\), and negating the answer. Thus \(\mathcal D\) is NP-hard under polynomial-time Turing reductions.
An unconditional deterministic upper bound, obtained by enumerating all interpretations, is
\[ O\!\left(L^3+(\tau+2^m)(m+L)^2\right). \]
The hardness already holds for \(\tau=1\); a small explicitly listed support therefore does not remove the difficulty of comparison against all possible interpretations.
⟨structured verdict parsed — rendered above⟩
The prover’s classification is correct: the decision problem is coNP-complete under polynomial-time many-one reductions, including when the support has one interpretation and the goalbase has one formula with weight \(1\). The proof resolves the task while correctly distinguishing many-one NP-hardness from Turing NP-hardness. No mathematical gaps were found.
The common-denominator construction is valid. Each denominator \(b_i\) is positive, so \(D>0\), each \(D/b_i\) is an integer, and multiplying utilities by \(D\) preserves all comparisons, including equality.
The stated bit-length bounds hold. The bit length of the product \(D\) is bounded by the sum of the denominator bit lengths. Each \(c_i=a_i(D/b_i)\) consequently has \(O(L)\) bits. Summing any subset of the coefficients adds at most a logarithmic factor in the number of goals to the bit length, which remains \(O(L)\). Signed weights cause no difficulty.
The arithmetic bounds are conservative and valid:
The masses can indeed be ignored: the decision condition depends only on the listed interpretations, and the task already requires all listed masses to be positive.
Because the support is finite and nonempty, its minimum utility exists and is attained. The equivalence between the original condition and the bound using \(u_{\min}\) is exact:
Consequently, a no instance has precisely the stated witness: an interpretation \(J\) with \(U(J)>u_{\min}\). The strict inequality correctly excludes tied maximizers from the rejection condition.
The witness has \(m\) bits. Because the input explicitly contains a nonempty support of full interpretations, this witness length is polynomial in the input length. The verifier computes the listed utilities and the witness utility using exact arithmetic in the claimed time
\(O(L^3+(\tau+1)(m+L)^2)\).
Thus the complement belongs to NP, and the decision problem belongs to coNP.
The reduction from propositional UNSAT satisfies all required conditions.
The variable \(q\) is fresh, the formula \(q\land F\) has polynomial encoding size, and the singleton support with mass \(1\) is a valid society. The all-zero listed interpretation has utility zero because it makes \(q\) false, regardless of \(F\).
Both directions are correct:
This establishes the required yes-to-yes and no-to-no equivalence with UNSAT. The cited coNP-completeness of propositional UNSAT applies to precisely the explicitly encoded propositional-formula source problem used here.
Together with membership, this proves the claimed coNP-completeness and its stated restricted-instance version.
All subsequent complexity claims follow correctly.
If the decision problem belongs to P, the reduction decides UNSAT in polynomial time; complementing its answer decides SAT in polynomial time. SAT’s NP-completeness then yields \(\mathrm{P}=\mathrm{NP}\). The converse correctly uses closure of P under complement.
The many-one NP-hardness qualification is also sound. Membership in coNP, together with NP-hardness and closure under polynomial-time preimages, would imply \(\mathrm{NP}\subseteq\mathrm{coNP}\). Taking complements gives the reverse inclusion. Conversely, equality of these classes converts the established coNP-hardness into NP-hardness.
The Turing-hardness claim is valid: the described construction and one negated oracle answer decide SAT. SAT’s NP-completeness then supplies NP-hardness under polynomial-time Turing reductions.
Finally, enumerating all \(2^m\) interpretations gives the stated unconditional running-time bound. Generating those interpretations is absorbed by the bound.
The write-up establishes the claimed classification and handles signed rational weights, empty goalbases, singleton supports, exact comparisons, and ties. No repair or additional clarification is necessary.
⟨structured verdict parsed — rendered above⟩
Tier: machine-proved, adversarially reviewed by an independent model. No human has checked this proof. Generated from pipeline artifacts by tools/atlas_build.py.