Answer: \(\mathrm{coNP}\)-complete under polynomial-time many-one reductions, even for \(\tau=1\) and unit costs; \(\mathrm{NP}\)-hard under polynomial-time Turing reductions; in \(\mathrm{P}\) if and only if \(\mathrm{P}=\mathrm{NP}\).
Theorem 1 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateCORE MEMBERSHIP is co-NP-complete, even in games with a single agent, and even when the valuation to be check- ed is empty. PROOF. Membership of co-NP is clear from the statement of the problem. For hardness, we reduce SAT to the complement of the problem, i.e., the problem of determining whether a valuation is blocked. Let Ψ be the SAT instance, with Boolean variables x1, . . . , xk.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a one-agent CBG template with Boolean variables [Phi[0m (that is, [0m\(\Phi\)), costs \(c\), and goal [gamma[0m (that is, [0m\(\gamma\)), together with a finite-support rational distribution [x_xi[0m (that is, [0m\(x_\xi\)) over local valuations [xi subset Phi[0m (that is, [0m\(\xi\subseteq\Phi\)), decide whether it is in the atomless core: whether there is no measurable coalition of positive mass whose members can change only their private Boolean variables so that every member strictly prefers their resulting local valuation under the template's goal-first, cost-second preferences.
Let \(\Phi\) be a nonempty set of \(m\) Boolean variables, let \(\gamma\) be an explicitly represented propositional formula over \(\Phi\), and let \(c:\Phi\to\mathbb{Q}_{\geq 0}\) give binary rational costs.
Each individual controls a private copy of all variables in \(\Phi\); its goal is evaluated solely on its own local valuation. For \(\xi\subseteq\Phi\), set \(k(\xi)=\sum_{p\in\xi}c(p)\) and \(u(\xi)=(1+\sum_{p\in\Phi}c(p))\mathbf{1}_{\xi\models\gamma}-k(\xi)\). Strict preference means strictly greater utility; equal utilities are indifference.
A society is given by its support: the list of the \(\tau\) distinct local valuations with positive mass, each mass \(x_\xi\) a binary rational, with \(\sum_\xi x_\xi=1\). Here \(\tau\) is the support size, not the number \(2^m\) of possible types.
Realize the society on \([0,1]\) with Lebesgue measure \(\lambda\), partitioned into measurable sets \(A_\xi\) of measure \(x_\xi\); the initial valuation map is \(v(t)=\xi\) on \(A_\xi\).
A blocking coalition is a measurable set \(C\) with \(\lambda(C)>0\), together with a measurable map \(w:[0,1]\to 2^\Phi\), such that \(w(t)=v(t)\) outside \(C\) and \(u(w(t))>u(v(t))\) for every \(t\in C\). Members may choose different valuations, including valuations outside the input support. Atomless core membership means that no such coalition exists.
Let \(L\) be the total input bit length, including the formula, costs, support valuations, and masses; state running times in \(m,\tau,L\).
Is atomless core membership in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard?
Discrete CBG core membership is \(\mathrm{coNP}\)-complete even with one agent and the empty initial valuation ([Dunne et al., 2008](https://www.cs.ox.ac.uk/people/michael.wooldridge/pubs/aamas2008d.pdf)).
No result settling this exact atomless problem was identified in the literature search.
Result.
Atomless core membership is \(\mathrm{coNP}\)-complete under polynomial-time many-one reductions, even when \(\tau=1\), the supported valuation is empty, and every variable has cost one.
Consequently, it belongs to \(\mathrm{P}\) if and only if \(\mathrm{P}=\mathrm{NP}\). It is \(\mathrm{NP}\)-hard under polynomial-time Turing reductions. Under polynomial-time many-one reductions, it is \(\mathrm{NP}\)-hard if and only if \(\mathrm{NP}=\mathrm{coNP}\). Thus the question’s proposed dichotomy needs this reduction-type qualification.
1. Characterizing blocking coalitions.
Write \(S\subseteq 2^\Phi\) for the input support, and define \(U^*=\max_{\eta\subseteq\Phi}u(\eta)\). This maximum exists because \(2^\Phi\) is finite.
We claim that the society belongs to the atomless core if and only if \(u(\xi)=U^*\) for every \(\xi\in S\).
Suppose first that some \(\xi\in S\) and \(\eta\subseteq\Phi\) satisfy \(u(\eta)>u(\xi)\). Take \(C=A_\xi\), and define \(w(t)=\eta\) on \(A_\xi\) and \(w(t)=v(t)\) elsewhere. Because \(A_\xi\) is measurable and \(v\) is a measurable map with finite range, \(w\) is measurable. Moreover, \(\lambda(C)=x_\xi>0\), and every member of \(C\) strictly improves. Hence \(C\) blocks.
Conversely, suppose every supported valuation attains \(U^*\). For every individual \(t\) and every alternative valuation \(\eta\), we have \(u(\eta)\leq U^*=u(v(t))\). Thus no individual can strictly improve, so no blocking coalition exists.
In particular, nonmembership is equivalent to the existence of a pair \((\xi,\eta)\) with \(\xi\in S\), \(\eta\subseteq\Phi\), and \(u(\eta)>u(\xi)\). The alternative \(\eta\) need not belong to the support. This characterization also proves that membership is independent of the particular measurable realization and of the positive masses.
2. Membership in \(\mathrm{coNP}\).
A certificate of nonmembership consists of a support index and an alternative valuation \(\eta\), using \(O(\log(\tau+1)+m)\) bits. The verifier evaluates \(\gamma\) at the two valuations and compares their utilities exactly.
To justify polynomial-time rational arithmetic, write \(c(p)=a_p/b_p\), where \(a_p\) is a nonnegative integer and \(b_p\) a positive integer. Let \(Q=\prod_{p\in\Phi}b_p\) and \(d_p=a_p(Q/b_p)\). Multiplication by the positive integer \(Q\) preserves strict utility comparisons, and
\(Q\,u(\eta)=\left(Q+\sum_{p\in\Phi}d_p\right)\mathbf{1}_{\eta\models\gamma}-\sum_{p\in\eta}d_p.\)
All these integers have \(O(L)\) bits: the bit length of \(Q\) is bounded by the total denominator encoding length, and multiplication by a numerator and summation add at most \(O(L)\) further bits. Schoolbook integer arithmetic therefore suffices for polynomial-time verification.
A conservative verification bound, including reading the input, is \(O((\tau+1)mL^2)\) bit operations. Hence nonmembership belongs to \(\mathrm{NP}\), and membership belongs to \(\mathrm{coNP}\).
3. Hardness with one supported valuation.
We give a polynomial-time many-one reduction from propositional unsatisfiability, which is \(\mathrm{coNP}\)-complete.
Let \(F\) be an arbitrary propositional formula on a variable set \(X\). Introduce a fresh variable \(q\), and construct the instance with \(\Phi=X\cup\{q\}\), \(\gamma=F\land q\), and \(c(p)=1\) for every \(p\in\Phi\). Its sole supported valuation is \(\varnothing\), with mass one. Thus \(\tau=1\), and \(\Phi\) is nonempty.
Since \(q\) is false at \(\varnothing\), its utility is \(u(\varnothing)=0\).
If \(F\) is satisfiable, choose a satisfying valuation \(\zeta\subseteq X\) and put \(\eta=\zeta\cup\{q\}\). Then \(\eta\models\gamma\), and, writing \(m=|\Phi|\),
\(u(\eta)=1+m-|\eta|\geq 1>0=u(\varnothing).\)
By Section 1, the society is outside the core.
If \(F\) is unsatisfiable, no valuation satisfies \(\gamma\). Therefore every \(\eta\subseteq\Phi\) has utility \(u(\eta)=-|\eta|\leq 0=u(\varnothing)\). Again by Section 1, the society belongs to the core.
We have proved \(F\in\mathrm{UNSAT}\) if and only if its constructed society belongs to the atomless core. The construction has polynomial size, establishing \(\mathrm{coNP}\)-hardness. Together with Section 2, this proves \(\mathrm{coNP}\)-completeness.
This reduction follows the same formula construction used for the discrete result in [Dunne et al., Theorem 1](https://www.cs.ox.ac.uk/people/michael.wooldridge/pubs/aamas2008d.pdf); Section 1 supplies the explicit justification for the present atomless model.
4. Running time and the meaning of hardness.
An exact deterministic algorithm computes \(b=\min_{\xi\in S}u(\xi)\), enumerates all \(2^m\) valuations, and rejects membership if it finds an \(\eta\) with \(u(\eta)>b\). The characterization in Section 1 proves correctness.
Using the integer scaling above, a conservative running-time bound is \(O((2^m+\tau+1)mL^2)\) bit operations. Thus fixed \(m\) gives polynomial time, but fixed support size does not remove the hardness: the reduction already has \(\tau=1\).
Finally:
⟨structured verdict parsed — rendered above⟩
The prover resolves the task correctly. Atomless core membership is \(\mathrm{coNP}\)-complete under polynomial-time many-one reductions, including the stated restriction to one supported valuation and unit costs. The qualifications concerning \(\mathrm{NP}\)-hardness are also correct. No major or minor mathematical issues were found.
The maximum \(U^*\) exists because the set of possible valuations is finite and nonempty.
If a supported valuation \(\xi\) admits a strictly better alternative \(\eta\), the proposed coalition \(C=A_\xi\) has positive measure because supported masses are strictly positive. The map \(w\) is measurable: it agrees with a measurable finite-range map outside a measurable set and is constant on that set. It preserves the initial valuation outside \(C\) and strictly improves utility at every point of \(C\), exactly as required.
Conversely, the measurable partition assigns every individual a supported valuation. If every supported valuation maximizes utility, no individual has a strictly improving alternative. This excludes every blocking coalition, including coalitions whose members choose different alternatives.
Thus the equivalence is established with the required pointwise strict inequality. Alternatives outside the input support are correctly allowed. Independence from the realization and from the positive masses follows for a fixed support.
A support index and an \(m\)-bit alternative valuation form a polynomial-size certificate. The characterization proves both completeness and soundness of this certificate: nonmembership yields such a pair, and every verified pair yields a blocking coalition.
Evaluating an explicitly represented propositional formula under a supplied valuation takes polynomial time. The rational-arithmetic argument is correct. Every denominator is positive, so \(Q\) is positive and scaling preserves strict inequalities. Each \(Q/b_p\) is an integer, and the displayed expression for \(Q\,u(\eta)\) follows directly from the utility definition.
The integers have \(O(L)\) bits. The product of denominators has bit length bounded by their total encoding length; multiplying by a numerator and summing at most \(m\) terms retains an \(O(L)\) bound. Zero numerators cause no difficulty. Schoolbook arithmetic therefore supplies polynomial-time exact verification.
The stated bound \(O((\tau+1)mL^2)\) is conservative but valid. Consequently, nonmembership is in \(\mathrm{NP}\), and membership is in \(\mathrm{coNP}\).
The construction produces a valid instance: the fresh variable ensures that \(\Phi\) is nonempty, unit costs are permitted binary rational costs, and the singleton support with mass one satisfies all support requirements. The construction has polynomial size and can be performed in polynomial time.
The fresh variable is false at the empty valuation, so \(\gamma\) is false there and the initial utility is exactly zero.
When \(F\) is satisfiable, the constructed alternative satisfies \(\gamma\). Since \(|\eta|\leq m\), its utility is at least one, giving the strict improvement required for blocking.
When \(F\) is unsatisfiable, every valuation fails \(\gamma\), so every utility equals \(-|\eta|\leq0\). The empty valuation is therefore a global maximizer. This includes indifference correctly: equal utility does not create a block.
Both directions of the reduction from \(\mathrm{UNSAT}\) are established. Together with the upper bound, they prove the claimed restricted \(\mathrm{coNP}\)-completeness.
The attribution is accurate: [Dunne et al., Theorem 1](https://www.cs.ox.ac.uk/people/michael.wooldridge/pubs/aamas2008d.pdf) uses the same fresh-variable conjunction and unit-cost construction. The present proof independently verifies its applicability to the atomless model.
The minimum supported utility \(b\) exists because the support is nonempty. An alternative with utility greater than \(b\) strictly improves a supported valuation attaining that minimum. Conversely, any alternative improving any supported valuation also has utility greater than \(b\). Thus the enumeration algorithm is correct.
Using the same scaled integers, the bound \(O((2^m+\tau+1)mL^2)\) is valid. Fixed \(m\) gives polynomial time. The singleton-support reduction correctly demonstrates that fixing \(\tau\) does not eliminate the hardness.
A polynomial-time membership algorithm would decide satisfiability by reversing the answer on the constructed instance. Conversely, if \(\mathrm{P}=\mathrm{NP}\), then \(\mathrm{coNP}=\mathrm{P}\), so membership is polynomial-time decidable.
The answer-reversing procedure is a valid polynomial-time Turing reduction and establishes Turing \(\mathrm{NP}\)-hardness.
Many-one \(\mathrm{NP}\)-hardness of a language in \(\mathrm{coNP}\) would imply \(\mathrm{NP}\subseteq\mathrm{coNP}\); taking complements gives equality. Conversely, equality makes the established \(\mathrm{coNP}\)-completeness imply many-one \(\mathrm{NP}\)-hardness. The proposed dichotomy is therefore qualified correctly.
No repair or additional clarification is required.
⟨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.