Answer: \(\Sigma_2^{\mathrm P}\)-complete; in particular, \(\mathrm{NP}\)-hard.
Theorem 50 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateThe complexity results in Table 1 hold. The results for adm and stb are due to Lehtonen, Wallner, and J¨arvisalo (2021a). We extend the results of (Lehtonen, Wallner, and J¨arvisalo 2021a,b) for grd, com, and pref. Key to establishing the results for our Θ-semantics is the complexity of Θ-defense.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given \(\tau\) supported types \(t=(D_t,a_t)\), where \(D_t\) is a finite ABA+ framework and \(a_t\) an assumption, rational masses \(\mu_t\ge 0\) summing to \(1\), and a rational threshold \(q\), decide whether \(\sum_{t=1}^{\tau}\mu_t\,\mathbf{1}[\exists E\in\Theta\text{-com}(D_t):a_t\in E]\ge q\).
A society is given by its support: a list of \(\tau\) distinct types \(t=(D_t,a_t)\) with positive binary-rational masses \(\mu_t\), where \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types.
Each framework is explicitly encoded as \(D=(\mathcal L,\mathcal R,A,c,\preceq)\): finite sentences, Horn rules with possibly empty bodies, nonempty assumptions \(A\subseteq\mathcal L\), a contrary map \(c:A\to\mathcal L\), and a reflexive transitive preference relation. No rule head belongs to \(A\); the queried assumption belongs to \(A\). Write \(u\prec v\) iff \(u\preceq v\) and \(v\not\preceq u\).
Write \(U\vdash p\) when a finite rule-derivation tree rooted at \(p\) has exactly \(U\) as its assumption-leaf labels; empty-body rules contribute only a dummy truth leaf.
For every \(U\subseteq A\), \(b\in A\) with \(U\vdash c(b)\), include the primitive attack \((U,\{b\})\) if no \(u\in U\) satisfies \(u\prec b\); otherwise include \((\{b\},U)\). Let \(B_D\) contain all these pairs. Define \(S\rightsquigarrow T\) iff some \((P,H)\in B_D\) satisfies \(P\subseteq S\) and \(H\subseteq T\).
A set \(S\subseteq A\) is admissible iff \(S\not\rightsquigarrow S\) and, for every \(T\subseteq A\) with \(T\rightsquigarrow S\), \(S\rightsquigarrow T\).
Define \(\Theta_D(S)=\{a\in A:\forall(P,H)\in B_D\text{ with }a\in H,\ S\rightsquigarrow P\text{ or }S\rightsquigarrow(H\setminus\{a\})\}\). A \(\Theta\)-complete extension is an admissible \(E\) satisfying \(\Theta_D(E)\subseteq E\); denote their family by \(\Theta\text{-com}(D)\).
Given also a binary-rational threshold \(q\in\mathbb Q\), the decision problem asks whether \(\sum_{t=1}^{\tau}\mu_t\mathbf 1[\exists E\in\Theta\text{-com}(D_t):a_t\in E]\ge q\). Let \(m=\max_t|A_t|\) and \(L\) be the total binary input length, including frameworks, masses, and threshold; express running times in \(m,\tau,L\).
Is this supported mass-threshold decision problem in \(\mathrm P\), or is it \(\mathrm{NP}\)-hard?
For a single finite flat ABA+ framework, credulous acceptance under \(\Theta\)-complete semantics is \(\Sigma_2^{\mathrm P}\)-complete. [Source](https://ojs.aaai.org/index.php/AAAI/article/download/28918/29747)
No result for exactly the explicitly supported mass-threshold formulation was identified in the search.
The supported mass-threshold problem is \(\Sigma_2^{\mathrm P}\)-complete under polynomial-time many-one reductions. In particular, it is \(\mathrm{NP}\)-hard. A polynomial-time algorithm would therefore imply \(\mathrm P=\mathrm{NP}\).
A deterministic algorithm runs in time \(O(\tau\,8^m\,\operatorname{poly}(L))\). Thus bounded support size alone does not remove the hardness, whereas fixed \(m\) gives polynomial-time solvability.
Write \(C(D,a)\) for the statement that some \(\Theta\)-complete extension of \(D\) contains \(a\).
The cited paper’s Theorem 50 and Table 1 establish that deciding \(C(D,a)\) is \(\Sigma_2^{\mathrm P}\)-complete for finite flat ABA+ frameworks. Its Definitions 3–6 use the same derivation trees, preferences, attack reversal, and admissibility as the task. Definitions 45 and 47 give the same \(\Theta\)-defense and completeness condition. In particular, they quantify over primitive normal or reversed attacks, exactly as the definition using \(B_D\) does. All the stated hypotheses therefore apply. [Dimopoulos et al., *Redefining ABA+ Semantics via Abstract Set-to-Set Attacks*](https://ojs.aaai.org/index.php/AAAI/article/download/28918/29747)
We use this established theorem for both hardness and membership.
A singleton support already transfers the single-framework hardness: give \((D,a)\) mass \(1\) and choose threshold \(1/2\).
The reduction also works with two distinct types, equal positive masses, and a threshold strictly between \(0\) and \(1\).
Given \((D,a)\), choose fresh sentences \(z,\bar z\) and define \(D_0\) by
This is finite and flat, its assumption set is nonempty, and its preference relation is reflexive and transitive.
The empty-body rule gives \(\varnothing\vdash\bar z\), so
\((\varnothing,\{z\})\in B_{D_0}\). Consequently, every set containing \(z\) attacks itself. No admissible set, and hence no \(\Theta\)-complete extension, contains \(z\). Thus \(C(D_0,z)\) is false.
Construct the society
\[
\]
with support \(\{(D,a),(D_0,z)\}\), masses \(\mu_1=\mu_2=1/2\), and threshold \(q=1/2\). The fresh sentences ensure that the types are distinct. Its accepted mass is exactly
\(\displaystyle \frac12\,\mathbf 1[C(D,a)]+\frac12\,\mathbf 1[C(D_0,z)] =\frac12\,\mathbf 1[C(D,a)].\)
It reaches the threshold precisely when \(C(D,a)\) holds.
The construction has polynomial size and leaves \(m\) unchanged, because the input already has at least one assumption. Therefore the supported problem is \(\Sigma_2^{\mathrm P}\)-hard even when \(\tau=2\), both masses are \(1/2\), and \(q=1/2\).
For each type, put \(x_t=\mathbf 1[C(D_t,a_t)]\). Positivity of the masses gives the equivalence
\(\displaystyle \sum_{t=1}^{\tau}\mu_t x_t\ge q \quad\Longleftrightarrow\quad \exists J\subseteq\{1,\ldots,\tau\}: \sum_{t\in J}\mu_t\ge q \ \text{and}\ C(D_t,a_t)\text{ holds for every }t\in J. \)
For the forward implication, take \(J=\{t:x_t=1\}\). For the reverse implication, every selected type contributes to the full accepted mass, and every additional contribution is nonnegative.
Since single-framework acceptance belongs to \(\Sigma_2^{\mathrm P}\), there is a polynomial-time predicate \(R\), with polynomially bounded strings \(u,v\), such that
\(\displaystyle C(D,a)\Longleftrightarrow\exists u\,\forall v\,R(D,a,u,v).\)
Accordingly, the society condition can be written as
\(\displaystyle \exists J,(u_t)_{t=1}^{\tau}\ \forall(v_t)_{t=1}^{\tau}: \left[\sum_{t\in J}\mu_t\ge q\right] \land \bigwedge_{t\in J}R(D_t,a_t,u_t,v_t). \)
This formula is equivalent to the preceding subset condition. In particular, for any selected \(t\), universal quantification over the tuple includes every possible \(v_t\), so the selected \(u_t\) certifies \(C(D_t,a_t)\).
The support is explicitly listed, so \(\tau\le L\). After padding the individual strings to suitable polynomial bounds, the total existential and universal string lengths are polynomial in \(L\).
The rational comparison is also polynomial-time. Write \(\mu_t=b_t/d_t\) and \(q=r/s\), with positive denominators, and use the common denominator \(Q=s\prod_t d_t\). Its binary length is bounded by the sum of the input denominator lengths. The comparison becomes
\(\displaystyle \sum_{t\in J} b_t(Q/d_t)\ge r(Q/s),\)
using integers of polynomial binary length.
Thus the quantified formula has a polynomial-time matrix and polynomially bounded quantifiers. The problem belongs to \(\Sigma_2^{\mathrm P}\), completing the classification.
The exact-support requirement in \(U\vdash p\) matters: ordinary Horn closure alone does not enumerate those supports. The following algorithm preserves them.
Fix one framework, with \(n=|A|\le m\) and \(N=|\mathcal L|\).
For each sentence \(p\), maintain a family \(F(p)\subseteq 2^A\). Initialize \(F(a)=\{\{a\}\}\) for assumptions \(a\), and initialize all other families to be empty.
Repeatedly apply each rule \(p\leftarrow p_1,\ldots,p_k\), adding to \(F(p)\) every union \(U_1\cup\cdots\cup U_k\) with \(U_i\in F(p_i)\). An empty-body rule adds \(\varnothing\).
Every inserted support has a derivation tree: join the trees witnessing the selected body supports beneath the rule. Conversely, induction on tree height shows that every finite derivation tree contributes its support after finitely many rounds. Hence, at termination,
\(\displaystyle F(p)=\{U\subseteq A:U\vdash p\}.\)
There are at most \(N2^n\) sentence-support pairs. Each nonfinal round inserts at least one new pair, so there are at most \(N2^n+1\) rounds.
For one rule, compute its possible unions one body sentence at a time. Each intermediate family contains at most \(2^n\) sets; combining two families examines at most \(4^n\) pairs. Therefore one round costs \(O(4^n\operatorname{poly}(L))\), and the whole saturation costs \(O(8^n\operatorname{poly}(L))\). This argument also covers cyclic rules.
The support families determine \(B_D\) directly. There are at most \(n2^n\) primitive attacks, because every attack arises from a pair \((U,b)\).
Precompute \(S\rightsquigarrow T\) for all \(4^n\) ordered pairs of assumption sets by scanning \(B_D\). Including subset-test costs, this takes \(O(n^2 8^n)\) time.
Now enumerate every candidate \(E\subseteq A\). Using the table:
These are exactly the defining conditions, so the search decides \(C(D,a)\). Its additional cost fits within \(O(8^n\operatorname{poly}(L))\).
Applying this procedure to all supported types and then comparing their accepted mass exactly gives total running time
\(\displaystyle O\!\left(\tau\,8^m\,\operatorname{poly}(L)\right).\)
The algorithm depends on the explicitly listed support, rather than on the number of possible types.
⟨structured verdict parsed — rendered above⟩
The argument is correct in substance and resolves the task: the supported mass-threshold problem is \(\Sigma_2^{\mathrm P}\)-complete, hence \(\mathrm{NP}\)-hard. The deterministic bound \(O(\tau\,8^m\,\operatorname{poly}(L))\) is also justified.
There are no major issues. One citation needs a minor correction.
The cited result applies to finite flat frameworks with nonempty assumption sets and reflexive, transitive preferences. The paper’s exact derivation supports, normal and reversed attacks, and lifted attack relation match the task. Its Definitions 45 and 47 match the task’s \(\Theta\)-defense and completeness conditions. Theorem 50 and Table 1 give \(\Sigma_2^{\mathrm P}\)-completeness for credulous \(\Theta\)-complete acceptance. [Cited paper](https://ojs.aaai.org/index.php/AAAI/article/download/28918/29747)
The prover correctly invokes this theorem rather than assuming that an explicitly generated attack relation has polynomial size.
Minor issue: The sentence attributing admissibility to “Definitions 3–6” gives an inaccurate reference. Admissibility is defined in Definition 7; Definition 6 supplies conflict-freeness and defense. This does not affect the semantic correspondence.
Minimum clarification: Replace “Definitions 3–6” with “Definitions 3–7.”
The singleton reduction is valid:
The two-type construction is also valid. The auxiliary framework satisfies every structural restriction: its assumption set is nonempty, its sole rule head is outside that set, and its preference relation is reflexive and transitive.
The empty-body rule establishes \(\varnothing\vdash\bar z\). Since the preference condition over the empty support is vacuous, \((\varnothing,\{z\})\) is a primitive normal attack. Every set containing \(z\) therefore attacks itself and fails admissibility. Thus the auxiliary queried assumption cannot be accepted.
Fresh sentence names make the two types distinct. Both masses are positive, their sum is one, and the accepted mass is exactly \(\frac12\mathbf 1[C(D,a)]\). Comparing against \(1/2\) preserves both yes-instances and no-instances.
The claim that \(m\) remains unchanged is correct: the auxiliary framework has one assumption, while the original input already has at least one.
The empty display immediately following “Construct the society” is an editorial artifact. The support, masses, and threshold are completely specified in the following sentence, so no mathematical information is missing.
The subset characterization is correct. Selecting all accepted types proves the forward direction. Nonnegativity of every remaining contribution proves the reverse direction.
The argument handles arbitrary rational thresholds:
The quantified formulation correctly combines the individual acceptance predicates. Existential witnesses are chosen simultaneously, and universal quantification over the tuple tests every challenge for every selected type. Unselected types impose no condition.
The explicit support encoding gives \(\tau\le L\). Polynomial bounds on each individual witness and challenge therefore yield polynomial bounds on the combined strings. Padding is explicitly acknowledged.
The rational comparison is valid. With positive denominators, \(Q=s\prod_t d_t\) is positive and divisible by every required denominator. Multiplication by \(Q\) preserves the inequality, including when the threshold numerator is negative. Its binary length, and the lengths of the resulting sums and products, are polynomial in the input length.
Consequently, the quantified matrix is polynomial-time decidable and establishes membership in \(\Sigma_2^{\mathrm P}\).
The initialization correctly represents assumption leaves. Flatness ensures that rules cannot generate additional supports for assumptions.
Each insertion preserves exact support: joining the selected derivation trees makes the assumption-leaf labels their union. Empty-body rules correctly contribute the empty support.
The converse induction on tree height is valid for finite derivation trees. Cyclic rules cause no difficulty because saturation ranges over finitely many sentence-support pairs.
The termination and cost bounds are correct:
Thus \(O(8^n\operatorname{poly}(L))\) is a valid upper bound.
The bound \(|B_D|\le n2^n\) is correct: each pair \((U,b)\) generates at most one primitive attack.
There are \(4^n\) ordered pairs of assumption sets. Scanning at most \(n2^n\) attacks for each pair, with \(O(n)\) subset tests, gives the claimed \(O(n^2 8^n)\) bound.
The candidate checks exactly implement conflict-freeness, admissibility, \(\Theta\)-closure, and membership of the queried assumption. The attack table includes empty sets, so the algorithm covers empty supports and empty residual heads.
The remaining enumeration costs fit within the stated exponential bound. Summing over the explicitly listed types and performing exact rational comparison gives \(O(\tau\,8^m\,\operatorname{poly}(L))\).
Fixed \(m\) therefore yields polynomial time. Bounded support size alone does not, as hardness already holds for singleton support.
Correct the admissibility reference to Definitions 3–7 and remove the empty display. No additional mathematical argument 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.