Answer: \(\mathrm{NP}\)-hard; explicitly listed clause contexts also preclude polynomial worst-case total running time.
Theorem 4 (Guarantee of finding an explanation) — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateIf there exists at least one abductive explanation h of S i<n Oi wrt S i<n Ti and A, and both termination of local interactions and temporal connex- ity are guaranteed, then the MAS will eventually stabilize in a state in which all agents share such an explanation (i.e. a group-explanation wrt the MAS that respects the bias A). Proof By contradiction, let us suppose the MAS stabilizes on a partial hypothesis.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite role set \(R\) with positive rational masses \(\mu_r\) summing to \(1\), role theories \(T_r\), grounded observations \(O_r\), common abducibles \(A\) and preference order, a connected role graph, and a fair periodic schedule of pairwise cohort interactions, compute a finite legal interaction trace ending in a common ground hypothesis \(h\) that is an abductive explanation of \((\bigcup_{r\in R}T_r,\bigcup_{r\in R}O_r)\) and respects \(A\), under the paper’s consistency, termination, and explanation-existence promises.
A society is given by its support: a list of \(\tau=|R|\) roles with positive binary-rational masses \(\mu_r\), summing to \(1\). Each role is a homogeneous cohort with one shared state; interactions update entire cohorts without splitting or transferring mass. The support size \(\tau\) is not the number of possible types.
Each role has a finite first-order clausal theory \(T_r\) and finite ground observations \(O_r\). All share a finite signature with \(m\) symbols, finite literal templates \(A\), and a total preference order on finite ground hypotheses, given by a polynomial-time comparison algorithm; fully abducible hypotheses precede partial ones. Both positive and negative literals are permitted, and abducibility means being a ground instance of a template in \(A\).
Write \(T=\bigcup_r T_r\) and \(O=\bigcup_r O_r\). An explanation is a finite ground hypothesis \(h\) satisfying \(T\cup h\models O\), \(T\cup h\not\models\bot\), and the abducibility condition. Local hypothesis generation selects preferred inclusion-minimal explanations, permitting arbitrary ground literals when no fully abducible local explanation exists.
For a theory \(S\), let \(\operatorname{Carc}(S)\) be its subsumption-minimal clause consequences over the common signature, identifying mutually subsuming clauses, and let \(N(S,U)=\operatorname{Carc}(S\cup U)\setminus\operatorname{Carc}(S)\). Negating a hypothesis means the clause \(\neg h=\bigvee_{\ell\in h}\neg\ell\).
The input includes a connected undirected role graph and an explicit period of \(q\) ordered adjacent pairs covering both orientations of every edge. Repeat this period; a designated learner initiates an interaction when its hypothesis or context differs from its last accepted state with that neighbour. Initially, hypotheses are locally generated, contexts are uncached, and every neighbour requires an initial interaction.
For learner \(a\), critic \(b\), and proposal \(h\), initialize \(C_0=N(T_a,h)\) or retrieve its cached context. Merge the critic's cached context for \(h\) into \(C_0\), then alternately compute \(C_i=N(T_{\alpha_i},C_{i-1})\), where \(\alpha_i=b\) for odd \(i\) and \(a\) for even \(i\). A contradiction rejects \(h\): both add \(\neg h\) to their theories and the learner proposes its next hypothesis.
Otherwise stop when \(C_i\subseteq C_{i-1}\), or, for \(i\geq2\), \(C_i\subseteq C_{i-2}\). Both cache \(C_i\cap C_{i-1}\); add \(C_i\setminus C_{i-1}\) to the other participant's theory and \(C_{i-2}\setminus C_{i-1}\) to the current participant's theory, omitting the latter update when \(i=1\).
Next, the critic sends each observation \(o\) not entailed by \(T_b\cup h\). If \(T_a\cup h\not\models o\), the learner adds \(o\) to its observations and regenerates a hypothesis. Otherwise it sends some \(p\subseteq h\) with \(T_a\cup p\models o\), and the critic adds \(o\vee\neg p\) to its theory. Recheck accountability until all critic observations are explained.
A critic holding a preferred hypothesis reverses roles and proposes it. Otherwise, a partial proposal is temporarily blocked by both participants while they seek another proposal, reversing roles if necessary. When alternatives are exhausted, restore temporary blocks and adopt the best surviving proposal; an acceptable fully abducible proposal may be adopted immediately. Retain learned clauses, observations, and cached contexts between interactions.
Promise that \(T\cup O\) is consistent, \(\operatorname{Carc}(T)\) is finite, all invoked local reasoning computations and bilateral interactions terminate, and a global abductive explanation exists. The required object is an explicit finite legal trace ending in a stable common hypothesis and context, with the hypothesis a global abductive explanation. Let \(L\) be the total input bit length; charge for local logical computation and every written trace symbol.
Can this promised trace-construction problem be solved in time polynomial in \(m,\tau,L,q\), or is it \(\mathrm{NP}\)-hard?
For finite discrete societies, [the convergence and explanation guarantee](https://doi.org/10.3233/978-1-60750-606-5-901) establishes eventual stabilization under these qualitative promises, without a polynomial-time bound. [A subsequent protocol study](https://ceur-ws.org/Vol-627/lads_5.pdf) investigates efficiency improvements experimentally; no result settling this exact mass-cohort trace problem was located.
The problem is \(\mathrm{NP}\)-hard, already with two identical roles, equal masses, a period of length two, and propositional theories.
Moreover, when the required trace explicitly lists its clause contexts, there is an unconditional obstruction to polynomial total running time: some promised instances force an exponentially large final context.
The hardness statement uses the following precise meaning for this search problem: a polynomial-time transformation maps every CNF formula to a promised instance, and a polynomial-time readout from every valid output determines whether that formula is satisfiable.
Let \(\varphi=\bigwedge_{j=1}^{k}D_j\) be a CNF formula over propositional atoms \(x_1,\ldots,x_n\). Introduce fresh atoms \(s,d,g\), and define
\[ S_\varphi= \{\neg s\vee D_j:1\leq j\leq k\} \cup \{\neg s\vee g,\ \neg d\vee g\}. \]
Use the propositional subcase of first-order logic: these atoms are nullary predicates, with no function symbols or equality.
Construct two roles \(a,b\) with
\[ T_a=T_b=S_\varphi,\qquad O_a=O_b=\{g\},\qquad \mu_a=\mu_b=\tfrac12. \]
The role graph is the single edge joining \(a\) and \(b\), and its period is \(((a,b),(b,a))\). Thus \(\tau=q=2\). Set the abducible templates to \(A=\{s,d\}\), both positive.
Choose this total preference order:
This comparison algorithm runs in polynomial time and performs no satisfiability computation.
The only fully abducible hypotheses are \(\varnothing,\{s\},\{d\},\{s,d\}\).
The empty hypothesis does not explain \(g\): setting \(s=d=g=\mathrm{false}\) satisfies \(S_\varphi\), regardless of the values of the original atoms.
The hypothesis \(\{d\}\) always explains \(g\), by \(\neg d\vee g\), and is consistent. A witnessing model sets \(s=\mathrm{false}\), \(d=g=\mathrm{true}\), and assigns the original atoms arbitrarily. Hence \(\{d\}\) is inclusion-minimal.
The hypothesis \(\{s\}\) entails \(g\). It is consistent exactly when \(\varphi\) is satisfiable:
Whenever consistent, \(\{s\}\) is inclusion-minimal because the empty hypothesis fails accountability.
Finally, \(\{s,d\}\) is not inclusion-minimal because its proper subset \(\{d\}\) is already an explanation.
Consequently, both roles initially select the same hypothesis \(H_\varphi\), where
\[ H_\varphi= \begin{cases} \{s\},&\text{if }\varphi\text{ is satisfiable},\\ \{d\},&\text{if }\varphi\text{ is unsatisfiable}. \end{cases} \]
Every formula, including an unsatisfiable formula, produces a promised instance.
First, \(T\cup O=S_\varphi\cup\{g\}\) is consistent: use the model with \(s=\mathrm{false}\), \(d=g=\mathrm{true}\).
Second, \(\{d\}\) is always a global abductive explanation.
Third, characteristic clause sets are finite. Over \(m=n+3\) propositional atoms, clauses identified with literal sets have at most \(2^{2m}\) possibilities. Thus entailment, subsumption, characteristic-clause computation, and hypothesis selection can all terminate by finite enumeration. This establishes termination, without asserting efficiency.
The construction has polynomial input length. Bilateral termination and stabilization are verified next directly.
We prove a useful fact about identical roles.
Let \(S\) be their common theory, and suppose their common selected hypothesis is the fully abducible singleton \(\{u\}\). Assume \(S\cup\{u\}\) is consistent and \(S\not\models u\). Define
\[ C=N(S,\{u\}). \]
The unit clause \(u\) belongs to \(\operatorname{Carc}(S\cup\{u\})\): its only proper subclause is the empty clause, which is not entailed because \(S\cup\{u\}\) is consistent. Also, \(u\notin\operatorname{Carc}(S)\), since \(S\not\models u\). Therefore \(u\in C\).
Every clause in \(C\) is entailed by \(S\cup\{u\}\). Conversely, \(u\in C\) implies \(S\cup C\models S\cup\{u\}\). Hence
\[ S\cup C\equiv S\cup\{u\}. \]
Characteristic clauses depend only on logical consequences, so
\[ N(S,C) = \operatorname{Carc}(S\cup C)\setminus\operatorname{Carc}(S) = C. \]
In the first interaction, the learner initializes \(C_0=C\). The critic has no cached context to add and computes \(C_1=N(S,C_0)=C\). Therefore the stopping condition holds at \(i=1\).
Both roles cache \(C_1\cap C_0=C\). The prescribed theory update is empty because \(C_1\setminus C_0=\varnothing\), and the other update is omitted at \(i=1\).
If \(\{u\}\) already explains both roles’ observations, accountability produces no update. The critic holds the same hypothesis, so it has no strictly preferred proposal. The proposal is fully abducible and can be accepted.
Any remaining mandatory interaction has the same calculation: cached contexts merge to \(C\), and \(N(S,C)=C\). After the mandatory interactions, neither hypothesis nor context changes, so the common state is stable.
Apply this argument to the reduction. For either selected atom \(u\in\{s,d\}\), \(S_\varphi\not\models u\), witnessed by setting \(s=d=g=\mathrm{false}\). All other hypotheses of the argument were established above.
Thus every completed legal trace retains \(H_\varphi\), and its terminal hypothesis satisfies
\[ \varphi\text{ is satisfiable} \quad\Longleftrightarrow\quad H_\varphi=\{s\}. \]
CNF satisfiability is \(\mathrm{NP}\)-complete by the standard Cook–Levin theorem. [Cook’s original paper](https://doi.org/10.1145/800157.805047)
Suppose a trace-construction algorithm ran in time polynomial in \(m,\tau,L,q\). Given \(\varphi\), construct the instance above, run that algorithm, and inspect its terminal hypothesis.
The construction is polynomial, every constructed instance satisfies the promises, and the output distinguishes satisfiable from unsatisfiable formulas. Since \(\tau=q=2\) and the remaining parameters are polynomially bounded in the formula’s encoding length, this would decide CNF satisfiability in polynomial time.
Therefore the promised trace-construction problem is \(\mathrm{NP}\)-hard. This argument does not claim membership in \(\mathrm{NP}\).
The explicit-output requirement yields a further obstruction, even for Horn theories.
For each positive integer \(n\), introduce atoms
\[ s,\quad z_0,\ldots,z_n,\quad a_1,\ldots,a_n,\quad b_1,\ldots,b_n. \]
Let
\[ S_n= \{\neg s\vee z_0\} \cup \{\neg z_{i-1}\vee\neg a_i\vee z_i,\ \neg z_{i-1}\vee\neg b_i\vee z_i: 1\leq i\leq n\}. \]
Use two identical roles with theory \(S_n\), observations \(\{z_0\}\), abducibles \(A=\{s\}\), equal masses, and the same two-pair period.
The unique fully abducible inclusion-minimal explanation is \(\{s\}\). Indeed, it consistently entails \(z_0\), whereas the empty hypothesis does not. The preceding identical-role argument shows that the stable common context is
\[ C_n=N(S_n,\{s\}). \]
We now prove that \(C_n\) contains at least \(2^n\) distinct clauses.
For each choice \(c_i\in\{a_i,b_i\}\), define
\[ E_{c_1,\ldots,c_n} = z_n\vee\neg c_1\vee\cdots\vee\neg c_n. \]
In any model of \(S_n\cup\{s\}\), \(z_0\) is true. If every chosen \(c_i\) is true, the corresponding Horn implications successively force \(z_1,\ldots,z_n\) to be true. Otherwise one of the literals \(\neg c_i\) is true.
Thus \(S_n\cup\{s\}\models E_{c_1,\ldots,c_n}\).
In this propositional signature, subsumption is literal-set inclusion. It suffices to show that deleting any one literal destroys entailment.
Deleting \(z_n\) destroys entailment: set \(s\), every \(z_i\), and every \(a_i,b_i\) to true. This satisfies \(S_n\cup\{s\}\), but makes every remaining literal \(\neg c_i\) false.
To delete \(\neg c_j\), use the following valuation:
Before stage \(j\), the required conclusions \(z_i\) are true. At stage \(j\), both antecedents involving \(a_j,b_j\) fail. After stage \(j\), every antecedent involving \(z_{i-1}\) fails. Hence this valuation satisfies \(S_n\cup\{s\}\).
It falsifies the shortened clause: \(z_n\) is false, and every remaining chosen \(c_i\) is true.
Therefore no proper subclause is entailed, establishing subsumption-minimality.
Set \(s\) and every \(z_i\) false, and every \(a_i,b_i\) true. This satisfies \(S_n\) and falsifies every \(E_{c_1,\ldots,c_n}\).
Consequently,
\[ E_{c_1,\ldots,c_n} \in \operatorname{Carc}(S_n\cup\{s\}) \setminus \operatorname{Carc}(S_n). \]
Different choices give different clauses, so \(|C_n|\geq 2^n\).
These instances satisfy all promises: the theories and observations are jointly consistent, \(\{s\}\) is a global explanation, the propositional reasoning spaces are finite, and the bilateral interactions terminate as proved above.
Here \(m=3n+2\), \(\tau=q=2\), and the input length is \(O(n\log(n+1))\) using binary indices. An explicit listing of the final context therefore requires at least \(2^n\) written symbols, which exceeds every polynomial in the input parameters.
The promised problem is \(\mathrm{NP}\)-hard even for two identical homogeneous cohorts. Qualitative termination does not supply a polynomial-time bound.
For traces that explicitly list the prescribed clause contexts, polynomial worst-case total running time is impossible independently of whether \(\mathrm{P}=\mathrm{NP}\), because the required output can already be exponentially large.
⟨structured verdict parsed — rendered above⟩
The prover establishes the claimed \(\mathrm{NP}\)-hardness. The reduction preserves every promise, and its initial hypothesis is forced by the specified preference order. The protocol calculations then show that this hypothesis persists to the terminal state. The additional context-size bound is also correct under its explicitly stated requirement that contexts be listed.
No major or minor mathematical issues were found.
The constructed instance satisfies the structural requirements:
The preference order is admissible. Testing full abducibility, comparing cardinalities, and lexicographically comparing finite literal sets require polynomial time. None requires deciding consistency or entailment.
The transformation has polynomial size: each input clause contributes one guarded clause, and the remaining additions have constant size.
Every case in the classification is correct.
Empty hypothesis. The valuation \(s=d=g=\mathrm{false}\) satisfies every guarded clause, including when an input clause is empty. It falsifies \(g\), so the empty hypothesis does not explain the observation.
Hypothesis \(\{d\}\). The clause \(\neg d\vee g\) establishes entailment of \(g\). The supplied valuation with \(s=\mathrm{false}\) and \(d=g=\mathrm{true}\) establishes consistency independently of the satisfiability of \(\varphi\). Its only proper subset is the empty hypothesis, so inclusion-minimality follows.
Hypothesis \(\{s\}\). Setting \(s\) true forces every clause \(D_j\), as well as \(g\). Conversely, every satisfying assignment of \(\varphi\) extends as specified. Thus consistency holds exactly when \(\varphi\) is satisfiable. Whenever consistent, this hypothesis is inclusion-minimal.
Hypothesis \(\{s,d\}\). Whenever it is an explanation, its proper subset \(\{d\}\) is already an explanation. It therefore cannot be inclusion-minimal.
Consequently, the preferred local explanation is uniquely \(\{s\}\) in the satisfiable case and uniquely \(\{d\}\) in the unsatisfiable case. Partial explanations cannot interfere, because a fully abducible local explanation always exists.
The reasoning also covers a formula with no clauses, unused variables, and formulas containing empty clauses.
The promise checks are valid.
Joint consistency. The supplied model satisfies \(S_\varphi\cup\{g\}\), regardless of \(\varphi\).
Global explanation. Since both roles have identical theories and observations, the established explanation \(\{d\}\) is also a global abductive explanation.
Finite characteristic clause set. In this nullary, function-free, equality-free signature, clauses are represented by subsets of the \(2m\) literals. The bound \(2^{2m}\) is therefore a valid upper bound, even allowing tautological clauses. Identifying mutually subsuming clauses cannot increase it.
Termination of local reasoning. There are finitely many propositional valuations, clauses, and hypotheses. Finite enumeration consequently provides terminating procedures for the invoked reasoning tasks. This establishes termination without assuming polynomial cost.
Termination of bilateral interactions. This is supplied by the explicit calculation in Section 2, checked next.
No convergence theorem needs to be invoked for these instances.
The identical-role calculation is correct for the propositional instances used in both constructions.
Because \(S\cup\{u\}\) is consistent, the empty clause is not a consequence. In this propositional setting, it is the only proper subclause of the unit clause \(u\). Hence \(u\) is subsumption-minimal among consequences of \(S\cup\{u\}\).
Because \(S\not\models u\), this unit clause is absent from \(\operatorname{Carc}(S)\). Thus \(u\in C=N(S,\{u\})\).
Both directions of the claimed equivalence are justified:
Therefore \(S\cup C\equiv S\cup\{u\}\), and taking the same characteristic-clause difference gives \(N(S,C)=C\).
The protocol consequences follow exactly as written:
Subsequent mandatory interactions have the same context and produce no changes. Once both ordered pairs have been processed, the accepted states agree with the unchanged current states.
For the reduction, the supplied valuation verifies \(S_\varphi\not\models s\) and \(S_\varphi\not\models d\). Thus all hypotheses of this calculation hold. There is no rejection, observation-driven regeneration, or preference-driven replacement that could alter the selected hypothesis.
Accordingly, every completed legal trace has the claimed terminal hypothesis.
The reduction uses the precise search-hardness interpretation stated by the prover: a polynomial-time construction of promised instances, with a readout that succeeds for every valid output.
The source problem is unrestricted CNF satisfiability, which is \(\mathrm{NP}\)-complete. This is the standard Cook–Levin result used here; the cited original paper supplies the foundational polynomial reduction result. [Cook’s paper](https://www.cs.toronto.edu/~sacook/homepage/1971.pdf)
A polynomial-time trace constructor would produce a polynomial-length output, because written symbols are charged. Inspecting its terminal hypothesis would then decide whether \(\varphi\) is satisfiable.
The constructed parameters satisfy \(\tau=q=2\), with \(m\) and \(L\) polynomially bounded by the source encoding length. The polynomial-time implication therefore follows.
This proves the stated \(\mathrm{NP}\)-hardness. It does not establish membership in \(\mathrm{NP}\), and the prover correctly makes no such claim.
The second construction is also correct.
The empty hypothesis does not entail \(z_0\), while \(\{s\}\) consistently entails it. Since \(A=\{s\}\), this is the unique fully abducible inclusion-minimal explanation. The identical-role calculation applies and fixes the common context as \(C_n=N(S_n,\{s\})\).
For each clause \(E_{c_1,\ldots,c_n}\), all three required properties are established:
Consequence. If all selected \(c_i\) are true, the Horn implications force the chain through \(z_n\). Otherwise a negative literal in the clause is true.
Subsumption-minimality. The valuation given for deleting \(z_n\) satisfies the theory and falsifies the shortened clause. For deleting \(\neg c_j\), the second valuation satisfies every Horn implication: conclusions before stage \(j\) are true, both stage-\(j\) antecedents fail, and later antecedents fail through their preceding \(z\)-atom. It falsifies the shortened clause.
Checking every single-literal deletion suffices here: any further shortened clause is also false under a valuation falsifying a containing single-deletion clause.
Newness. Setting \(s\) and all \(z_i\) false, with every \(a_i,b_i\) true, satisfies \(S_n\) and falsifies every selected clause. Thus none is a consequence of \(S_n\).
Distinct choices produce distinct literal sets, giving \(|C_n|\geq 2^n\).
The parameter counts are correct: \(m=3n+2\), \(\tau=q=2\), and \(L=O(n\log(n+1))\) under the stated encoding. Consequently, a literal-by-literal listing of the final context has superpolynomial length in the input parameters.
The scope qualification matters: this establishes the additional unconditional running-time obstruction for explicitly enumerated contexts. It does not independently establish that obstruction for an encoding permitting compressed contexts. The prover states the qualification, and the hardness result does not depend on it.
None. The argument resolves the target hardness question, and its additional output-size claim holds with the representation qualification expressly given.
⟨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.