Answer: Polynomial-time solvable: in \(\mathrm{P}\), with running time \(O(L+m\tau+\tau s+q\tau^3)\) in the standard word-RAM model.
Theorem 1 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateModel checking of formula φ for a given agent in a given social network could be accomplished in time O(|φ|(|A|3 + |A| · |{≺a}a∈A|)) in the worst case.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite support \(T\) with rational masses \(\mu_t>0\) summing to \(1\), a formula \(\phi\), and a designated type \(t^\star\), decide whether \(t^\star\models\phi\). Each type records its propositional labels, humbled and egotistic status, friend types \(F(t)\), and strict partial preference order \(\prec_t\) over types; require \(t\in F(t)\) and the paper's compatibility, humbleness, and egotism conditions lifted to whole cohorts. Interpret \(F\phi\) over friend types and \(L\phi\) by requiring every supported type \(u\not\models\phi\) to satisfy \(u\prec_t v\) for every supported type \(v\models\phi\).
A society is given by its support: a nonempty list \(T\) 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.
Each type has Boolean labels for \(m\) propositional variables, membership flags in sets \(H,E\subseteq T\), an explicitly listed friend set \(F(t)\subseteq T\), and a strict partial preference order \(\prec_t\) represented by the transitive closure of an input DAG on \(T\). These data apply uniformly to each whole cohort; within a cohort there are no strict preferences.
Inputs satisfy \(t\in F(t)\); for all \(t,u,v\in T\) and \(f\in F(t)\), \(u\prec_t v\Rightarrow\neg(v\prec_f u)\); for \(h\in H\) and \(f\in F(h)\), \(\neg(f\prec_h h)\); and for \(e\in E\) and \(f\in F(e)\), \(\neg(e\prec_e f)\). Friendship need not be symmetric, and \(H\) and \(E\) may overlap.
Formulae have grammar \(\psi ::= p\mid\eta\mid\varepsilon\mid\neg\psi\mid(\psi\to\psi)\mid F\psi\mid L\psi\), with standard Boolean semantics and the given propositional labels; \(\eta\) and \(\varepsilon\) mean membership in \(H\) and \(E\), respectively.
Define \(t\models F\psi\) iff every \(f\in F(t)\) satisfies \(\psi\), and \(t\models L\psi\) iff \(u\prec_t v\) for every \(u,v\in T\) with \(u\not\models\psi\) and \(v\models\psi\). This universal condition is vacuous if either class is empty.
Given such a society, a formula \(\phi\), and \(t^\star\in T\), the decision problem asks whether \(t^\star\models\phi\). Let \(L\) be the total input bit length, \(q=|\phi|\) its symbol count, and \(s\) the total number of input preference edges; state running times in \(m,\tau,L,q,s\).
Is this continuous model-checking problem in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard?
For finite agent societies, model checking is solvable in \(O(q(n^3+ns))\) time, where \(n\) is the number of agents and \(s\) counts preference-generating edges ([Jiang and Naumov, 2022](https://www.ijcai.org/proceedings/2022/0371.pdf)). No result for exactly the mass-based formulation above was identified in the literature search.
The problem is in \(\mathrm{P}\). More precisely, it admits a deterministic algorithm running in
\(O(L+m\tau+\tau s+q\tau^3)\)
time in the standard word-RAM model.
The key point is that the support is explicitly listed, and neither modal operator uses the numerical masses. Formula evaluation therefore requires one truth value per support type, without expanding cohorts according to their masses.
Index the support as \(T=\{1,\ldots,\tau\}\). For each \(t\in T\), let \(G_t\) be the input DAG generating \(\prec_t\), and let \(s_t\) be its number of edges. Thus \(s=\sum_{t\in T}s_t\).
First compute a Boolean table \(R_t\) for each type, defined by
\(R_t[u,v]=1\) exactly when \(G_t\) contains a directed path of positive length from \(u\) to \(v\).
By the input representation, this is equivalent to \(u\prec_t v\). Since \(G_t\) is acyclic, its diagonal entries are false.
Parse \(\phi\) into a syntax tree and process its nodes in an order in which children precede parents. For each subformula occurrence \(\psi\), compute a Boolean vector \(B_\psi\) indexed by \(T\), using the following rules:
\(B_{L\psi}[t]=\bigwedge_{(u,v)\in X_\psi\times Y_\psi}R_t[u,v]\).
An empty conjunction is true. Thus the last rule implements the stipulated vacuity when either class is empty.
Return \(B_\phi[t^\star]\).
We prove by structural induction that, for every subformula occurrence \(\psi\) and every \(t\in T\),
\(B_\psi[t]=1\) if and only if \(t\models\psi\).
For a propositional variable, the assertion follows from the input label. For \(\eta\) and \(\varepsilon\), it follows from their respective membership semantics.
Suppose the assertion holds for \(\psi\). Then \(B_{\neg\psi}[t]=1\) exactly when \(B_\psi[t]=0\), which by the induction hypothesis means \(t\not\models\psi\). This is precisely \(t\models\neg\psi\).
Suppose it holds for both \(\psi\) and \(\chi\). The implication rule makes \(B_{\psi\to\chi}[t]\) true exactly when \(t\not\models\psi\) or \(t\models\chi\), as required by Boolean semantics.
For \(F\psi\), the induction hypothesis gives
\(B_{F\psi}[t]=1\) if and only if every \(f\in F(t)\) satisfies \(\psi\).
This is exactly the definition of \(t\models F\psi\).
For \(L\psi\), the induction hypothesis identifies
\(X_\psi=\{u\in T:u\not\models\psi\}\) and
\(Y_\psi=\{v\in T:v\models\psi\}\).
The reachability tables satisfy \(R_t[u,v]=1\) if and only if \(u\prec_t v\). Consequently, \(B_{L\psi}[t]=1\) exactly when \(u\prec_t v\) for every \(u\not\models\psi\) and \(v\models\psi\). Empty classes produce an empty conjunction, so this equivalence also covers the vacuous cases.
The induction is complete. In particular, the returned value correctly decides whether \(t^\star\models\phi\).
The additional friendship and preference compatibility conditions are input promises. The proof applies to every input satisfying them; it requires no stronger assumptions.
Reading and parsing the input costs \(O(L)\), and storing the propositional labels costs \(O(m\tau)\).
For each \(G_t\), run a graph search from each of its \(\tau\) vertices. Each search costs \(O(\tau+s_t)\), so all reachability tables cost
\(O\!\left(\sum_{t\in T}\tau(\tau+s_t)\right)=O(\tau^3+\tau s)\).
There are at most \(q\) syntax-tree nodes. The cost of computing the truth vector at one node is:
| Node kind | Time |
|---|---:|
| Atomic or Boolean | \(O(\tau)\) |
| \(F\psi\) | \(O(\tau^2)\) |
| \(L\psi\) | \(O(\tau^3)\) |
For the friendship bound, \(\sum_{t\in T}|F(t)|\leq\tau^2\). For the preference bound, each of the \(\tau\) types requires at most \(\tau^2\) table lookups.
Since \(q\geq1\) and \(\tau\geq1\), the total time is therefore
\(O(L+m\tau+\tau s+q\tau^3)\).
A sufficient space bound is \(O(L+m\tau+\tau^3+q\tau)\).
These bounds use constant-time Boolean table access and words of \(O(\log(L+2))\) bits. Explicit input encoding gives \(\tau,q,s=O(L)\), and the explicitly supplied labels give \(m\tau=O(L)\). Hence the time and storage are polynomial in the total input length. A standard Turing-machine simulation also has polynomial running time, establishing membership in \(\mathrm{P}\).
For fixed support types, labels, friendship sets, and preference orders, replacing the masses by any other positive rational masses summing to \(1\) leaves every formula’s truth unchanged. This follows directly from the induction above: every recurrence uses only the structural data and previously computed truth values.
Thus binary denominators cause no computational expansion. The algorithm reads the mass encoding as part of the input but performs no mass arithmetic. Its dependence is on the listed support size \(\tau\), rather than on the number of possible label combinations or any denominator-derived population size.
This is consistent with the finite-society algorithm in [Jiang and Naumov, Theorem 1](https://www.ijcai.org/proceedings/2022/0371.pdf). The proof here independently establishes the result for the specified mass-based input, with preference closures computed once and reused.
Accordingly, the target question is resolved as polynomial-time solvable. NP-hardness under polynomial-time many-one reductions would imply \(\mathrm{P}=\mathrm{NP}\).
⟨structured verdict parsed — rendered above⟩
The prover’s claim is proved. The algorithm implements the supplied semantics exactly, and its running time is polynomial in the total input bit length. No major or minor mathematical issues were found.
The task explicitly lists the support \(T\), with \(\tau\) types, and defines satisfaction directly on those types. Thus a truth vector with one entry per support type has the correct domain.
Neither modal clause uses the masses \(\mu_t\). Ignoring their numerical values during evaluation is therefore justified. Reading their encoding contributes to \(O(L)\), but no population expansion or arithmetic on denominators is required.
By the stipulated representation, \(u\prec_t v\) holds exactly when the input DAG \(G_t\) contains a directed path of positive length from \(u\) to \(v\). This is exactly the definition of \(R_t[u,v]\).
Acyclicity rules out positive-length paths from a vertex to itself, so the stated false diagonal is correct. The algorithm does not substitute reflexive reachability for the required strict relation.
Processing syntax-tree children before parents ensures that every recurrence has its required truth vectors available. Working with subformula occurrences also handles repeated subformulae without requiring any additional identification or sharing mechanism.
The rules for propositional variables, \(\eta\), and \(\varepsilon\) use precisely the supplied labels and membership flags.
Negation complements the child’s truth value. Implication uses \(\neg B_\psi[t]\lor B_\chi[t]\), matching standard Boolean implication. The corresponding induction steps establish the required equivalences for every type.
The recurrence checks every member of the explicitly supplied \(F(t)\). Under the induction hypothesis, it is true exactly when every \(f\in F(t)\) satisfies \(\psi\).
No symmetry assumption is introduced. Self-friendship is handled by the supplied set itself.
The induction hypothesis identifies \(X_\psi\) with all types failing \(\psi\), and \(Y_\psi\) with all types satisfying it. For each evaluating type \(t\), the recurrence checks \(R_t[u,v]\) for every ordered pair in \(X_\psi\times Y_\psi\).
The orientation is correct: it checks \(u\prec_t v\), with \(u\) failing the formula and \(v\) satisfying it.
If either class is empty, the conjunction is empty and true, as required. This also covers constant truth vectors and the case \(\tau=1\).
The induction covers every constructor in the grammar and quantifies over every support type. Consequently, its specialization to \(\phi\) and \(t^\star\) proves that the returned Boolean value answers the decision problem.
The compatibility conditions are input promises. The proof does not need them beyond the specified input semantics, and proving correctness on a broader collection of structures does not weaken correctness on promised inputs. Overlap between \(H\) and \(E\) causes no problem because their flags are evaluated independently.
A graph search from each of the \(\tau\) vertices of \(G_t\) costs \(O(\tau(\tau+s_t))\). Summing over all \(\tau\) evaluating types gives \(O(\tau^3+\tau s)\), since \(s=\sum_t s_t\).
Atomic and Boolean nodes require \(O(\tau)\) operations. Friendship evaluation examines at most \(\sum_t|F(t)|\leq\tau^2\) memberships. Preference evaluation examines at most \(\tau^2\) pairs for each of \(\tau\) types, giving \(O(\tau^3)\).
Constructing the two truth classes takes \(O(\tau)\), which is absorbed by the preference-node bound.
There are at most \(q\) syntax-tree nodes. Because \(q\geq1\), the preprocessing term \(O(\tau^3)\) is absorbed by \(O(q\tau^3)\). The claimed total time \(O(L+m\tau+\tau s+q\tau^3)\) follows.
The space bound accounts for the input, labels, all reachability tables, and all subformula truth vectors. Words of \(O(\log(L+2))\) bits suffice for indices and addresses in polynomial-sized storage, with a suitable constant factor.
Explicit encoding gives \(\tau,q,s=O(L)\) and \(m\tau=O(L)\). Hence both resource bounds are polynomial. The polynomial Turing-machine simulation suffices for membership in \(\mathrm{P}\).
[Jiang and Naumov, Theorem 1](https://www.ijcai.org/proceedings/2022/0371.pdf) states the cited finite-society bound. The prover uses it only as a consistency comparison; the supplied proof independently establishes the present result.
The final statement about NP-hardness is correctly conditional: polynomial-time many-one NP-hardness together with membership in \(\mathrm{P}\) would imply \(\mathrm{P}=\mathrm{NP}\).
No repair or additional clarification 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.