← back to the atlas

d4-conf-atal-2016-0262 (d4-conf-atal-2016-0262)

Answer: Polynomial-time solvable for every fixed \(k\ge2\); all limits exist, with running time \(O(\tau L^3+\tau^2L)=O(mL^3+m^2L)\) for \(m=\tau\).

The anchor (named result in the paper)

Theorem 4 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateThe k-coalitional Shapley value of the Network Control Game can be computed in polynomial time assuming that k is constant. PROOF. The proof is based on the following lemma. LEMMA 3. Assume we have n numbered items and k colors, and we color each item with a single color.

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

The continuous mirror question, as graded

Fix \(k\), and take a finite type set \(T\), rational masses \(\mu_t>0\) summing to \(1\), and a symmetric matrix \(A\in\{0,1\}^{|T|\times |T|}\). Let \(D\) be a common denominator of the masses and form \(G_r\) with \(rD\mu_t\) vertices of type \(t\); distinct vertices of types \(t,u\) are adjacent exactly when \(A_{tu}=1\). For each vertex \(i\), set \(I_i(S)=|S\cap M^+(i)|\), where \(M^+(i)\) is its closed neighborhood, and use the paper’s value \(\nu(S,P)=|\{i:S\in\arg\max_{Q\in P} I_i(Q)\}|\) on partitions with at most \(k\) coalitions. Determine whether the \(k\)-coalitional Shapley payoff \(\Phi_t(r)\) of a vertex of each type \(t\) has a limit as \(r\to\infty\); when it does, compute each limit to accuracy \(\varepsilon\) and provide a certified \(R\) such that \(|\Phi_t(r)-\lim_{s\to\infty}\Phi_t(s)|\le\varepsilon\) for every \(r\ge R\).

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

