Answer: \(\Sigma_2^p\)-complete, even for \(\tau=3\); hence \(\mathrm{NP}\)-hard.
Theorem 6 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximate8h 2 N \ {1, 2} [ {1}, CAS-NONEMPTY[h] is ⌃p 2-complete on normal environments.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite set of types \(T\), positive rational masses \(\mu_t\) summing to \(1\), a normal ASP module \(P_t\), and a per-agent payoff function \(w_t\) for each type, does there exist a grand-coalition answer set \(M \in AS(P_T)\) whose type payoffs \(x_t=w_t(M)\) are individually rational and efficient, and for which no nonzero submass \(q\), with \(0 \le q_t \le \mu_t\), has a blocking answer set \(M' \in AS(P_{S(q)})\) satisfying \(w_t(M')>x_t\) for every active type \(t \in S(q)=\{t:q_t>0\}\)?
A society is given by its support: a list \(T\) of \(\tau\geq 3\) types with positive binary-rational masses \(\mu_t\), where \(\sum_{t\in T}\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types.
Each type has a finite ground normal ASP module \(P_t\) over a common atom set \(\Gamma\supseteq T\); type atoms occur only in rule bodies. Its payoff function \(w_t:2^\Gamma\to\mathbb Q\) is encoded by a Boolean circuit outputting a signed binary numerator and a positive binary denominator; negative payoffs are allowed.
For \(S\subseteq T\), define \(P_S=\bigcup_{t\in S}(P_t\cup\{t.\})\), and let \(AS(P_S)\) denote its stable models. An outcome is a single answer set, with every participant of type \(t\) receiving the same per-agent payoff \(w_t(M)\).
A coalition is a real vector \(q\) satisfying \(0\leq q_t\leq\mu_t\) and \(\sum_tq_t>0\), with active support \(S(q)=\{t:q_t>0\}\). Its available outcomes are \(AS(P_{S(q)})\); quantities do not otherwise affect programs or payoffs, and the full society may deviate.
For \(M\in AS(P_T)\), put \(x_t=w_t(M)\). Individual rationality means \(x_t\geq w_t(A)\) for every \(t\in T\) and \(A\in AS(P_{\{t\}})\), vacuously if this answer-set family is empty. Efficiency means that every \(A\in AS(P_T)\) has some \(t\in T\) with \(x_t\geq w_t(A)\).
A coalition \(q\) blocks \(M\) if some \(A\in AS(P_{S(q)})\) satisfies \(w_t(A)>x_t\) for every \(t\in S(q)\). The decision problem asks whether an individually rational, efficient grand-coalition answer set exists that no coalition blocks.
Let \(m=|\Gamma|\) and \(L\) be the total binary input length, including modules, circuits, and masses; state running times in \(m,\tau,L\).
Is this continuous core-existence decision problem solvable in polynomial time in \(m,\tau,L\), or is it NP-hard?
For finite agents, core-answer-set existence for normal modules is \(\Sigma_2^p\)-complete, even for each fixed number of agents at least three and additively separable payoffs. [Source](https://www.ijcai.org/Proceedings/16/Papers/013.pdf)
No published result specifically addressing the mass formulation above was located.
The problem is \(\mathrm{NP}\)-hard, even with exactly three types and payoffs in \(\{0,1\}\). In fact, the supplied finite-agent hardness theorem implies \(\Sigma_2^p\)-completeness. Thus a polynomial-time algorithm in \(m,\tau,L\) would imply \(\mathrm{P}=\mathrm{NP}\).
1. Coalition quantities can be eliminated
For a grand-coalition answer set \(M\), write \(x_t=w_t(M)\).
Lemma. A coalition blocks \(M\) if and only if there exist a nonempty \(S\subseteq T\) and \(A\in AS(P_S)\) such that \(w_t(A)>x_t\) for every \(t\in S\).
Proof. A blocking coalition \(q\) supplies such a witness with \(S=S(q)\), directly by definition. Conversely, given \(S,A\), choose \(q_t=\mu_t\) for \(t\in S\) and \(q_t=0\) otherwise. Positivity of the masses makes this an admissible coalition with active support exactly \(S\). The assumed inequalities make it block \(M\). \(\square\)
Consequently, the numerical masses have no effect on core existence, provided every listed mass is positive.
Moreover, absence of blocking already implies both additional requirements:
Thus the question is exactly whether some \(M\in AS(P_T)\) has no blocking support.
2. A direct, self-contained satisfiability reduction
We first prove the requested hardness independently of the cited finite-agent theorem.
Let \(\varphi\) be a Boolean formula with variables \(v_1,\ldots,v_n\). Construct three types \(T=\{t_1,t_2,t_3\}\), with masses
\[ \mu_{t_1}=\mu_{t_2}=\frac14,\qquad \mu_{t_3}=\frac12. \]
Introduce distinct atoms \(a_i,b_i\) for each variable, and take \(\Gamma=T\cup\{a_i,b_i:1\leq i\leq n\}\).
The module \(P_{t_1}\) contains, for every \(i\), the two normal rules
\[ a_i\leftarrow t_2,t_3,\operatorname{not}b_i, \qquad b_i\leftarrow t_2,t_3,\operatorname{not}a_i. \]
Set \(P_{t_2}=P_{t_3}=\varnothing\). Type atoms occur only in module rule bodies, as required.
For any interpretation \(B\subseteq\Gamma\), let \(\alpha_B(v_i)=1\) precisely when \(a_i\in B\). Define
\[ w_{t_1}(B)= \begin{cases} \varphi(\alpha_B),&t_2,t_3\in B,\\ 1,&\text{otherwise}, \end{cases} \qquad w_{t_2}(B)=w_{t_3}(B)=0, \]
where the Boolean formula value is interpreted as an integer in \(\{0,1\}\). These functions have polynomial-size Boolean circuits; every denominator is the constant \(1\).
Answer sets of the construction. For every proper support \(S\subsetneq T\), the unique answer set is \(S\). Indeed, either \(P_{t_1}\) is absent or at least one of its positive guards \(t_2,t_3\) is absent. No rule can then derive an assignment atom, and the reduct’s least model consists exactly of the support facts.
For the full support, the answer sets are exactly
\[ M_\alpha=T\cup \{a_i:\alpha(v_i)=1\}\cup \{b_i:\alpha(v_i)=0\}, \]
one for every Boolean assignment \(\alpha\). To verify this, consider each pair of choice rules:
Thus stability requires exactly one atom from each pair, and every such selection is the least model of its reduct.
In particular, every nonempty coalition has an answer set, and the grand coalition always has answer sets.
Correctness of the reduction. A grand outcome \(M_\alpha\) has payoff vector \((\varphi(\alpha),0,0)\). The singleton support \(\{t_1\}\) has outcome \(\{t_1\}\), giving type \(t_1\) payoff \(1\). Therefore \(M_\alpha\) is individually rational exactly when \(\varphi(\alpha)=1\); the other two singleton comparisons are \(0\geq0\).
Every grand outcome is efficient, because type \(t_2\) receives \(0\) in every grand outcome.
If \(\varphi(\alpha)=1\), no coalition blocks \(M_\alpha\): a support containing \(t_2\) or \(t_3\) cannot strictly improve that type’s constant zero payoff, while support \(\{t_1\}\) can obtain only its current payoff \(1\). If \(\varphi(\alpha)=0\), support \(\{t_1\}\) blocks.
Hence
\[ \varphi\text{ is satisfiable} \quad\Longleftrightarrow\quad \text{the constructed society has a core answer set}. \]
The construction has \(m=2n+3\), \(\tau=3\), and input length \(L\) polynomial in the formula’s binary input length. Its construction time is polynomial as well. This proves \(\mathrm{NP}\)-hardness under polynomial-time many-one reductions.
3. Upper bound and stronger classification
For a normal ground program, stable-model verification is polynomial-time: form the reduct, compute its least Horn model, and compare it with the proposed interpretation. If headless constraints are permitted, also check their satisfaction.
Payoff evaluation and comparison are polynomial-time in \(L\). Specifically, comparing signed rational outputs \(n_1/d_1\) and \(n_2/d_2\) reduces to comparing the integers \(n_1d_2\) and \(n_2d_1\), because both denominators are positive.
Define the polynomial-time predicate
\[ B(M,S,A)\iff S\neq\varnothing \ \land\ A\in AS(P_S) \ \land\ \bigwedge_{t\in S}w_t(A)>w_t(M). \]
By Section 1, the decision problem is expressed by
\[ \exists M\subseteq\Gamma\; \forall S\subseteq T\; \forall A\subseteq\Gamma: \left[M\in AS(P_T)\land\neg B(M,S,A)\right]. \]
The existential witness has \(m\) bits, and the universal witness has \(\tau+m\) bits. The matrix is polynomial-time decidable. This proves membership in \(\Sigma_2^p\).
For hardness at that level, apply the supplied finite-agent theorem. Theorem 6 and Table 1 of [Amendola, Greco, Leone, and Veltri](https://www.ijcai.org/Proceedings/16/Papers/013.pdf) give \(\Sigma_2^p\)-hardness for normal modules with three agents and additively separable weights. Their module construction and strict blocking definition agree with the present definitions.
Map those three agents to three types, retain their modules, and assign masses \((1/4,1/4,1/2)\). Compile their additive payoff functions into the required circuits. In the cited hardness construction the atom weights are binary integers: a circuit selects each atom’s constant weight according to its membership bit and sums the selected constants. With \(m\) atom weights of at most \(b\) bits, a signed sum needs only \(b+\lceil\log_2(m+1)\rceil+2\) bits, so this compilation has polynomial size. Set the output denominator to \(1\).
Every support has exactly the same program and payoff outcomes before and after this transformation. Section 1 proves that its finite-agent blocking witnesses are exactly the continuous coalition blocking witnesses. Individual rationality and efficiency are preserved as well. This is therefore a polynomial-time many-one reduction, proving \(\Sigma_2^p\)-hardness even for \(\tau=3\).
Together with membership, the problem is \(\Sigma_2^p\)-complete.
4. Running time
A direct deterministic algorithm enumerates all \(2^m\) candidate interpretations \(M\), verifies grand-coalition stability, and searches all \(2^\tau\) supports and all \(2^m\) interpretations for a blocking witness. Its running time is
\[ O\!\left(2^{\,2m+\tau}\operatorname{poly}(m,\tau,L)\right). \]
It can use polynomial space by enumerating witnesses sequentially. The hardness result rules out a polynomial-time algorithm in \(m,\tau,L\) unless \(\mathrm{P}=\mathrm{NP}\), even when \(\tau\) is fixed at three.
⟨structured verdict parsed — rendered above⟩
The output resolves the task correctly. The direct reduction proves \(\mathrm{NP}\)-hardness with exactly three types and payoffs in \(\{0,1\}\). The upper bound and the verified application of the supplied theorem also establish \(\Sigma_2^p\)-completeness. No major or minor mathematical issues were found.
1. Elimination of coalition quantities
Both directions of the lemma are valid.
This argument uses precisely the task’s assumption that quantities affect neither available outcomes nor per-agent payoffs. It establishes that the masses do not affect core existence on the specified input domain.
The redundancy of individual rationality and efficiency is also correctly justified. Failure of individual rationality supplies a strictly improving singleton outcome. Failure of efficiency supplies a grand-coalition outcome strictly improving every type. Both are admissible blocking witnesses. Empty singleton answer-set families cause no difficulty because their comparisons are vacuous.
2. Validity of the satisfiability construction
The constructed instance satisfies the input restrictions:
The payoff functions are defined on every interpretation, including interpretations that are not stable models. All payoffs lie in \(\{0,1\}\), as claimed.
3. Characterization of answer sets
For a proper support, the argument correctly separates the possibilities: either the only nonempty module is absent, or one of its positive type guards is unavailable. Because absent type atoms have no defining heads, they cannot enter the reduct’s least model. Consequently, no assignment atom is derived, and the unique stable model consists of the support facts.
For the full support, the three cases for each assignment pair are exhaustive and correctly analyzed:
The type facts activate all surviving rules. There are no other assignment-producing rules, so selections for distinct variables do not interfere. The asserted correspondence between assignments and grand-coalition stable models follows.
The construction also handles the zero-variable case: there are no assignment pairs, and the grand program has the single stable model consisting of its type facts.
4. Correctness of the reduction
For a grand outcome \(M_\alpha\), the payoff vector is correctly computed as \((\varphi(\alpha),0,0)\).
The singleton outcome for the first type yields payoff \(1\). Thus individual rationality holds exactly when the assignment satisfies the formula; the other singleton comparisons impose no additional restriction.
Every grand outcome satisfies the task’s efficiency definition because the second type receives the same payoff in every grand outcome. Equality is sufficient under that definition.
The blocking analysis covers every nonempty support. Any support containing the second or third type cannot strictly improve every member, since that member’s payoff is constantly zero. The only remaining support is the first singleton, whose available payoff is \(1\). It blocks exactly the grand outcomes with first payoff zero.
Therefore the displayed satisfiability equivalence is valid in both directions. The construction has polynomial output length and construction time, establishing a polynomial-time many-one reduction.
5. Upper bound
Stable-model verification for finite ground normal programs is polynomial-time by the reduct and least-model procedure stated in the output. The qualification concerning headless constraints is appropriate.
Circuit outputs have bit lengths bounded by their encoded sizes. Positive denominators justify cross multiplication without changing inequality direction, and the resulting integer products have polynomial bit length. Negative numerators therefore introduce no problem.
The predicate \(B(M,S,A)\) is polynomial-time decidable. It explicitly excludes the empty support and checks stability and strict improvement only for active types.
The quantified expression has an existential witness of \(m\) bits and a universal witness of \(\tau+m\) bits. Keeping grand-coalition stability inside the universal matrix is logically valid: the universal domain is nonempty, so an unstable existential candidate cannot satisfy the expression. This proves membership in \(\Sigma_2^p\).
6. Transfer of the cited hardness theorem
Theorem 6 and Table 1 confirm \(\Sigma_2^p\)-hardness for core-answer-set existence with three agents, normal modules, and additively separable weights. The paper’s module formation, restriction on agent atoms, and strict blocking comparisons match the relevant definitions here. Its displayed hardness construction uses integer atom weights. [Source: Amendola et al.](https://www.ijcai.org/Proceedings/16/Papers/013.pdf)
The proposed transformation preserves modules and payoff functions while replacing agents with types of positive mass. The support lemma establishes the necessary correspondence of blocking witnesses.
The additive-weight circuit compilation is polynomial in size. Summing at most \(m\) signed weights of at most \(b\) bits requires only the stated conservative output-width bound. The cited construction’s weights have polynomial binary length, even when their numerical values are exponential.
Thus the stronger hardness transfer is justified. This completeness claim concerns the general payoff-circuit problem; the separate Boolean-payoff reduction establishes the stated restricted \(\mathrm{NP}\)-hardness.
7. Running time and conclusion
The deterministic enumeration bound correctly counts at most \(2^m\) grand candidates, \(2^\tau\) supports, and \(2^m\) outcome interpretations for each candidate-support pair. Each verification costs \(\operatorname{poly}(m,\tau,L)\), yielding the stated bound.
Sequential enumeration and polynomial-time verification require only polynomial space. The conditional exclusion of a polynomial-time algorithm unless \(\mathrm{P}=\mathrm{NP}\) follows from the independently established hardness.
No additional clarification or repair is needed.
⟨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.