← back to the atlas

Strategyproof Mechanisms for Additively Separable and Fractional Hedonic Games (d4-journals-jair-2021-0003)

Answer: Polynomial-time solvable; the guarantee \(W_{\mathrm{pair}}(x)\ge\tfrac12\mathrm{OPT}_\infty(\mu,V)\) is achievable and sharp among pair allocations.

The anchor (named result in the paper)

Theorem 1 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateFor symmetric fractional hedonic games, returning the coalitions induced by Mechanism M1 is a 2-approximation of the maximum social welfare.

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

The continuous mirror question, as graded

Given a finite type set \(T\), rational masses \(\mu\) with \(\sum_t\mu_t=1\), and a rational symmetric valuation matrix \(V\), define \(\mathrm{OPT}_\infty(\mu,V)=\limsup_{N\to\infty,\;N\mu\in\mathbb{Z}^T}\mathrm{OPT}(N\mu,V)/N\), where \(\mathrm{OPT}(N\mu,V)\) is maximum FHG welfare for the corresponding clone population. Compute pair masses \(x_{\{s,t\}}\) and \(x_{tt}\), with singleton remainder, satisfying \(2x_{tt}+\sum_{s\ne t}x_{\{s,t\}}\le\mu_t\) and \(W_{\mathrm{pair}}(x)=\sum_{s<t}v_{st}x_{\{s,t\}}+\sum_t v_{tt}x_{tt}\ge\frac12\mathrm{OPT}_\infty(\mu,V)\).

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

A society is given by its support: a nonempty list \(T\) of \(\tau\) types with positive binary rational masses \(\mu_t\), where \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types; \(m=\tau\) is the valuation matrix dimension, and \(L\) is the total input bit length.
The input includes a symmetric matrix \(V=(v_{st})\in([-1,1]\cap\mathbb Q)^{T\times T}\). For an integer \(N\) with \(N\mu\in\mathbb Z^T\), create \(N\mu_t\) distinct clones of type \(t\). Distinct clones of types \(s,t\) value each other at \(v_{st}\), including when \(s=t\); every clone values itself at zero.
In this fractional hedonic game, a clone \(i\) in a nonempty coalition \(C\) has utility \(u_i(C)=|C|^{-1}\sum_{j\in C\setminus\{i\}}v_{t(i),t(j)}\). Let \(\mathrm{OPT}(N\mu,V)\) be the maximum sum of utilities over all partitions into coalitions, with no stability or incentive constraints.
Define \(\mathrm{OPT}_\infty(\mu,V)=\limsup_{N\to\infty,\;N\mu\in\mathbb Z^T}\mathrm{OPT}(N\mu,V)/N\).
A pair allocation consists of nonnegative rational pair counts per unit population \(x_{\{s,t\}}\) and \(x_{tt}\), satisfying \(2x_{tt}+\sum_{s\ne t}x_{\{s,t\}}\le\mu_t\); the remaining mass forms singletons. Its welfare is \(W_{\mathrm{pair}}(x)=\sum_{s<t}v_{st}x_{\{s,t\}}+\sum_t v_{tt}x_{tt}\), using any fixed ordering of \(T\).

Does a polynomial-time algorithm in \(m,\tau,L\) always produce a feasible pair allocation with \(W_{\mathrm{pair}}(x)\ge\tfrac12\mathrm{OPT}_\infty(\mu,V)\), or is obtaining this approximation NP-hard?

