← back to the atlas

d4-journals-jair-2024-0058 (d4-journals-jair-2024-0058)

Answer: \(\mathrm{NP}\)-hard; more precisely, \(\#\!\cdot\!\mathrm{NP}\)-complete under parsimonious reductions.

The anchor (named result in the paper)

Theorem 7(1) — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximate#PCredS is (1) # · NP-complete via parsimonious reductions if S ∈{stable, admissible, complete}, and (2) # · ΣP 2 -complete via parsimonious reductions if S ∈{stage, semi-stable}. Similarly, one can introduce problems of the form #SkepS and #PSkepS corresponding to the counting versions of the skeptical reasoning problem. As skeptical is dual to credulous reasoning, one easily obtains completeness results for the dual counting classes.

statement extracted from the paper’s text layer; consult the paper for the exact wording

The continuous mirror question, as graded

Given a finite set of supported argument types \(T\), a type-uniform attack relation \(R\subseteq T\times T\), a rational distribution \(\mu\) with \(\mu_t>0\) and \(\sum_{t\in T}\mu_t=1\), a target type \(c^\star\), and a projection \(P\subseteq T\), count the distinct projected mass profiles \((q_t)_{t\in P}\) induced by stable sets \(S\subseteq T\) containing \(c^\star\), where \(S\) is conflict-free, attacks every type outside \(S\), and \(q_t=\mu_t\) for \(t\in S\) and \(q_t=0\) otherwise.

Packaged proof task (what the prover saw — nothing else)

A society is given by its support: a nonempty list \(T\) of \(\tau\) argument types, each with positive binary rational mass \(\mu_t\), with \(\sum_{t\in T}\mu_t=1\). Here \(\tau=|T|\) is the support size, not the number of possible types.
The input also specifies an explicit type-uniform attack relation \(R\subseteq T\times T\) (self-attacks allowed), a target \(c^\star\in T\), and a projection \(P\subseteq T\), possibly empty. Let \(m=|R|\) and \(L\) be the total input bit length; state running times in \(m,\tau,L\).
A feasible selection is a stable extension \(S\subseteq T\) containing \(c^\star\): \((S\times S)\cap R=\varnothing\), and every \(t\in T\setminus S\) has an attacker \(s\in S\) with \((s,t)\in R\). Each type is selected with its entire mass or omitted.
Its projected mass profile has \(q_t=\mu_t\) if \(t\in S\), and \(q_t=0\) otherwise, for \(t\in P\). Compute the exact number of distinct such profiles, counting identical profiles only once.

Is this exact counting problem solvable in polynomial time in \(m,\tau,L\), or is it \(\mathrm{NP}\)-hard?

For finite argumentation frameworks, counting distinct projections of stable extensions containing a designated argument is \(\#\!\cdot\!\mathrm{NP}\)-complete under parsimonious reductions. [Source](https://arxiv.org/pdf/1811.11501).

Modeling choices made when packaging the task

Prover output (gpt-6.1-sol / high, Bolzano prover prompt)

1. Profiles are exactly projected subsets

The problem is \(\mathrm{NP}\)-hard, even when \(P=\varnothing\). More precisely, it is \(\#\!\cdot\!\mathrm{NP}\)-complete under parsimonious reductions.

For an input instance \(I\), define
\[ \mathcal E(I)=\{S\subseteq T:c^\star\in S,\ (S\times S)\cap R=\varnothing,\ \text{every }t\in T\setminus S\text{ is attacked by }S\}. \]
Here and below, “attacked by \(S\)” means that some \(s\in S\) satisfies \((s,t)\in R\).

For any \(S,S'\in\mathcal E(I)\), their projected profiles satisfy
\[ q(S)=q(S')\quad\Longleftrightarrow\quad S\cap P=S'\cap P. \]
Indeed, for each \(t\in P\), the coordinate \(q_t(S)\) is either \(0\) or \(\mu_t\). Because \(\mu_t>0\), these two values are distinct and reveal whether \(t\in S\).

Consequently, the required count is exactly
\[ F(I)=\bigl|\{S\cap P:S\in\mathcal E(I)\}\bigr|. \]
In particular, equal masses assigned to different types cause no collisions: the profile retains its type-indexed coordinates.

2. Valid masses can be assigned with polynomial encoding size

Any nonempty finite argumentation framework can be made into a society without changing its stable extensions.

Let its argument set be \(T=\{t_1,\ldots,t_\tau\}\), and put \(k=\lceil\log_2\tau\rceil\). Assign
\[ \mu_{t_i}=2^{-k}\quad(1\leq i<\tau), \qquad \mu_{t_\tau}=\frac{2^k-\tau+1}{2^k}. \]
The final numerator is positive because \(2^k\geq\tau\), and
\[ \sum_{i=1}^{\tau}\mu_{t_i} =\frac{\tau-1+2^k-\tau+1}{2^k}=1. \]
This also covers \(\tau=1\), giving its sole type mass \(1\).

Each mass has \(O(\log(\tau+1))\) encoding bits. These masses are dyadic, so the construction works even if “binary rational” requires a terminating binary expansion.

Thus, for an explicitly indexed framework of bit length \(B\), adding the masses takes \(O(\tau\log(\tau+1))\) bit operations and produces an instance of length
\[ L=O\bigl(B+\tau\log(\tau+1)\bigr). \]
The attack count \(m\) and support size \(\tau\) remain unchanged.

3. Direct proof of NP-hardness, including empty projection

We give a reduction from CNF satisfiability. Let \(\varphi\) have variables \(x_1,\ldots,x_n\) and clauses \(C_1,\ldots,C_r\).

Create the types
\[ T=\{c^\star\}\cup\{x_i,\bar x_i:1\leq i\leq n\}\cup\{d_j:1\leq j\leq r\}. \]
The attack relation consists of:

There are no other attacks. Assign the masses from Section 2 and take \(P=\varnothing\).

We prove that stable extensions correspond bijectively to satisfying assignments.

From extensions to assignments. Let \(S\) be stable.

First, \(c^\star\in S\): otherwise stability would require an attacker of \(c^\star\), but none exists. Each \(d_j\notin S\), because its self-attack would violate conflict-freeness.

For each variable, at most one of \(x_i,\bar x_i\) lies in \(S\), because they attack each other. At least one lies in \(S\): if both were omitted, neither would have an attacker in \(S\), since their only incoming attacks are from each other. Hence exactly one is selected.

Define \(x_i\) to be true exactly when \(x_i\in S\). Every omitted clause type \(d_j\) must be attacked by \(S\). Its self-attacker is omitted, so a selected literal occurring in \(C_j\) must attack it. That literal is true under the assignment. Thus every clause is satisfied.

From assignments to extensions. Given a satisfying assignment, select \(c^\star\) and exactly the true literal type for each variable. This set is conflict-free: it contains no clause types and never contains both members of a literal pair. Every omitted literal is attacked by its selected opposite. Every clause type is attacked by a selected literal because the clause is satisfied. Therefore the set is stable.

These constructions are inverse to each other.

With \(P=\varnothing\), every feasible selection has the same empty profile. Hence
\[ F(I_\varphi)= \begin{cases} 1,&\text{if }\varphi\text{ is satisfiable},\\ 0,&\text{otherwise}. \end{cases} \]
An exact counting algorithm would therefore decide CNF satisfiability by testing whether its output is positive.

If \(h\) denotes the number of distinct literal–clause incidences, this construction has
\[ \tau=2n+r+1,\qquad m=2n+r+h, \]
and output length \(L=O((m+\tau)\log(\tau+1))\). Its construction time is polynomial in the formula’s input length and output length. Thus a running time polynomial in \(m,\tau,L\) would imply \(\mathrm P=\mathrm{NP}\).

4. Exact counting classification and an upper bound

The cited theorem states that counting distinct projected stable extensions containing a designated argument is \(\#\!\cdot\!\mathrm{NP}\)-complete under parsimonious reductions. Its definition matches the projected-subset count in Section 1. [Fichte, Hecher and Meier, Theorem 7](https://arxiv.org/pdf/1811.11501)

Section 2 gives a polynomial-time, count-preserving reduction from that problem to the society problem: retain the framework, target, and projection, and add valid positive masses. This proves \(\#\!\cdot\!\mathrm{NP}\)-hardness.

For membership, fix an ordering of \(P\). A counted object is a bit vector representing \(U\subseteq P\). Whether it should be counted is the predicate
\[ \exists S\subseteq T: \quad S\cap P=U,\quad c^\star\in S,\quad S\text{ is stable}. \]
This predicate is in \(\mathrm{NP}\). Given \(S\), mark all targets attacked by selected types while scanning \(R\); simultaneously reject any attack whose endpoints are both selected. Then check that every omitted type is marked, that \(c^\star\) is selected, and that the projection equals \(U\). Verification takes \(O(m+\tau)\) operations after reading the input.

Counting distinct polynomial-length objects satisfying an \(\mathrm{NP}\) predicate is precisely membership in \(\#\!\cdot\!\mathrm{NP}\). This proves completeness.

For an explicit exponential upper bound, enumerate every \(U\subseteq P\), and then enumerate its completions in \(T\setminus P\), counting \(U\) once if any completion is feasible. Across all \(U\), there are at most \(2^\tau\) candidate selections. The running time is
\[ O\bigl(L+2^\tau(m+\tau)\bigr) \]
in the usual indexed word-RAM model, including the counter updates. A conservative bit-operation bound is \(O(L+2^\tau(m+\tau)L)\). The answer is at most \(2^{|P|}\), so its binary output uses at most \(|P|+1\) bits.

The target question is therefore resolved: the exact counting problem is \(\mathrm{NP}\)-hard, and no polynomial-time algorithm in \(m,\tau,L\) exists unless \(\mathrm P=\mathrm{NP}\).

⟨structured verdict parsed — rendered above⟩

Adversarial review (gpt-6.1-sol / medium, Bolzano verifier prompt)

The prover resolves the task correctly. The direct reduction establishes \(\mathrm{NP}\)-hardness even with empty projection, and the cited theorem supports the stronger completeness claim for unrestricted projections. I found no major or minor mathematical issues.

The equivalence
\[ q(S)=q(S')\quad\Longleftrightarrow\quad S\cap P=S'\cap P \]
is correct. Each coordinate is indexed by its type, and positivity of \(\mu_t\) distinguishes selection from omission. Equal masses on different types therefore introduce no additional identifications.

The family \(\mathcal E(I)\) includes precisely the feasibility requirements in the task: target containment, conflict-freeness, and an attack from a selected type to every omitted type. Thus the expression for \(F(I)\) counts exactly the requested profiles.

When \(P=\varnothing\), this gives one profile if any feasible selection exists and zero otherwise. The prover correctly distinguishes these cases.

With \(k=\lceil\log_2\tau\rceil\), the numerator \(2^k-\tau+1\) is positive. The displayed sum evaluates to one, so all assigned masses satisfy the input requirements.

The construction also handles \(\tau=1\): \(k=0\), the first group of assignments is empty, and the sole mass is one. Both numerators and denominators have \(O(\log(\tau+1))\) bits. The dyadic construction meets either the ordinary binary encoding of rational numbers or a requirement for terminating binary expansions.

Adding these masses does not alter the attack relation or feasible subsets. Consequently, it preserves the projected count. The stated construction time and output-length bound are valid for explicitly indexed frameworks.

The constructed framework is nonempty because it contains \(c^\star\). Its self-attacks are permitted by the task.

Every step in the extension-to-assignment direction is justified:

The assignment-to-extension direction is also correct. The proposed selection has no internal attacks. Every omitted literal is attacked by its selected opposite, and every clause type is attacked by a selected satisfying literal. These checks cover every omitted type.

The two constructions are inverse: every stable extension contains exactly the target and the literal types determined by its assignment. The claimed bijection is therefore established.

Empty clauses, repeated literals, tautological clauses, and formulas with no clauses do not invalidate the argument. An empty clause leaves its clause type without a possible selected attacker; repeated occurrences do not change the attack relation; the other cases follow from the same stated checks.

With empty projection, the displayed output is exactly the satisfiability indicator. Testing whether the count is positive therefore decides CNF satisfiability using one evaluation of the counting function.

The counts
\[ \tau=2n+r+1,\qquad m=2n+r+h \]
are correct when \(h\) counts distinct literal–clause incidences. The stated indexed encoding size and polynomial construction time are sufficient for the reduction.

Thus a counting algorithm polynomial in \(m,\tau,L\) would decide CNF satisfiability in polynomial time. The conditional conclusion concerning \(\mathrm P=\mathrm{NP}\) follows. This establishes computational hardness of the counting function; it does not assert that the empty-projection restriction is itself complete for the stronger counting class.

The citation is accurate. Theorem 7 states parsimonious \(\#\!\cdot\!\mathrm{NP}\)-completeness for projected credulous counting under stable semantics. The paper defines the counted objects as distinct intersections with the projection set among extensions containing the designated argument. Its frameworks are finite and nonempty, and its attack relation allows the relations used here. These hypotheses match the reduction. [Fichte, Hecher and Meier, definitions and Theorem 7](https://arxiv.org/pdf/1811.11501)

Retaining the framework, target, and projection while adding valid masses is polynomial and preserves the count by the profile equivalence already established. The claimed parsimonious hardness transfer is justified.

A fixed ordering of \(P\) gives each projected subset exactly one bit-vector representation. This avoids counting multiple representations of the same object.

The existential predicate correctly asks whether that projected subset has a feasible completion. The certificate \(S\) has polynomial length. Scanning the attacks detects internal conflicts and marks attacked types; the remaining checks enforce stability, target containment, and the prescribed projection.

The stated \(O(m+\tau)\) verification bound is valid in the indexed word-RAM model after input reading. Counting these distinct polynomial-length objects with an \(\mathrm{NP}\) membership predicate establishes the claimed class membership.

Every subset of \(T\) has exactly one decomposition into its projection and its completion. Accordingly, the nested enumeration examines at most \(2^\tau\) candidate selections and counts each feasible projected subset once.

The stated word-RAM and conservative bit-operation bounds are consistent with generating candidates, checking feasibility, and maintaining the count. There are at most \(2^{|P|}\) profiles, so \(|P|+1\) bits suffice for the binary answer, including the empty-projection case.

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.