Answer: \(\mathrm{NP}\text{-complete}\), already for \(\tau=1\) with all arguments and attacks certain and only supports uncertain.
Theorem 2 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateOver s-iBAFs, IBVERσ is NP-complete under σ ∈ {s-ad, d-co, s-co, d-gr, s-gr}.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a common argument vocabulary \(U\), a finite support of \(s\)-iBAF types \(IF_t\) over \(U\), binary-rational masses \(\mu_t\) summing to \(1\), a set \(S\) of arguments certain in every type, and a rational threshold \(q\), decide whether \(W \ge q\), where \(W=\sum_{t:\,\exists\text{ completion of }IF_t\text{ in which }S\text{ is an }s\text{-ad extension}}\mu_t\).
Let \(U\) be a finite argument vocabulary, with \(m=|U|\). A society is given by its support: a list of \(\tau\) types with positive binary-rational masses \(\mu_t\) summing to \(1\). Here \(\tau\) is the support size, not the number of possible types. Let \(L\) be the total input bit length; state running times in \(m,\tau,L\).
Each type is an explicitly encoded incomplete bipolar framework \(IF_t=(A_t,A_t^{?},R_{a,t},R_{a,t}^{?},R_{s,t},R_{s,t}^{?})\). The certain and uncertain argument sets are disjoint subsets of \(U\); attack relations and support relations are subsets of \((A_t\cup A_t^{?})^2\), with the certain and uncertain relations disjoint within each category. Self-loops are allowed.
A completion selects \(A_t\subseteq B\subseteq A_t\cup A_t^{?}\), retains every certain attack and support whose endpoints lie in \(B\), and independently selects any subset of the uncertain attacks and supports with endpoints in \(B\). Write the resulting framework as \((B,R_a,R_s)\).
In a completion, \(x\Rightarrow^{+}y\) means a support path of positive length. A generic attack \(x\leadsto y\) exists exactly when \((x,y)\in R_a\), or some \(z\in B\) satisfies \(x\Rightarrow^{+}z\) and \((z,y)\in R_a\). No other implicit attacks are used.
A set \(S\subseteq B\) is safe if there is no \(y\in B\) such that some member of \(S\) generically attacks \(y\) and either \(y\in S\) or some member of \(S\) transitively supports \(y\). It is an \(s\text{-ad}\) extension if it is safe and, for every \(x\in S\) and \(y\in B\) with \(y\leadsto x\), some \(z\in S\) satisfies \(z\leadsto y\).
Given \(S\subseteq\bigcap_{t=1}^{\tau}A_t\) and a binary-rational threshold \(q\in\mathbb{Q}\), define \(W=\sum_{t:\,\exists\text{ completion of }IF_t\text{ in which }S\text{ is an }s\text{-ad}\text{ extension}}\mu_t\). Completions are chosen separately for each type; the decision problem asks whether \(W\ge q\).
Is this weighted possible-extension decision problem solvable in polynomial time, or is it NP-hard?
For a single incomplete framework with these support and extension semantics, possible-extension verification is NP-complete, even when all arguments and attacks are certain and only supports may be uncertain.
The weighted possible-extension decision problem is \( \mathrm{NP} \)-complete. Hardness already holds for \( \tau=1 \), with all arguments and attacks certain and only supports uncertain. Thus a polynomial-time algorithm exists if and only if \( \mathrm{P}=\mathrm{NP} \).
Fix a type and a completion \( (B,R_a,R_s) \). We first show that verifying whether the given \( S \) is an \( s\text{-ad} \) extension takes polynomial time.
Let \( P(x,y) \) mean that there is a support path of positive length from \( x \) to \( y \). Compute \( P \) by transitive closure of \( R_s \), initializing the closure with \( R_s \), without automatically adding identity pairs. Consequently, \( P(x,x) \) holds precisely when a positive-length support cycle passes through \( x \). This computation takes \( O(m^3) \) Boolean operations.
Construct the generic-attack relation \( G \) by setting, for each \( x,y\in B \),
\( G(x,y)=R_a(x,y)\lor\bigvee_{z\in B}\bigl(P(x,z)\land R_a(z,y)\bigr). \)
This is exactly the generic-attack definition in the question and takes \( O(m^3) \) Boolean operations.
For each \( y\in B \), define
\( D(y)=\bigvee_{z\in S}G(z,y) \)
and
\( H(y)=(y\in S)\lor\bigvee_{z\in S}P(z,y). \)
By the stated definition of safety, \( S \) is safe exactly when no \( y\in B \) satisfies both \( D(y) \) and \( H(y) \).
The defense condition holds exactly when, for every \( x\in S \) and \( y\in B \), \( G(y,x) \) implies \( D(y) \). Indeed, \( D(y) \) states precisely that some member of \( S \) generically attacks \( y \).
Computing these predicates and checking both conditions takes \( O(m^2) \) further Boolean operations. Therefore a specified completion can be verified in \( O(m^3) \) Boolean operations. Its validity as a completion is also checked directly against the input: certain arguments must be present, selected arguments and relations must be permitted, and all certain relations whose endpoints are present must be retained.
For an input instance, let \( T^\star \) be the set of types that admit a completion in which \( S \) is an \( s\text{-ad} \) extension. Thus \( W=\sum_{t\in T^\star}\mu_t \).
A certificate consists of:
A completion is encoded by one selection bit for each uncertain argument, attack, and support. Certain components are determined by the input and the selected arguments. Because every uncertain component is explicitly encoded in the input, the total certificate length is \( O(L) \).
The verifier checks every supplied completion using Section 1 and accepts exactly when all checks pass and \( \sum_{t\in J}\mu_t\ge q \).
Soundness. Every verified type belongs to \( T^\star \), so \( J\subseteq T^\star \). Since all masses are positive, \( \sum_{t\in J}\mu_t\le W \). Acceptance therefore implies \( W\ge q \).
Completeness. If \( W\ge q \), choose \( J=T^\star \) and supply a witnessing completion for each of its types. This certificate passes every check and its mass sum equals \( W \).
The graph computations require \( O(\tau m^3) \) Boolean operations. Exact rational arithmetic is polynomial as well: using a product of the input denominators as a common denominator requires only \( O(L) \) bits. Schoolbook arithmetic gives an \( O(\tau L^2) \) bit-operation bound for summation and comparison. Thus verification uses \( O(\tau m^3+L) \) graph and input-processing operations, plus \( O(\tau L^2) \) arithmetic bit operations.
This proves membership in \( \mathrm{NP} \).
Use the single-framework \( \mathrm{NP} \)-completeness result supplied in the question, restricted to instances with all arguments and attacks certain and only supports uncertain.
Given such an instance \( (IF,S) \), construct a society with:
Keep the same vocabulary and candidate set \( S \). Because all arguments are certain, the requirement \( S\subseteq A_1 \) is satisfied.
If the original instance admits a completion making \( S \) an \( s\text{-ad} \) extension, then \( W=1 \). Otherwise \( W=0 \). Hence \( W\ge q \) holds exactly when the original possible-extension instance is positive.
The construction copies the original instance and adds constant-size data, so it takes \( O(L) \) time. It is a polynomial-time many-one reduction, proving \( \mathrm{NP} \)-hardness under the stated restrictions.
Together with Section 2, this establishes \( \mathrm{NP} \)-completeness.
⟨structured verdict parsed — rendered above⟩
The prover resolves the task correctly: the weighted possible-extension decision problem is \( \mathrm{NP} \)-complete, already with one type, all arguments and attacks certain, and only supports uncertain. No major or minor issues were found.
Positive-length support reachability. Initializing transitive closure with \( R_s \), without inserting identity pairs, correctly computes positive-length reachability. In particular, \( P(x,x) \) holds exactly when a positive-length support cycle passes through \( x \). This handles self-loops and longer cycles consistently with the task. The stated \( O(m^3) \) Boolean-operation bound is valid.
Generic attacks. The formula
\[
G(x,y)=R_a(x,y)\lor\bigvee_{z\in B}\bigl(P(x,z)\land R_a(z,y)\bigr)
\]
matches the task exactly. It includes direct attacks and attacks preceded by a positive-length support path, without introducing any other implicit attacks. Its computation takes \( O(m^3) \) Boolean operations.
Safety. The predicates \( D(y) \) and \( H(y) \) correctly express, respectively, that some member of \( S \) generically attacks \( y \), and that \( y \) belongs to \( S \) or is positively transitively supported by some member of \( S \). Thus excluding every \( y\in B \) with both predicates true is precisely the required safety condition. The existential witnesses for attack and support may be different members of \( S \), as the definition allows.
Defense. Requiring \( G(y,x)\Rightarrow D(y) \) for every \( x\in S \) and \( y\in B \) exactly matches the defense condition. The defending member of \( S \) may depend on the attacker; the formulation imposes no stronger quantifier requirement.
Completion validity. The listed validity checks enforce the permitted argument set, permitted relations, and retention of every certain relation whose endpoints are selected. They agree with the completion semantics. Uncertain relations with absent endpoints cannot appear in the resulting framework.
The additional predicate computations and checks take \( O(m^2) \) Boolean operations. The overall polynomial verification claim is correct.
Certificate size. A subset of the explicitly listed types, together with selection bits for their explicitly encoded uncertain components, has size \( O(L) \). Encoding the subset requires at most \( O(\tau) \) additional bits, which is also \( O(L) \). Certain components need not be included separately.
Soundness. Every successfully verified type belongs to \( T^\star \). Positivity of the masses therefore gives
\[
\sum_{t\in J}\mu_t\le W.
\]
Consequently, certificate acceptance implies \( W\ge q \). No claim about unwitnessed types is needed.
Completeness. If \( W\ge q \), the finite set \( J=T^\star \) admits one witnessing completion per type. These witnesses jointly form a polynomial-size certificate because the types are explicitly listed and completions are chosen independently.
Exact arithmetic. The product of the input denominators has bit length bounded by their aggregate input length, hence \( O(L) \). Including the threshold denominator preserves this bound. Numerators and intermediate sums also have polynomial, indeed \( O(L) \), bit length under the stated positive, normalized mass assumptions. The claimed \( O(\tau L^2) \) schoolbook-arithmetic bound is sufficient for exact summation and comparison.
Thus the stated verification bounds are polynomial in \( m,\tau,L \).
The prover invokes the single-framework \( \mathrm{NP} \)-completeness result expressly supplied by the task, with the same support and extension semantics and the required restriction to certain arguments and attacks.
The construction uses \( \tau=1 \), copies the framework and candidate set, and sets \( \mu_1=q=1 \). It satisfies all target-instance requirements:
The resulting weight is \( 1 \) exactly when a witnessing completion exists, and \( 0 \) otherwise. Hence the reduction preserves yes and no instances. Copying the input and adding constant-size data takes \( O(L) \) time.
The hardness conclusion and its combination with membership in \( \mathrm{NP} \) are valid.
Empty candidate sets, support cycles, and self-loops are covered by the written predicates. Arbitrary rational thresholds cause no gap: the existing soundness and completeness arguments also cover \( q\le0 \) and \( q>1 \), including certificates with \( J=\varnothing \).
The statement that a polynomial-time algorithm exists if and only if \( \mathrm{P}=\mathrm{NP} \) follows from the established \( \mathrm{NP} \)-completeness.
No additional lemma, 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.