Answer: Polynomial-time solvable; the grounded labelling is the unique Pareto-optimal complete labelling.
Theorem 3 — class: other
PDF text-layer excerpt — equations and symbol order may be approximateIf agents have rejection-minimising prefer- ences, then for any outcome L ∈L, either L is the grounded extension, or L is Pareto dominated by the grounded exten- sion.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite argumentation framework \(AF=(A,\rightharpoonup)\) and a rational finite-support distribution \(\mu\) over types \(t=(A_t,\mathrm{reject})\), where \(A_t\subseteq A\), find the complete labellings that are Pareto optimal when each positive-mass type has utility \(u_t(L)=-|out(L)\cap A_t|\).
Given a finite argumentation framework \(AF=(A,\rightharpoonup)\), let \(m=|A|\); outcomes are complete labellings under Dung semantics, and \(\operatorname{out}(\ell)=\{a\in A:\ell(a)=\mathrm{out}\}\).
A society is given by its support: a list of \(\tau\) types \(t=(A_t,\mathrm{reject})\), each with positive binary rational mass \(\mu_t\), where \(A_t\subseteq A\) and \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types; let \(L\) be the total input bit length.
Require \(\bigcup_{t\in\operatorname{supp}(\mu)}A_t=A\); argument sets may overlap and individual sets may be empty.
Each type has utility \(u_t(\ell)=-|\operatorname{out}(\ell)\cap A_t|\), with higher utility preferred and equal utilities tied.
A complete labelling \(\ell'\) dominates \(\ell\) when \(u_t(\ell')\geq u_t(\ell)\) for every supported type and the inequality is strict for at least one supported type. A labelling is Pareto optimal if no complete labelling dominates it.
Can all Pareto-optimal complete labellings be computed in time polynomial in \(m,\tau,L\), or is this computation NP-hard?
For finite agent populations with rejection-minimising preferences and argument coverage, the grounded labelling is Pareto optimal and dominates every other complete labelling. [Rahwan–Larson, 2008](https://cdn.aaai.org/AAAI/2008/AAAI08-024.pdf)
The extended treatment repeats this characterization and explicitly allows overlapping argument sets. [Larson–Rahwan, 2008](https://comsoc-community.org/assets/proceedings/comsoc-2008/Larson.pdf) No separate result for the specified mass formulation was identified in the search.
All Pareto-optimal complete labellings can be computed in polynomial time in \(m,\tau,L\): there is exactly one, the grounded labelling.
This agrees with Theorem 3 and Corollary 1 of [Rahwan–Larson (2008)](https://cdn.aaai.org/AAAI/2008/AAAI08-024.pdf). Below is a self-contained proof for the specified support-and-mass formulation, allowing overlapping and empty argument sets.
For \(a\in A\), define its attackers by \(\operatorname{Att}(a)=\{b\in A:b\rightharpoonup a\}\).
A complete labelling satisfies both equivalences:
Every remaining argument is labelled \(\mathrm{undec}\).
Starting with \(I_0=O_0=\varnothing\), define simultaneously
\(I_{k+1}=\{a\in A:\operatorname{Att}(a)\subseteq O_k\}\),
\(O_{k+1}=\{a\in A:\operatorname{Att}(a)\cap I_k\ne\varnothing\}\).
We verify the properties needed for this construction.
Monotonicity. Both update rules are monotone in their respective input sets. Since \(I_0\subseteq I_1\) and \(O_0\subseteq O_1\), induction gives \(I_k\subseteq I_{k+1}\) and \(O_k\subseteq O_{k+1}\) for every \(k\).
Disjointness. Initially \(I_0\cap O_0=\varnothing\). Suppose \(I_k\cap O_k=\varnothing\). If \(a\in I_{k+1}\cap O_{k+1}\), then some attacker \(b\) of \(a\) belongs to \(I_k\). But membership of \(a\) in \(I_{k+1}\) requires every attacker, including \(b\), to belong to \(O_k\). This contradicts disjointness. Thus \(I_k\cap O_k=\varnothing\) for all \(k\).
Termination and completeness. Every nonstationary iteration adds at least one argument to the two growing, disjoint sets. There are only \(m\) arguments, so after at most \(m\) such iterations the pair stabilizes at \((I_*,O_*)\). Label these sets \(\mathrm{in}\) and \(\mathrm{out}\), respectively, and the complement \(\mathrm{undec}\). The fixed-point equations are exactly the two complete-labelling equivalences above, so this defines a complete labelling \(g\).
Leastness. Let \(\ell\) be any complete labelling, with in-set \(I_\ell\) and out-set \(O_\ell\). We prove inductively that \(I_k\subseteq I_\ell\) and \(O_k\subseteq O_\ell\).
The assertion holds at \(k=0\). If it holds at \(k\), then:
Consequently \(I_*\subseteq I_\ell\) and \(O_*\subseteq O_\ell\) for every complete labelling. In particular, \(g\) has the least complete in-set and is therefore the grounded labelling.
We have proved \(\operatorname{out}(g)\subseteq\operatorname{out}(\ell)\) for every complete labelling \(\ell\).
The out-set uniquely determines a complete labelling: its in-set is necessarily
\(\operatorname{in}(\ell)=\{a\in A:\operatorname{Att}(a)\subseteq\operatorname{out}(\ell)\}\),
and its undecided set is the complement of its in-set and out-set.
Therefore, if \(\ell\ne g\), their out-sets cannot be equal. Hence
\(\operatorname{out}(g)\subsetneq\operatorname{out}(\ell)\).
For every supported type \(t\), out-set inclusion implies
\(\lvert\operatorname{out}(g)\cap A_t\rvert\leq\lvert\operatorname{out}(\ell)\cap A_t\rvert\),
and therefore \(u_t(g)\geq u_t(\ell)\).
Now suppose \(\ell\ne g\). Choose \(a\in\operatorname{out}(\ell)\setminus\operatorname{out}(g)\). Coverage supplies a supported type \(t_0\) with \(a\in A_{t_0}\). The intersection inclusion for this type is strict, giving
\(\lvert\operatorname{out}(g)\cap A_{t_0}\rvert<\lvert\operatorname{out}(\ell)\cap A_{t_0}\rvert\),
so \(u_{t_0}(g)>u_{t_0}(\ell)\). Thus \(g\) dominates every other complete labelling.
Conversely, no complete labelling dominates \(g\), because every complete labelling has utility at most \(u_t(g)\) for every supported type. Hence \(g\) is the unique Pareto-optimal complete labelling.
Overlaps do not affect this argument; coverage is used only to find \(t_0\). Empty sets contribute constant zero utilities. The masses do not enter the stated dominance definition, so their magnitudes and denominators do not affect the characterization.
Let \(q=\lvert\rightharpoonup\rvert\). Each iteration above can be implemented by scanning the arguments and attacks, using \(O(m+q)\) elementary graph operations. There are at most \(m\) nonstationary iterations and one final equality check, giving \(O((m+1)(m+q))\) graph operations.
Since \(q\leq m^2\), this is polynomial. Reading the full input adds polynomial cost in \(L\), including the support and binary rational masses. Outputting \(g\) requires only \(m\) labels.
Thus the algorithm computes all Pareto-optimal complete labellings by returning the singleton \(\{g\}\).
⟨structured verdict parsed — rendered above⟩
The prover’s claim is proved. The argument establishes that the grounded labelling is the unique Pareto-optimal complete labelling and gives a polynomial-time algorithm that outputs it. No major or minor issues were found.
The two stated equivalences correctly characterize complete labellings:
For a total labelling, assigning \(\mathrm{undec}\) to the remaining arguments supplies the third label. The construction subsequently establishes disjointness, so these assignments are consistent.
Monotonicity: Correct. Both update maps preserve inclusion. Starting from the empty pair, the induction establishes that both sequences grow monotonically. Simultaneous updating introduces no problem.
Disjointness: Correct. If an argument belonged to both updated sets, its membership in \(O_{k+1}\) would supply an attacker in \(I_k\), while membership in \(I_{k+1}\) would force that same attacker into \(O_k\). This contradicts the induction hypothesis.
Termination: Correct. Every change adds at least one argument to the union of two growing, disjoint subsets of \(A\). Consequently there are at most \(m\) nonstationary updates. An unchanged update is a fixed point, so the process cannot resume changing afterward.
Completeness: Correct. At stabilization, the fixed-point equations give exactly the two labelling equivalences. Together with disjointness and the complementary undecided set, they define a complete labelling.
Leastness: Correct. The induction applies completeness of the arbitrary comparison labelling separately to each update rule. It establishes both \(I_*\subseteq I_\ell\) and \(O_*\subseteq O_\ell\) for every complete labelling. Identifying the resulting least complete labelling as grounded is consistent with grounded semantics.
The prover correctly distinguishes inclusion from strict inclusion.
The displayed formula for the in-set follows directly from the complete-labelling equivalence. Thus two complete labellings with the same out-set have the same in-set and the same complementary undecided set. They must be identical.
Accordingly, the already established inclusion becomes strict whenever \(\ell\ne g\). This step justifies the strictness needed for Pareto dominance; it does not merely appeal to an ambiguous “minimal out-set” property.
Weak improvement for every supported type: Correct. Out-set inclusion persists after intersection with each \(A_t\), and negating the resulting cardinalities gives the claimed utility inequality.
Strict improvement for some supported type: Correct. Strict out-set inclusion supplies an argument newly rejected by \(\ell\). Coverage ensures that this argument belongs to at least one supported type. For that type, intersection inclusion is strict. Since the sets are finite, their cardinalities differ strictly.
Pareto optimality of \(g\): Correct. Every complete labelling has utility at most that of \(g\) for every supported type, so none can strictly improve any supported type while satisfying the dominance conditions.
Uniqueness: Correct. Every other complete labelling is dominated by \(g\), and \(g\) itself is undominated.
The treatment of overlapping sets, empty individual sets, and masses is also correct. Overlap does not invalidate intersection inclusion; empty sets contribute zero utility; and masses do not occur in the specified dominance definition.
The per-update bound \(O(m+q)\) is justified by scanning arguments and attacks to evaluate the two update predicates. The iteration count gives \(O((m+1)(m+q))\) graph operations, and \(q\leq m^2\) makes this polynomial.
Accounting for reading the support and binary rational masses adds polynomial cost in \(L\). No expansion into a population proportional to mass denominators is used. The singleton output contains only \(m\) labels, so output size presents no enumeration obstacle.
The construction also covers unattacked arguments, self-attacks, and cyclic frameworks through the same update rules. If \(A\) is empty, it immediately produces the unique empty labelling; the strict-dominance argument is then vacuous because there is no distinct complete labelling.
The claimed agreement with Theorem 3 and Corollary 1 is accurate: those results state grounded dominance and the corresponding Pareto characterization for rejection-minimising populations. [Rahwan–Larson (2008)](https://cdn.aaai.org/AAAI/2008/AAAI08-024.pdf)
The prover supplies an independent proof for the specified support formulation, rather than relying on an unverified transfer from finite populations. It therefore resolves the assigned computation question in full.
Required repair or clarification: None.
⟨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.