For discrete symmetric fractional hedonic games, maximum-weight matching with unmatched agents as singletons gives a polynomial-time factor-\(2\) approximation; this factor is best possible among pair-and-singleton partitions ([Flammini et al., 2021](https://jair.org/index.php/jair/article/view/12107)). No result settling this exact clone-limit approximation problem was identified in the literature search.

Modeling choices made when packaging the task

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

Result

A polynomial-time algorithm always produces the required pair allocation. Specifically, optimize the pair-allocation linear program exactly. Its optimal value is at least \(\tfrac12\mathrm{OPT}_\infty(\mu,V)\). The factor is sharp, even with one type.

1. The algorithm and its complexity

Fix an ordering of \(T\). Let \(P(\mu,V)\) be the optimum of the linear program

\(\displaystyle \max_{x\ge 0}\left(\sum_{s<t}v_{st}x_{\{s,t\}}+\sum_t v_{tt}x_{tt}\right)\)

subject to, for every \(t\in T\),

\(\displaystyle 2x_{tt}+\sum_{s\ne t}x_{\{s,t\}}\le\mu_t.\)

Return an exact rational optimizer \(x^*\).

This program has \(\tau(\tau+1)/2\) variables and \(\tau\) capacity constraints. Its coefficients are rational, and its encoding length is polynomial in \(\tau\) and \(L\): the constraint coefficients belong to \(\{0,1,2\}\), while the objective coefficients and capacities come directly from the input.

The feasible region is nonempty because \(x=0\) is feasible. Summing its capacity constraints gives

\(\displaystyle 2\left(\sum_{s<t}x_{\{s,t\}}+\sum_t x_{tt}\right)\le\sum_t\mu_t=1.\)

Consequently, the feasible region is bounded. The standard polynomial-time theorem for rational linear programming therefore applies: an exact rational optimizer, with polynomial encoding length, can be computed in time polynomial in the program’s encoding length. See [MIT’s linear-programming notes](https://courses.csail.mit.edu/6.854/21/Notes/n14-LP_algorithms.html). Thus the algorithm runs in polynomial time in \(m,\tau,L\), where \(m=\tau\).

2. Converting any coalition partition into a feasible pair allocation

Fix an admissible population size \(N\), meaning \(N\mu\in\mathbb Z^T\), and an arbitrary partition \(\mathcal P\) of its clones.

For each coalition \(C\), write \(k_C=|C|\) and let \(n_t(C)\) be its number of type-\(t\) clones. Define

\(\displaystyle x^{\mathcal P}_{\{s,t\}}=\frac1N\sum_{C\in\mathcal P}\frac{n_s(C)n_t(C)}{k_C}\quad(s<t),\)

and

\(\displaystyle x^{\mathcal P}_{tt}=\frac1N\sum_{C\in\mathcal P}\frac{\binom{n_t(C)}2}{k_C}.\)

These quantities are nonnegative rational numbers. They assign weight \(1/k_C\) to each unordered pair of distinct clones within \(C\), then aggregate by type and normalize by \(N\).

Feasibility. For each type \(t\),

\(\displaystyle 2x^{\mathcal P}_{tt}+\sum_{s\ne t}x^{\mathcal P}_{\{s,t\}}=\frac1N\sum_{C\in\mathcal P}\frac{n_t(C)(n_t(C)-1)+n_t(C)\sum_{s\ne t}n_s(C)}{k_C}.\)

Since \(\sum_s n_s(C)=k_C\), this equals

\(\displaystyle \frac1N\sum_{C\in\mathcal P}n_t(C)\frac{k_C-1}{k_C}\le\frac1N\sum_{C\in\mathcal P}n_t(C)=\mu_t.\)

Hence \(x^{\mathcal P}\) is feasible. This calculation also covers singleton coalitions, whose contribution is zero.

Welfare identity. Symmetry implies that every unordered pair of distinct clones contributes twice to the sum of their coalition’s utilities. Therefore

\(\displaystyle \sum_{i\in C}u_i(C)=\frac2{k_C}\left(\sum_{s<t}v_{st}n_s(C)n_t(C)+\sum_t v_{tt}\binom{n_t(C)}2\right).\)

The diagonal term counts distinct same-type clones; it introduces no self-valuation. Summing over coalitions yields the exact identity

\(\displaystyle W_{\mathrm{pair}}(x^{\mathcal P})=\frac1{2N}\sum_{C\in\mathcal P}\sum_{i\in C}u_i(C).\)

No nonnegativity assumption on valuations was used.

Taking \(\mathcal P\) to be a welfare-maximizing partition and using optimality of \(x^*\), we obtain, for every admissible \(N\),

\(\displaystyle P(\mu,V)=W_{\mathrm{pair}}(x^*)\ge\frac{\mathrm{OPT}(N\mu,V)}{2N}.\)

3. Passing to the clone limit

Because all masses are rational, admissible population sizes include every positive multiple of a common denominator, so there are arbitrarily large admissible \(N\).

Singleton partitions have welfare zero. Moreover, each clone’s utility is at most \(1\), because all valuations are at most \(1\). Thus

\(\displaystyle 0\le\frac{\mathrm{OPT}(N\mu,V)}N\le1.\)

The limsup is consequently finite. Taking the limsup in the inequality proved above gives

\(\displaystyle W_{\mathrm{pair}}(x^*)=P(\mu,V)\ge\tfrac12\mathrm{OPT}_\infty(\mu,V).\)

The rational allocation also has an exact clone interpretation: choose \(N\) divisible by the denominators of all \(\mu_t\) and \(x^*\)-coordinates. Then the required pair counts are integers, and the capacity inequalities permit assigning distinct clones to those pairs, leaving the others as singletons. Each pair of types \(s,t\) contributes total welfare \(v_{st}\). This verifies that the output represents actual pair-and-singleton partitions along infinitely many admissible population sizes.

4. Sharpness

Take \(T=\{t\}\), \(\mu_t=1\), and \(v_{tt}=1\).

A coalition of size \(k\) has total welfare \(k-1\). Hence a partition into \(q\) coalitions has welfare \(N-q\), maximized by the grand coalition. It follows that

\(\displaystyle \mathrm{OPT}(N\mu,V)=N-1,\qquad \mathrm{OPT}_\infty(\mu,V)=1.\)

Every feasible pair allocation satisfies \(2x_{tt}\le1\), so its welfare is at most \(\tfrac12\), attained by \(x_{tt}=\tfrac12\).

Thus no pair-allocation algorithm can guarantee a fraction strictly greater than \(\tfrac12\) of the clone-limit optimum on every input.

⟨structured verdict parsed — rendered above⟩

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

Verification report

The output correctly resolves the assigned approximation problem. The proposed rational linear program has polynomial encoding length, and the partition-to-allocation construction proves the required guarantee for every admissible population size before taking the limsup. No major or minor mathematical issues were found.

The result concerns computing the requested approximation. It does not claim to compute the exact value of \(\mathrm{OPT}_\infty(\mu,V)\).

1. Algorithm, existence, and complexity

The program’s variables, objective, and capacity constraints agree exactly with the pair-allocation definition in USER_TASK. In particular, a same-type pair consumes two units of its type’s capacity, and a cross-type pair consumes one unit of each endpoint type’s capacity.

The stated variable count \(\tau(\tau+1)/2\) is correct. There are \(\tau\) capacity constraints, together with the nonnegativity constraints. All coefficients have polynomial total encoding length: the capacity matrix uses only \(0,1,2\), and the remaining rational data come from the input.

The feasibility and boundedness arguments are valid. The zero allocation is feasible. Summing the capacity constraints counts every pair variable twice, giving
\(2(\sum_{s<t}x_{\{s,t\}}+\sum_t x_{tt})\le1\).
Together with nonnegativity, this bounds every coordinate. The feasible region is also closed, so the linear objective attains its maximum.

The invoked theorem is correctly stated for this application: an explicitly encoded rational linear program with a nonempty bounded feasible region admits an exact rational optimizer of polynomial encoding length, computable in polynomial bit time. Its hypotheses are all verified in the write-up. The cited [MIT notes](https://courses.csail.mit.edu/6.854/21/Notes/n14-LP_algorithms.html) discuss polynomial-time LP algorithms, polynomial bounds on vertex encodings, and recovery of exact optimal vertices.

Consequently, the polynomial-time claim is justified. Since \(m=\tau\), there is no additional matrix-dimension parameter omitted from the analysis.

2. Construction from an arbitrary partition

For each coalition, the cross-type count \(n_s(C)n_t(C)\) counts each unordered pair of types \(s,t\) exactly once when \(s<t\). The count \(\binom{n_t(C)}2\) counts precisely the distinct same-type clone pairs.

Every coalition is nonempty, so division by \(k_C\) is valid. Since the coalition counts and \(N\) are integers, every constructed allocation coordinate is a nonnegative rational number.

The construction does not assert that these fractional weights form a matching on the original population. That assertion is unnecessary: the target permits rational pair counts per unit population.

3. Capacity verification

The displayed capacity calculation is correct. Within a coalition, the numerator for type \(t\) is
\(n_t(C)(n_t(C)-1)+n_t(C)\sum_{s\ne t}n_s(C)=n_t(C)(k_C-1)\).

Since \(k_C\ge1\), the factor \((k_C-1)/k_C\) lies in \([0,1]\). Summing therefore yields a type-\(t\) usage at most
\(N^{-1}\sum_C n_t(C)=\mu_t\).

This verifies every capacity constraint. It also covers absent types within individual coalitions and singleton coalitions, without a separate exception.

4. Welfare identity and finite-population bound

Symmetry is used correctly: each unordered pair of distinct clones contributes its valuation twice to the coalition’s total utility numerator. The common denominator is \(k_C\), exactly as required by the utility definition.

The diagonal contribution counts distinct clones of the same type. It does not include any clone’s self-valuation.

Substituting the allocation definitions therefore gives the exact identity
\(W_{\mathrm{pair}}(x^{\mathcal P})=(2N)^{-1}\sum_{C\in\mathcal P}\sum_{i\in C}u_i(C)\).
Both the factor \(2\) and the normalization by \(N\) are correct.

Negative valuations cause no problem: this is an equality, and feasibility is independent of valuations. A maximizing partition exists because the finite clone population has finitely many partitions. Applying LP optimality to its constructed allocation proves
\(P(\mu,V)\ge\mathrm{OPT}(N\mu,V)/(2N)\)
for every positive admissible \(N\).

5. Limsup and exact clone interpretation

Rational masses ensure arbitrarily large admissible population sizes through multiples of a common denominator.

The bounds on normalized optimal welfare are valid. Singletons give welfare zero. Each clone’s utility is at most \(1\), including when some valuations are negative. Thus the normalized optimum lies in \([0,1]\).

Taking the limsup preserves the established inequality because its left side is independent of \(N\). No convergence assumption or exchange of optimization and limits is needed.

The additional realization claim is also correct. At common multiples of the denominators of the masses and allocation coordinates, all population and pair counts are integers. The capacity constraints ensure enough distinct clones of every type to fill all prescribed pair endpoints. Each realized pair has total welfare equal to its valuation.

6. Sharpness

The one-type example satisfies every input restriction.

With valuation \(1\), each member of a size-\(k\) coalition receives \((k-1)/k\), so the coalition’s total welfare is \(k-1\). A partition into \(q\) coalitions consequently has welfare \(N-q\), maximized at \(q=1\), including the case \(N=1\).

Hence the normalized optimum tends to \(1\), whereas every feasible pair allocation has welfare at most \(1/2\). This establishes the claimed sharpness among pair allocations.

Required clarification or repair: None.

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