Answer: Exact computation of all bloc EGSVs and optional per-capita rates is polynomial-time solvable, with \(O(L+\tau+K+mK)\) arithmetic operations and input-processing steps, and \(O((L+\tau+K+mK)(L+K\log_2(K+1))^2)\) bit operations for exact numerator–denominator outputs.
Theorem 5.5 — class: algorithmic
Given supported types \(t\) with rational masses \(\mu_t\) summing to \(1\), a fixed partition of those types into \(K\) blocs \(B_1,\ldots,B_K\), and literal embedded rules with per-unit rates \(q\), compute each bloc's EGSV and, optionally, its per-capita rate. A matching rule contributes \(q\lambda(B_j)\) to its target bloc, where \(\lambda(B_j)=\sum_{t\in B_j}\mu_t\), and type cohorts join blocs as units.
A society is given by its support \(U\): the list of the \(\tau\) types with positive binary-rational masses \(\mu_t\), summing to \(1\); \(\tau\) is the support size, not the number of possible types. The input includes a partition \(\pi=\{B_1,\ldots,B_K\}\) into nonempty blocs; type cohorts are indivisible. Write \(\lambda(S)=\sum_{t\in S}\mu_t\).
There are \(m\) embedded rules \(P_0\mid P_1,\ldots,P_k\to q\), with signed binary-rational rates \(q\). Each \(P_i\) is a conjunction of positive and negative type literals: \(S\) satisfies it exactly when it contains every positive type and no negative type. An empty conjunction is true. Each rule has at least one positive literal in \(P_0\) or negative literal among \(P_1,\ldots,P_k\).
For a partition \(\rho\) of \(U\) and \(S\in\rho\), a rule matches \((S,\rho)\) when \(S\) satisfies \(P_0\) and every external pattern \(P_i\) has a witness in \(\rho\setminus\{S\}\); witnesses need not be distinct. Its contribution is \(q\lambda(S)\). Let \(w(S,\rho)\) be the sum of matching contributions.
Define a characteristic-function game on the \(K\) blocs by \(v(\varnothing)=0\) and, for nonempty \(T\subseteq\pi\), \(v(T)=w(S_T,\{S_T,U\setminus S_T\}\setminus\{\varnothing\})\), where \(S_T=\bigcup_{B\in T}B\). The EGSV of \(B_j\) is its standard Shapley value \(\phi_j(v)\); its optional per-capita rate is \(\phi_j(v)/\lambda(B_j)\).
Is exact computation of all bloc EGSVs (and optional per-capita rates) polynomial-time solvable, or is it NP-hard? State running times in \(m,\tau,K,L\), where \(L\) is the total binary input length, including all literal occurrences.
For finite agents with constant rule values, EGSV admits a representation with two transformed rules per input rule and computation linear in representation size ([discrete result](https://www.cs.ox.ac.uk/people/michael.wooldridge/pubs/aamas2010c.pdf)).
No result settling this exact mass-dependent formulation was identified in the literature search.
Exact computation of all bloc EGSVs and their optional per-capita rates is polynomial-time solvable.
Let \(B=L+K\log_2(K+1)\). An algorithm uses
\[ O(L+\tau+K+mK) \]
arithmetic operations and input-processing steps, and can be implemented in
\[ O\!\left((L+\tau+K+mK)B^2\right) \]
bit operations using schoolbook integer arithmetic, with exact rational outputs represented as numerator–denominator pairs.
The proof below derives the required Shapley formulas directly. It uses conjunction games, as in the [linked discrete result](https://www.cs.ox.ac.uk/people/michael.wooldridge/pubs/aamas2010c.pdf), while explicitly accounting for coalition mass.
Identify the blocs with the player set \(N=\{1,\ldots,K\}\). Write \(b(t)\) for the bloc containing type \(t\), and put \(a_j=\lambda(B_j)\). Thus \(a_j>0\) and \(\sum_{j\in N}a_j=1\).
Consider one rule \(r:P_0\mid P_1,\ldots,P_k\to q\). Let \(X_i^+\) and \(X_i^-\) denote the positive and negative type literals in \(P_i\).
If literals may name types outside \(U\), first normalize them. A positive literal naming an absent type makes the rule impossible, because every possible witness is a subset of \(U\). Negative literals naming absent types can be deleted. This preprocessing also covers the interpretation in which every literal already names a supported type.
For a remaining rule, define
\[ A=\left\{b(t):t\in X_0^+\cup\bigcup_{i=1}^kX_i^-\right\}, \qquad D=\left\{b(t):t\in X_0^-\cup\bigcup_{i=1}^kX_i^+\right\}. \]
Here \(A\) contains the required blocs, and \(D\) contains the forbidden blocs. Cohort indivisibility justifies this translation: a coalition of blocs contains type \(t\) exactly when it contains \(b(t)\).
If \(A\cap D\ne\varnothing\), discard the rule. No coalition can meet its simultaneous inclusion and exclusion requirements.
Suppose henceforth that \(A\cap D=\varnothing\). For a nonempty proper coalition \(T\subsetneq N\), its embedded partition contains exactly two coalitions: \(S_T\) and \(U\setminus S_T\). Consequently, every external pattern must be witnessed by \(U\setminus S_T\). The rule therefore matches exactly when
\[ A\subseteq T,\qquad D\cap T=\varnothing. \]
This equivalence uses the stipulated permission to reuse a witness.
Define
\[ g_{A,D}(T)= \left(\sum_{j\in T}a_j\right) \mathbf 1_{\{A\subseteq T,\ D\cap T=\varnothing\}}. \]
This definition gives \(g_{A,D}(\varnothing)=0\), including when \(A=\varnothing\).
Let \(u_N(T)=\mathbf 1_{\{T=N\}}\), and set
\[ \delta_r= \begin{cases} 1,&k>0\text{ and }D=\varnothing,\\ 0,&\text{otherwise}. \end{cases} \]
The rule’s characteristic-function contribution is exactly
\[ v_r(T)=q\,g_{A,D}(T)-\delta_r q\,u_N(T). \]
To verify the boundary cases:
In particular, an empty external pattern still requires a witness; the correction handles this case.
For disjoint sets \(H,D\subseteq N\), with \(h=|H|\geq1\) and \(d=|D|\), define
\[ e_{H,D}(T)=\mathbf 1_{\{H\subseteq T,\ D\cap T=\varnothing\}}. \]
Its Shapley values are
\[ \phi_j(e_{H,D})= \begin{cases} \dfrac{(h-1)!\,d!}{(h+d)!},&j\in H,\\[6pt] -\dfrac{h!\,(d-1)!}{(h+d)!},&j\in D,\\[6pt] 0,&j\notin H\cup D. \end{cases} \]
The second case applies only when \(d\geq1\).
Proof. Use the random-permutation definition of the Shapley value. The relative order of the \(h+d\) players in \(H\cup D\) is uniform.
For \(j\in H\), its marginal contribution is \(1\) precisely when every player in \(H\setminus\{j\}\) precedes \(j\), and every player in \(D\) follows \(j\). There are \((h-1)!\,d!\) such relative orders out of \((h+d)!\).
For \(j\in D\), its marginal contribution is \(-1\) precisely when every player in \(H\) precedes \(j\), and every player in \(D\setminus\{j\}\) follows \(j\). There are \(h!\,(d-1)!\) such relative orders.
Adding a player outside \(H\cup D\) never changes the game value, so its marginal contribution is always zero. These observations prove every case. \(\square\)
Also, \(\phi_j(u_N)=1/K\): a player changes the grand-coalition indicator precisely when it is last in the permutation.
For every \(T\subseteq N\),
\[ g_{A,D}(T)= \sum_{j\in N\setminus D}a_j\,e_{A\cup\{j\},D}(T). \]
Indeed, if \(T\) violates the requirements \(A\subseteq T\) and \(D\cap T=\varnothing\), every term on the right vanishes. Otherwise, its \(j\)-th term equals \(a_j\) exactly when \(j\in T\), so the sum equals the mass of \(T\).
Every conjunction on the right has at least one required player. Thus the formula proved in Section 2 applies even if normalization produced \(A=\varnothing\).
This already proves polynomial-time computability: each input rule becomes at most \(K\) constant-valued conjunction games and one grand-coalition correction. The following aggregation gives a sharper running time.
Let
\[ F=N\setminus(A\cup D),\qquad p=|A|,\qquad d=|D|,\qquad M_A=\sum_{j\in A}a_j,\qquad M_F=\sum_{j\in F}a_j. \]
Then
\[ g_{A,D}=M_Ae_{A,D}+\sum_{j\in F}a_j e_{A\cup\{j\},D}, \]
where the first term is omitted when \(A=\varnothing\).
For \(h\geq1\), define
\[ c_+(h,d)=\frac{(h-1)!\,d!}{(h+d)!}, \]
and, when \(d\geq1\), define
\[ c_-(h,d)=-\frac{h!\,(d-1)!}{(h+d)!}. \]
Linearity of the Shapley value now gives the complete formulas.
If \(j\in A\), then \(p\geq1\) and
\[ \phi_j(g_{A,D}) =M_Ac_+(p,d)+M_Fc_+(p+1,d). \]
If \(j\in D\), then \(d\geq1\), and
\[ \phi_j(g_{A,D})= \begin{cases} M_Ac_-(p,d)+M_Fc_-(p+1,d),&p\geq1,\\ M_Fc_-(1,d),&p=0. \end{cases} \]
If \(j\in F\), then
\[ \phi_j(g_{A,D})=a_jc_+(p+1,d). \]
Terms multiplied by \(M_F=0\) can simply be omitted.
To justify the aggregation, a required player belongs to the positive set of every component conjunction; a forbidden player belongs to the negative set of every component conjunction. A free player \(j\) occurs only in its own component, with coefficient \(a_j\), and is a null player in all other components.
Therefore, one input rule contributes
\[ \phi_j(v_r)=q\,\phi_j(g_{A,D})-\frac{\delta_rq}{K} \]
to bloc \(j\).
The input game is the sum of these rule games. Summing these contributions therefore computes all bloc EGSVs exactly, including for signed rates.
The algorithm performs the following steps:
Reading and translating all literal occurrences takes \(O(L)\) input-processing steps. Computing bloc masses takes \(O(\tau)\) arithmetic operations. Each rule takes \(O(K)\) additional arithmetic operations, including its updates to all outputs. Precomputing factorials takes \(O(K)\) operations.
Hence the total is
\[ O(L+\tau+K+mK). \]
For the bit bound, write the input rationals as integer numerator–denominator pairs. Let \(D_\mu\) be the product of the mass denominators and \(D_q\) the product of the rate denominators. Both have \(O(L)\) bits. Set
\[ H=D_\mu D_q K!. \]
For every conjunction actually used, \(h+d\leq K\). Its Shapley coefficients satisfy
\[ K!c_+(h,d)=\frac{K!}{(h+d)!}(h-1)!\,d!\in\mathbb Z, \]
and, for \(d\geq1\),
\[ K!c_-(h,d)=-\frac{K!}{(h+d)!}h!\,(d-1)!\in\mathbb Z. \]
The grand-coalition correction also has denominator dividing \(K!\).
Consequently, all outputs can be accumulated as integers over the common denominator \(H\). Specifically, \(D_\mu a_j\) and \(D_q q\) are integers, and multiplying these integers by the scaled Shapley coefficients gives the corresponding output numerator increments.
Input rate magnitudes are at most \(2^{O(L)}\), and summing over \(m\) rules adds only \(O(\log(m+1))\) bits. Thus every integer used in this implementation has
\[ O\!\left(L+K\log_2(K+1)\right)=O(B) \]
bits, including intermediate factorial products.
Schoolbook multiplication and long division on these integers cost \(O(B^2)\) bit operations. This proves the stated bound
\[ O\!\left((L+\tau+K+mK)B^2\right) \]
for exact numerator–denominator outputs. Reducing the fractions, if desired, also takes polynomial time.
Since \(K\leq\tau\) and the society, partition, and rules are explicitly represented, this is polynomial in the total input length.
Every bloc is nonempty and every supported type has positive mass. Therefore \(a_j>0\), and the per-capita rate \(\phi_j(v)/a_j\) is well-defined.
Write \(a_j=x_j/D_\mu\), where \(x_j\) is a positive integer. If the computed EGSV is \(n_j/H\), then its per-capita rate is
\[ \frac{\phi_j(v)}{a_j} =\frac{n_j}{D_qK!\,x_j}. \]
This requires only \(O(K)\) additional integer operations on \(O(B)\)-bit numbers and preserves the polynomial bit bound.
As a computational cross-check, the formulas were compared using exact rational arithmetic with direct Shapley summation over every coalition in 600 generated instances with one through six blocs. These checks included grouped types, contradictory requirements, absent-type literals, empty external patterns, and signed rates. All comparisons agreed; the proof above establishes correctness independently.
⟨structured verdict parsed — rendered above⟩
The prover resolves the stated task. The rule compilation, Shapley formulas, and exact bit-complexity bound are correct. I found no major or minor issues requiring repair.
The proof uses the \(K\) blocs as Shapley players, as required. The mass \(a_j=\lambda(B_j)\) is positive because each bloc is nonempty and each supported type has positive mass. Also, \(K\geq1\), so division by \(K\) is valid.
The argument addresses the specified mass-dependent contribution \(q\lambda(S)\), including signed rates. It does not substitute the constant-valued discrete formulation.
The preprocessing of unsupported types is correct: an unsupported positive literal cannot be satisfied by any coalition or witness, while an unsupported negative literal is always satisfied.
For a nonempty proper coalition \(T\), the embedded partition has exactly one external coalition, namely its complement. Therefore:
These are precisely the definitions of \(A\) and \(D\). Reusing the complement as a witness is permitted by the task. Thus the matching equivalence is correct.
If \(A\cap D\neq\varnothing\), the requirements are inconsistent. Discarding such a rule is valid, including at the grand coalition: external patterns then have no witness, while a rule without external patterns retains contradictory internal requirements.
The identity \(v_r=qg_{A,D}-\delta_rqu_N\) handles both boundaries correctly.
At the empty coalition, the mass factor makes \(g_{A,D}\) zero even when \(A=\varnothing\). The grand-coalition indicator is also zero there.
At the grand coalition:
An empty external conjunction still needs an external witness under the task’s definition. The correction handles this correctly.
The permutation counting is correct.
For \(j\in H\), a positive marginal occurs exactly when all other required players precede \(j\) and all forbidden players follow it. The number of qualifying relative orders is \((h-1)!\,d!\), out of \((h+d)!\).
For \(j\in D\), a negative marginal occurs exactly when all required players precede \(j\) and every other forbidden player follows it. The count is \(h!\,(d-1)!\).
Players outside \(H\cup D\) have zero marginal contribution. The restrictions \(h\geq1\) and \(d\geq1\) for the negative case prevent undefined factorials.
The grand-coalition indicator gives each player \(1/K\), since its marginal is nonzero exactly when that player is last.
The decomposition into conjunction games is valid coalition by coalition. If a coalition violates the original requirements, every component vanishes. Otherwise, precisely the components indexed by its members contribute their masses.
Every component has a nonempty required set, so the conjunction formulas apply even when \(A=\varnothing\).
The aggregated formulas correctly distinguish required, forbidden, and free players. In particular, a free player appears as a required player only in its own component and is null in every other component.
When \(F=\varnothing\), the stated instruction to omit terms multiplied by \(M_F=0\) avoids evaluating coefficients for unused conjunctions whose sizes could exceed \(K\).
Shapley linearity then justifies summing the rule contributions. Signed rates introduce no additional restriction.
The operation count is consistent with the algorithm:
The common denominator \(H=D_\mu D_qK!\) is sufficient. For every conjunction actually used, \(h+d\leq K\), so the displayed scaled coefficients are integers. The grand-coalition correction also has denominator dividing \(K!\).
The denominator products have \(O(L)\) bits, and \(K!\) has \(O(K\log_2(K+1))\) bits. Input magnitudes and accumulation over the explicitly represented rules preserve the claimed \(O(B)\) bound on integer lengths. Schoolbook multiplication and division therefore yield the stated bit bound \(O((L+\tau+K+mK)B^2)\).
Because \(K\leq\tau\) and the support and partition are explicitly represented, this is polynomial in input length.
The division by bloc mass is valid because every \(a_j>0\). The cancellation giving the denominator \(D_qK!x_j\) is correct, and its bit length remains \(O(B)\).
The reported randomized checks are supplementary. Their execution is not independently documented in the supplied output, but correctness does not depend on them: the written derivation establishes the result.
No repair or additional lemma 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.