Fix an integer \(k\ge2\). A society is given by its support: a nonempty list \(T\) of \(\tau\) types with positive binary-rational masses \(\mu_t\) summing to \(1\); \(\tau\) counts supported types, not possible types. Also given are a symmetric matrix \(A\in\{0,1\}^{\tau\times\tau}\) and binary-rational accuracy \(0<\varepsilon<1\).
Let \(D\) be the least common denominator of the masses. For integers \(r\ge\lceil k/D\rceil\), construct the simple graph \(G_r\) with \(rD\mu_t\) vertices of type \(t\); distinct vertices of types \(t,u\) are adjacent exactly when \(A_{tu}=1\), including when \(t=u\).
For each vertex \(j\), let \(M^+(j)\) be its closed neighborhood and \(I_j(S)=|S\cap M^+(j)|\). For a partition \(P\) into at most \(k\) nonempty coalitions, define \(\nu(S,P)=|\{j:I_j(S)=\max_{Q\in P}I_j(Q)\}|\) for \(S\in P\): every tied maximizing coalition receives full credit. Set the value of the empty coalition to \(0\).
Define the payoff of vertex \(i\) by this random process: start with the grand coalition, remove vertices in a uniformly random order, and independently assign each departing vertex uniformly to one of \(k-1\) labeled exits; vertices assigned to the same exit form a coalition.
If \(S\) is the remaining coalition just before \(i\) departs, and \(P,P'\) are the partitions before and after its transfer, its payoff is the expectation of \(\nu(S,P)-\nu(S\setminus\{i\},P')\). Empty groups are omitted. Write \(\Phi_t(r)\) for this unnormalized payoff of any vertex of type \(t\).
The computational problem is to decide, for each \(t\), whether the finite real limit \(\ell_t=\lim_{r\to\infty}\Phi_t(r)\) exists, and for every existing limit compute a rational \(a_t\) with \(|a_t-\ell_t|\le\varepsilon\) and a binary integer \(R\ge\lceil k/D\rceil\) satisfying \(|\Phi_t(r)-\ell_t|\le\varepsilon\) for all integers \(r\ge R\).
For each fixed \(k\), is this problem solvable in polynomial time, or is it NP-hard? State running times in \(m=\tau\), \(\tau\), and total input bit length \(L\), including the encoding of \(\varepsilon\).
For explicit finite graphs, these payoffs are computable in polynomial time when \(k\) is constant ([discrete algorithm](https://aamas.csc.liv.ac.uk/Proceedings/aamas2016/pdfs/p177.pdf)). No result settling this exact limit-and-certification problem was located.

Modeling choices made when packaging the task

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

Result

The problem is polynomial-time solvable for every fixed \(k\ge2\). Every limit exists, and the limits are rational. The key simplification is that the finite-graph payoffs are independent of \(k\).

The proof uses exactly the departure process and full tie credit stipulated in the question; these are also described in Sections 4 and 6 of the [cited paper](https://aamas.csc.liv.ac.uk/Proceedings/aamas2016/pdfs/p177.pdf).

1. A local payoff identity

Let \(V\) be a finite vertex set, and fix a nonempty subset \(B\subseteq V\). Define a local coalition value by

\(v_B(S,P)=\mathbf 1_{\{|S\cap B|=\max_{Q\in P}|Q\cap B|\}}\)

for nonempty \(S\in P\), and set \(v_B(\varnothing,P)=0\).

Let \(X_i^B\) be vertex \(i\)'s realized marginal contribution to this local value under the specified departure process.

Lemma. For every \(i\in V\),

\(\mathbb E[X_i^B]=1/|B|\) if \(i\in B\), and \(\mathbb E[X_i^B]=0\) otherwise.

Proof.

First suppose \(i\notin B\). Its departure changes none of the intersection counts with \(B\). Creating an exit coalition containing no member of \(B\), or omitting such an empty coalition, also cannot change the maximum: because \(B\ne\varnothing\) and the partition covers \(V\), that maximum is always positive.

The only additional case is that the remaining coalition becomes empty. Immediately before that departure it is \(\{i\}\), which contains no member of \(B\), while some exit contains a member of \(B\). Its local value is therefore already zero. Consequently, \(X_i^B=0\) in every realization.

Next, fix a complete realization. Write \(S_q\) and \(P_q\) for the remaining coalition and partition after \(q\) departures, with \(S_0=V\) and \(S_{|V|}=\varnothing\). The marginal contributions telescope:

\(\displaystyle \sum_{i\in V}X_i^B =\sum_{q=1}^{|V|}\bigl(v_B(S_{q-1},P_{q-1})-v_B(S_q,P_q)\bigr) =v_B(V,\{V\})-v_B(\varnothing,P_{|V|})=1.\)

Finally, any permutation of the vertices preserving \(B\) preserves both the local value and the distribution of the departure process. In particular, exchanging two members of \(B\) exchanges their marginal contributions without changing their distribution. Thus all members of \(B\) have the same expected contribution.

Their expected contributions sum to \(1\), since the contributions of vertices outside \(B\) vanish. Each expectation is therefore \(1/|B|\). This proves the lemma. \(\square\)

Applying the lemma separately with \(B=M^+(j)\), and using linearity of expectation, gives the following exact identity for any finite undirected graph:

\(\displaystyle \Phi_i=\sum_{\substack{j\in V\\i\in M^+(j)}}\frac1{|M^+(j)|} =\sum_{j\in M^+(i)}\frac1{|M^+(j)|}.\)

The second equality uses symmetry of adjacency. No asymptotic argument is involved in this identity.

2. Exact payoffs for the replicated graphs

Define the positive integers and row sums

\(\displaystyle c_t=D\mu_t,\qquad B_u=\sum_{v\in T}A_{uv}c_v,\qquad \delta_u=1-A_{uu}.\)

Thus \(\sum_t c_t=D\), and every \(c_t\ge1\).

In \(G_r\), the number of vertices of type \(u\) is \(r c_u\). Every vertex of that type has closed-neighborhood size

\(\displaystyle d_u(r)=rB_u+\delta_u.\)

Indeed, when \(A_{uu}=1\), the term \(rB_u\) already includes the vertex itself. When \(A_{uu}=0\), the closed neighborhood requires adding that vertex separately.

All these denominators are positive. If \(\delta_u=0\), then \(A_{uu}=1\) and \(B_u\ge c_u\ge1\); otherwise \(\delta_u=1\).

For a vertex of type \(t\), the finite-graph identity therefore yields

\(\displaystyle \Phi_t(r)= \sum_{u\in T}\frac{A_{tu}\,r c_u}{rB_u+\delta_u} +\frac{\delta_t}{rB_t+\delta_t}.\)

The last term supplies the vertex's own contribution precisely when \(A_{tt}=0\).

3. Every limit exists

If \(B_t=0\), positivity of all \(c_u\) implies that row \(t\) of \(A\) is zero. In particular, \(\delta_t=1\), and the exact formula gives

\(\displaystyle \Phi_t(r)=1\)

for every admissible \(r\).

Now suppose \(B_t>0\). The last term in the formula tends to zero. Whenever \(A_{tu}=1\), symmetry gives \(A_{ut}=1\), so

\(\displaystyle B_u\ge c_t\ge1.\)

Hence every nonzero summand has the limit \(c_u/B_u\). There are finitely many summands, so the limit exists and is finite.

Combining the two cases,

\(\displaystyle \boxed{\ell_t= \mathbf 1_{\{B_t=0\}} +\sum_{\substack{u\in T\\B_u>0}}\frac{A_{tu}c_u}{B_u}.}\)

This is an explicit rational formula for every type's limit.

4. A uniform convergence certificate

Suppose \(B_t>0\). For each \(u\) with \(A_{tu}=1\), we have \(B_u\ge1\), and

\(\displaystyle \left|\frac{r c_u}{rB_u+\delta_u}-\frac{c_u}{B_u}\right| =\frac{c_u\delta_u}{B_u(rB_u+\delta_u)} \le\frac{c_u}{rB_u^2} \le\frac{c_u}{r}. \)

Also,

\(\displaystyle 0\le\frac{\delta_t}{rB_t+\delta_t}\le\frac1r.\)

The triangle inequality and \(\sum_u c_u=D\) now give

\(\displaystyle |\Phi_t(r)-\ell_t| \le\frac1r+\sum_{u:A_{tu}=1}\frac{c_u}{r} \le\frac{D+1}{r}.\)

For \(B_t=0\), the error is identically zero, so the same bound holds.

Consequently, a single certificate valid for all types is

\(\displaystyle \boxed{R= \max\left\{\left\lceil\frac{k}{D}\right\rceil, \left\lceil\frac{D+1}{\varepsilon}\right\rceil\right\}.}\)

Every integer \(r\ge R\) satisfies \(|\Phi_t(r)-\ell_t|\le\varepsilon\) for every \(t\).

5. Computing the requested rational approximations

Although the limits are rational, the algorithm need not materialize their exact common denominator.

Choose the least nonnegative integer \(h\) satisfying

\(\displaystyle 2^h\ge\frac{\tau}{\varepsilon}.\)

For each \(u\), compute

\(\displaystyle w_u=\left\lfloor\frac{2^h c_u}{B_u}\right\rfloor\)

when \(B_u>0\), and set \(w_u=0\) otherwise. Output

\(\displaystyle a_t=\mathbf 1_{\{B_t=0\}}+2^{-h}\sum_{u\in T}A_{tu}w_u.\)

For every \(u\) with \(B_u>0\),

\(\displaystyle 0\le\frac{c_u}{B_u}-2^{-h}w_u<2^{-h}.\)

There are at most \(\tau\) summands in each row. Therefore,

\(\displaystyle 0\le\ell_t-a_t\le\tau\,2^{-h}\le\varepsilon.\)

Thus the algorithm outputs valid rational approximations and the certified threshold from Section 4. It never constructs any \(G_r\).

6. Encoding lengths and running time

Use the usual encoding of rationals by binary integer numerators and positive denominators, and let \(L\) include the encoding of \(\varepsilon\).

First reduce the masses and compute the least common multiple \(D\) of their denominators. Since \(D\) divides their product, its binary length is \(O(L)\). Each \(c_t\) and \(B_u\) also has \(O(L)\) bits, because \(c_t\le D\) and \(B_u\le D\).

Moreover,

\(\displaystyle h=O\!\left(\log\tau+\log(1/\varepsilon)\right)=O(L).\)

All integers used to compute the \(w_u\) and \(a_t\) have \(O(L)\) bits. For example,

\(\displaystyle \sum_u w_u\le 2^h\sum_u c_u=2^hD,\)

which bounds every approximation numerator after putting it over denominator \(2^h\).

Writing \(\varepsilon=p/q\), the certificate uses the integer ceiling of \((D+1)q/p\). Hence \(R\) has \(O(L+\log k)\) bits, and \(O(L)\) bits for fixed \(k\).

A conservative implementation using schoolbook arithmetic and ordinary Euclid has the following costs:

Thus a proved polynomial bound is

\(\displaystyle \boxed{O(\tau L^3+\tau^2L)=O(mL^3+m^2L),\qquad m=\tau.}\)

In particular, this is \(O(L^4)\), since \(\tau\le L\). The output has \(O(\tau L)\) bits for fixed \(k\). These bounds include the accuracy encoding and depend on its bit length rather than its reciprocal value.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Verdict: proved. The output resolves the assigned limit-and-certification problem for every fixed \(k\ge2\). The local identity, exact replicated-graph formula, convergence certificate, approximation algorithm, and polynomial bit bound are valid. No major or minor mathematical issues were found.

1. Local payoff identity

The local value is well-defined because \(B\) is nonempty and every partition covers \(V\). Consequently, at least one coalition has a positive intersection count with \(B\).

For \(i\notin B\), transferring \(i\) preserves every positive intersection count. Creating an exit with zero intersection count cannot affect the positive maximum. If the remaining coalition disappears, its previous intersection count was zero, so its local value was already zero. Thus the assertion \(X_i^B=0\) holds in every realization, including the final departure.

The telescoping identity is correct: the post-transfer remaining coalition and partition at one departure are exactly the pre-transfer objects at the next departure. The initial local value is \(1\), and the terminal value is \(0\) by the stipulated empty-coalition convention. Therefore,
\[ \sum_{i\in V}X_i^B=1. \]

Permuting vertices within \(B\) preserves the local value, the uniform departure-order distribution, and the independent uniform exit assignments. Hence all members of \(B\) have equal expected contributions. Together with the zero contributions outside \(B\), this establishes the claimed expectation \(1/|B|\).

The lemma does not require individual realized contributions to be nonnegative, and the proof makes no such assumption.

2. Application to graph payoffs

Under full tie credit, the coalition value is precisely the sum of the local indicators for \(B=M^+(j)\). Each such set is nonempty because it contains \(j\). Finite linearity of expectation therefore applies without additional hypotheses.

Undirected adjacency gives
\[ i\in M^+(j)\quad\Longleftrightarrow\quad j\in M^+(i), \]
so both displayed forms of the finite-graph payoff identity are valid.

The cited paper’s Section 4 describes the departure process, and Section 6 uses the full-credit maximizing-coalition definition. This attribution is consistent with the [cited paper](https://aamas.csc.liv.ac.uk/Proceedings/aamas2016/pdfs/p177.pdf). The argument here is self-contained and does not depend on applying its computational theorem.

3. Replicated-graph formula

The definitions \(c_t=D\mu_t\) produce positive integers summing to \(D\).

The closed-neighborhood size
\[ d_u(r)=rB_u+\delta_u \]
correctly handles both diagonal cases:

The denominator is always positive. When \(\delta_u=0\), the diagonal entry forces \(B_u\ge c_u\ge1\); otherwise the additive term is \(1\).

The formula for \(\Phi_t(r)\) counts exactly the adjacent type classes and adds the vertex’s own contribution when required. There is neither omission nor double counting.

4. Existence and value of the limits

If \(B_t=0\), positivity of the \(c_u\) forces the entire row of \(A\) to vanish. The vertex is isolated, and the exact formula indeed gives \(\Phi_t(r)=1\).

If \(B_t>0\), the self term tends to zero. For every included neighbor type, symmetry ensures
\[ B_u\ge c_t\ge1. \]
Thus every included fraction has the stated finite limit. Passing the limit through this finite sum is justified.

The displayed formula for \(\ell_t\) handles isolated types and all possible zero row sums without dividing by zero. Every limit exists and is rational.

5. Uniform convergence certificate

The fraction subtraction is algebraically correct:
\[ \left|\frac{rc_u}{rB_u+\delta_u}-\frac{c_u}{B_u}\right| =\frac{c_u\delta_u}{B_u(rB_u+\delta_u)}. \]
For included terms, \(B_u\ge1\), so both subsequent bounds are valid. The self term is at most \(1/r\) when \(B_t>0\).

The triangle inequality gives
\[ |\Phi_t(r)-\ell_t|\le\frac{D+1}{r}. \]
For isolated types the error is zero, so the bound remains valid.

The stated integer \(R\) satisfies both the graph-admissibility requirement and the error requirement. The certificate holds for every integer \(r\ge R\), simultaneously for all supported types.

6. Rational approximation

The choice of \(h\) guarantees \(\tau2^{-h}\le\varepsilon\). Each floor operation introduces a downward error strictly smaller than \(2^{-h}\). Each row contains at most \(\tau\) included terms, so
\[ 0\le\ell_t-a_t\le\varepsilon. \]
Terms with \(B_u=0\) are correctly assigned weight zero. The isolated-type indicator is represented exactly.

Thus every reported \(a_t\) meets the requested absolute-error bound.

7. Encoding and running time

The bit-length claims are valid:

The stated arithmetic costs are conservative valid upper bounds. Computing the \(c_t\), although not separately itemized, fits within the stated preprocessing bound. Exact integer comparisons, floors, and ceilings suffice throughout.

Consequently,
\[ O(\tau L^3+\tau^2L)=O(mL^3+m^2L),\qquad m=\tau, \]
is a justified polynomial bound, including the encoding of \(\varepsilon\). The claimed \(O(L^4)\) consequence and \(O(\tau L)\) output bound also follow.

No 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.