← back to the atlas

Coalition Formation Games and Social Ranking Solutions (aamas22-00099)

Answer: Deciding existence is \(\mathrm{NP}\)-complete, and finding a stable allocation is \(\mathrm{NP}\)-hard. Both admit an exact algorithm taking \(O\!\left(\left[\sum_{j=0}^{\min\{m,\tau\}}\binom mj\right]\operatorname{poly}(m,\tau,L)\right)\) time.

The anchor (named result in the paper)

Theorem 3.2 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateLet ⊒∈T P(N ) be a power relation and let G1 = (N, (≽i)i ∈N ) be a hedonic game where the players’ preferences are defined according to relation (1). It holds that C(G1) = A(⊒).

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_t\ge0\) with \(\sum_{t\in T}\mu_t=1\), a finite template set \(\mathcal K\subseteq\mathbb Z_{\ge0}^{\tau}\setminus\{0\}\), and a total preorder \(\succcurlyeq\) on \(\mathcal K\), find \(q\ge0\) satisfying \(\sum_{a\in\mathcal K}a_tq_a=\mu_t\) for every \(t\), such that no template \(b\) has \(\sum_{a:\,b\succ a}a_tq_a>0\) for every type \(t\) with \(b_t>0\).

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

A society is given by its support \(T\): the list of its \(\tau\) types with positive binary rational masses \(\mu_t\), with \(\sum_{t\in T}\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types.
The input also explicitly lists \(\mathcal K\subseteq\mathbb Z_{\ge0}^{\tau}\setminus\{0\}\), with binary integer coordinates, and a total preorder \(\succcurlyeq\) represented by ordered indifference classes; write \(m=|\mathcal K|\) and let \(L\) be the total input bit length.
Only listed templates are admissible. All types share this ranking; \(b\succ a\) means strict preference, and indifference creates no incentive to deviate.
An allocation is \(q\in\mathbb R_{\ge0}^{\mathcal K}\) satisfying \(\sum_{a\in\mathcal K}a_tq_a=\mu_t\) for every \(t\in T\); thus template \(a\) receives type masses \(a_tq_a\).
A template \(b\) blocks \(q\) exactly when \(\sum_{a\in\mathcal K:\,b\succ a}a_tq_a>0\) for every \(t\) with \(b_t>0\): deviations may use any positive scale of \(b\). An allocation is stable if no template blocks it.

Is deciding whether a stable allocation exists in \(\mathrm P\), or is it \(\mathrm{NP}\)-hard? Is finding one when it exists polynomial-time solvable, or \(\mathrm{NP}\)-hard? State running times in \(m,\tau,L\).

For finite agents with a common total preorder on all nonempty coalitions, stable partitions are exactly those generated by repeatedly selecting a strongest remaining coalition and deleting intersecting coalitions; one partition is obtainable in polynomial time in the explicit input size. [Source](https://www.lamsade.dauphine.fr/~moretti/preprints/LMR.pdf)
No result settling this exact continuous template problem was located in the literature search.

Modeling choices made when packaging the task

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

Result

Deciding whether a stable allocation exists is \(\mathrm{NP}\)-complete. Finding one is \(\mathrm{NP}\)-hard. These statements hold even with three indifference classes, equal dyadic masses, and templates having zero–one coordinates and at most four nonzero coordinates.

Both decision and construction admit an exact algorithm with running time

\( \displaystyle O\!\left(\left[\sum_{j=0}^{\min\{m,\tau\}}\binom mj\right]\operatorname{poly}(m,\tau,L)\right). \)

Thus this is at most \(2^m\operatorname{poly}(m,\tau,L)\), and also at most \((m+1)^\tau\operatorname{poly}(m,\tau,L)\). Neither problem has a polynomial-time algorithm unless \(\mathrm P=\mathrm{NP}\).

The proofs follow.

1. Stability depends only on support

For an allocation \(q\), define its support by

\( S(q)=\{a\in\mathcal K:q_a>0\}. \)

Since every summand in the blocking condition is nonnegative,

\( \displaystyle \sum_{a:\,b\succ a}a_tq_a=0 \quad\Longleftrightarrow\quad a_t=0\text{ for every }a\in S(q)\text{ with }b\succ a. \)

Consequently, \(q\) is stable exactly when

\[ \displaystyle \forall b\in\mathcal K\;\exists t\text{ with }b_t>0: \quad a_t=0\text{ for every }a\in S(q)\text{ with }b\succ a. \tag{1} \]

In particular, if \(q\) is stable and \(p\) is another feasible allocation with \(S(p)\subseteq S(q)\), then \(p\) is stable: every zero sum witnessing the stability of \(q\) remains zero for \(p\).

2. Polynomial-size certificates

Lemma. If a stable allocation exists, then one exists with at most \(\tau\) positive entries, all rational and of polynomial encoding length.

Proof. Let \(q\) be stable. Among feasible allocations supported inside \(S(q)\), choose \(p\) with the smallest support cardinality. Such a choice exists because there are finitely many possible supports.

The columns corresponding to \(S(p)\) are linearly independent. Otherwise there is a nonzero vector \(v\), indexed by \(S(p)\), satisfying

\( \displaystyle \sum_{a\in S(p)}a\,v_a=0. \)

Replacing \(v\) by \(-v\) if necessary, assume some \(v_a>0\). Define

\( \displaystyle \varepsilon=\min_{a:\,v_a>0}\frac{p_a}{v_a}>0. \)

Then \(p-\varepsilon v\) is nonnegative, satisfies the same balance equations, and has strictly smaller support. This contradicts the choice of \(p\).

Write \(r=|S(p)|\). Linear independence gives \(r\leq\tau\), and some \(r\) rows yield a nonsingular integer matrix \(B\). The positive entries of \(p\) satisfy

\( Bp_{S(p)}=\mu_I. \)

Cramer’s rule makes them rational. To bound their encoding length, let \(D_\mu\) be the product of the denominators of the selected masses. Its bit length is \(O(L)\). Clearing these denominators and using the determinant bound

\( |\det B|\leq r!\,H^r, \)

where \(H\) bounds the absolute entries, shows that each numerator and denominator has \(O(r(L+\log(r+1)))\) bits. This is polynomial in the input length.

Finally, \(p\) is stable by support containment and (1). \(\square\)

A verifier checks the balance equations and the blocking conditions by exact rational arithmetic. Processing indifference classes from worst to best, while accumulating the type masses assigned to strictly worse classes, requires \(O(m\tau)\) arithmetic operations. The certificate bounds make the bit running time polynomial in \(m,\tau,L\).

Therefore the decision problem belongs to \(\mathrm{NP}\).

3. Reduction from satisfiability

We reduce from the standard \(\mathrm{NP}\)-complete problem of satisfiability for Boolean formulas in conjunctive normal form with at most three literals per clause.

Remove tautological clauses, repeated literals, and duplicate clauses. These operations preserve satisfiability. Every remaining clause is nonempty and contains distinct variables. Let the variables be \(v_1,\ldots,v_n\), with \(n\geq1\), and let the clauses be \(F_1,\ldots,F_c\).

Types and masses

For each variable introduce types \(x_i,y_i,z_i\), and introduce two additional types \(h,k\).

To obtain equal dyadic masses, set

\( \displaystyle D=2^{\lceil\log_2(3n+2)\rceil}, \qquad d=D-(3n+2), \qquad \sigma=\frac1D. \)

Add dummy types \(w_1,\ldots,w_d\). Every type has mass \(\sigma\), so

\( \tau=D,\qquad \sum_{t\in T}\mu_t=D\sigma=1. \)

Let \(e_t\) denote the unit vector of type \(t\).

Templates and ranking

There are three indifference classes, ordered from best to worst.

| Class | Listed templates |
|---|---|
| Top | \(A_i=e_{x_i}+e_{z_i}\), \(B_i=e_{y_i}+e_{z_i}\), for every \(i\) |
| Middle | \(G_i=e_{x_i}+e_{y_i}+e_h\), for every \(i\); and clause templates \(C_j\), defined below |
| Bottom | \(X_i=e_{x_i}\), \(Y_i=e_{y_i}\), for every \(i\); \(R=e_h+e_k\); and \(W_s=e_{w_s}\), for every dummy type |

For a literal \(\ell\), define its associated type by

\( \displaystyle s(v_i)=x_i,\qquad s(\neg v_i)=y_i. \)

The clause template is

\( \displaystyle C_j=e_h+\sum_{\ell\in F_j}e_{s(\ell)}. \)

The preprocessing ensures that clause templates have zero–one coordinates. It also ensures that they are distinct from each other and from the variable templates \(G_i\): a clause contains no variable with both signs.

Every template is nonzero and has at most four nonzero coordinates. The number of templates is

\( m=5n+c+1+d. \)

Moreover, \(D<2(3n+2)\), so both \(m\) and \(\tau\) are polynomial in the formula size. Under explicit coordinate encoding, the constructed input length is

\( L=O(m\tau+\tau\log\tau+m\log m). \)

The reduction therefore takes polynomial time.

4. What feasibility forces

Let \(q\) be any feasible allocation.

Only \(R\) contains type \(k\). Its balance equation forces

\( q_R=\sigma. \)

The templates containing \(h\) are precisely \(R\) and all middle templates. Hence the balance equation for \(h\) is

\( \displaystyle q_R+\sum_iq_{G_i}+\sum_jq_{C_j}=\sigma. \)

Substituting \(q_R=\sigma\) and using nonnegativity gives

\( q_{G_i}=q_{C_j}=0 \)

for every variable and clause template.

These middle templates receive zero mass in every feasible allocation, but they remain admissible deviations.

Write

\( u_i=q_{A_i},\qquad v_i=q_{B_i}. \)

Only \(A_i,B_i\) contain \(z_i\), so its balance equation gives

\[ u_i+v_i=\sigma. \tag{2} \]

Since all middle allocations vanish, the other two balance equations give

\[ q_{X_i}=\sigma-u_i=v_i,\qquad q_{Y_i}=\sigma-v_i=u_i. \tag{3} \]

Each dummy template has allocation \(q_{W_s}=\sigma\).

In particular, every constructed instance has a feasible allocation: take \(u_i=v_i=\sigma/2\), use (3), assign \(\sigma\) to \(R\) and every dummy template, and assign zero to all middle templates.

5. Stability is equivalent to satisfiability

Variable templates force Boolean choices

The templates strictly worse than \(G_i\) are the bottom templates. By (3), their masses of types \(x_i,y_i,h\) are respectively

\( v_i,\qquad u_i,\qquad \sigma. \)

Thus \(G_i\) blocks exactly when both \(u_i>0\) and \(v_i>0\). A stable allocation must therefore satisfy

\[ \displaystyle (u_i,v_i)\in\{(\sigma,0),(0,\sigma)\}, \tag{4} \]

because of (2).

Interpret these choices as

\( v_i\text{ is true}\quad\Longleftrightarrow\quad u_i=\sigma. \)

Here the symbol \(v_i\) in the phrase “\(v_i\) is true” denotes the Boolean variable; the allocation quantity \(v_i=q_{B_i}\) is zero in that case.

For a positive literal, the mass of its associated type assigned below the middle class is

\( q_{X_i}=v_i, \)

which is zero exactly when the literal is true. For a negative literal, that mass is

\( q_{Y_i}=u_i, \)

which is zero exactly when the negative literal is true.

Clause templates enforce satisfaction

For \(C_j\), the mass of type \(h\) assigned to strictly worse templates is \(\sigma>0\). Therefore \(C_j\) does not block exactly when at least one of its literal types has zero mass below the middle class.

Under the Boolean choices (4), this means exactly that at least one literal of \(F_j\) is true.

Consequently, every stable allocation yields a satisfying assignment.

A satisfying assignment yields stability

Conversely, given a satisfying assignment, choose

\( \displaystyle (u_i,v_i)= \begin{cases} (\sigma,0),&\text{if the Boolean variable is true},\\ (0,\sigma),&\text{if it is false}. \end{cases} \)

Use the bottom allocations prescribed by (3), assign \(\sigma\) to \(R\) and each dummy template, and assign zero to all middle templates. The preceding balance equations prove feasibility.

Every listed template is nonblocking:

The allocation is therefore stable.

This proves the equivalence

\( \displaystyle \text{the formula is satisfiable} \quad\Longleftrightarrow\quad \text{a stable allocation exists}. \)

Together with Section 2, it establishes \(\mathrm{NP}\)-completeness.

6. Search hardness and running times

The reduction also proves search hardness directly: from any stable allocation, read the Boolean choices (4) to obtain a satisfying assignment. Thus finding a stable allocation is \(\mathrm{NP}\)-hard under polynomial-time search reductions.

A polynomial-time algorithm guaranteed to return a stable allocation on every yes-instance would imply \(\mathrm P=\mathrm{NP}\). Run it for its polynomial time bound and verify its output: on a yes-instance it returns a valid allocation, while on a no-instance no output can pass verification.

For an unconditional exact algorithm, enumerate every subset \(S\subseteq\mathcal K\) of cardinality at most \(\tau\). For each subset:

\( \displaystyle \sum_{a\in S}a_tq_a=\mu_t\quad(t\in T),\qquad q_a\geq0\quad(a\in S). \)

Any feasible solution has support contained in \(S\), so (1) proves its stability. Conversely, the sparse-certificate lemma guarantees that a stable instance has a subset encountered by this enumeration.

The support check takes \(O(m\tau)\) Boolean operations by processing ranking classes from worst to best. Each linear program has at most \(\min\{m,\tau\}\) variables, \(\tau\) balance equations, and encoding length \(O(L)\), and is solvable in polynomial bit time. This proves the stated running-time bound for both decision and construction.

7. Relation to the finite-agent result

The [cited finite-agent theorem](https://www.lamsade.dauphine.fr/~moretti/preprints/LMR.pdf) assumes a ranking over all nonempty coalitions. Here admissibility is restricted to listed templates.

The reduction uses that restriction explicitly: \(k\) appears only in \(R\), forcing every middle template to receive zero allocation. Such templates nevertheless impose blocking conditions. Those conditions force discrete choices even though allocation quantities are continuous. Every reduced instance remains feasible, so the hardness concerns stability itself.

⟨structured verdict parsed — rendered above⟩

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

The argument establishes the claimed complexity classification, subject to one minor clarification about the SAT source problem. The reduction, certificate bound, and exact algorithm are sound. No major issue prevents the conclusion.

For each template \(b\) and type \(t\), every summand \(a_tq_a\) is nonnegative. Therefore the sum over strictly worse templates is zero exactly when every supported, strictly worse template has zero coordinate at \(t\).

Because every admissible template is nonzero, its set of required types is nonempty. Negating the stated blocking condition consequently gives exactly condition (1). The quantifiers are correct: each potential blocker needs at least one required type witnessing a zero sum.

The support-containment consequence also follows: removing supported templates cannot invalidate an existing zero-sum witness. This argument concerns strictly worse templates throughout and correctly excludes indifference.

A feasible allocation with minimum support among those supported inside \(S(q)\) exists: this family is nonempty, and its attainable support cardinalities form a finite set.

If its supported columns are dependent, the stated vector \(v\) exists. After the permitted sign change, at least one coordinate is positive, so the minimum defining \(\varepsilon\) is over a nonempty finite set of positive numbers.

For positive coordinates of \(v\), the choice of \(\varepsilon\) preserves nonnegativity; for negative coordinates, subtraction increases the allocation. At least one positive allocation becomes zero. The balance equations remain satisfied because the column combination with coefficients \(v\) is zero. Thus the claimed contradiction is valid.

Linear independence implies \(r\leq\tau\), and an integer matrix of column rank \(r\) has a nonsingular submatrix formed from \(r\) rows. Its subsystem uniquely determines the supported allocation, so Cramer’s rule applies.

The bit-length claim is also valid. The selected denominator product has \(O(L)\) bits, and the determinant bound contributes \(O(r\log(r+1)+r\log H)\) bits. Since the input coordinates and mass denominators have bit lengths bounded by \(L\), the asserted polynomial bound follows. Restricting the support preserves stability by the already established characterization.

The sparse rational allocation supplies a polynomial-length certificate. Exact rational arithmetic can verify nonnegativity, all balance equations, and all blocking conditions in polynomial bit time.

The worst-to-best scan gives the stated \(O(m\tau)\) arithmetic-operation count, provided each indifference class is tested before its contributions enter the accumulated masses. This is precisely what accumulating masses from *strictly* worse classes requires; the description is sufficient.

Where: Section 3, “Every remaining clause is nonempty and contains distinct variables.”

Removing tautological clauses, repeated literals, and duplicate clauses does not eliminate an empty clause. For example, a formula on one variable containing an empty clause retains that clause after all three operations.

This is a source-domain clarification, rather than a substantive defect in the hardness argument: the usual nonempty-clause SAT source is the evidently intended reading.

Minimum clarification: Explicitly state that the chosen SAT source has nonempty clauses, each containing at most three literals. Then the stated preprocessing has the asserted properties.

The requirement \(n\geq1\) is already explicit. Formulas with no clauses cause no difficulty: the variable gadgets still give three nonempty ranking classes.

There are \(3n+2+d=D\) types, each with positive dyadic mass \(1/D\), so the normalization is exact.

The template count is correctly computed as
\[ m=2n+(n+c)+(2n+1+d)=5n+c+1+d. \]

After the specified preprocessing, clause templates have zero–one coordinates and at most four nonzero coordinates. Distinct normalized clauses give distinct clause templates. A clause template cannot equal \(G_i\), because that would require both signs of the same variable in a remaining clause. The additional types and coordinate patterns distinguish the other template families.

The bound \(D<2(3n+2)\) is correct, including when \(3n+2\) is already a power of two. Thus the numbers of types and templates are polynomial in the source size. The displayed bound on explicit input length correctly accounts for coordinates, rational masses, and the ranking representation.

Only \(R\) contains \(k\), so \(q_R=\sigma\). That allocation already exhausts the entire mass of \(h\). Since every middle template contains \(h\) and allocations are nonnegative, every middle allocation must be zero.

Only \(A_i\) and \(B_i\) contain \(z_i\), giving \(u_i+v_i=\sigma\). Once the middle allocations vanish, the remaining balance equations give exactly
\[ q_{X_i}=\sigma-u_i=v_i,\qquad q_{Y_i}=\sigma-v_i=u_i. \]

Each dummy type occurs only in its singleton template. The stated allocation with \(u_i=v_i=\sigma/2\) therefore proves feasibility of every constructed instance.

This step correctly distinguishes allocation from admissibility: a middle template receiving zero allocation remains a possible blocker.

The only strictly worse class for \(G_i\) is the bottom class. Its required types have bottom masses \(v_i,u_i,\sigma\). Since \(\sigma>0\), its blocking condition is exactly \(u_i>0\) and \(v_i>0\).

Together with nonnegativity and \(u_i+v_i=\sigma\), nonblocking forces precisely the two choices in (4). No fractional intermediate choice survives.

The repeated use of \(v_i\) for a Boolean variable and an allocation quantity is explicitly disambiguated. Although cumbersome, it does not create a logical gap.

Under the forced Boolean choices, a positive literal’s associated bottom mass is zero exactly when that literal is true. The corresponding statement for a negative literal follows from \(q_{Y_i}=u_i\).

Every clause template has strictly worse mass \(\sigma>0\) at \(h\). Its nonblocking condition therefore requires at least one literal type with zero strictly worse mass. This is exactly clause satisfaction.

Consequently, every stable allocation determines a satisfying assignment.

Conversely, the allocation constructed from a satisfying assignment satisfies all balance equations. The nonblocking check covers every template family:

The equivalence needed for the polynomial many-one reduction is established.

From any stable allocation of a reduced instance, the Boolean choices can be read directly. Thus the construction transfers satisfying-assignment search to stable-allocation search.

The timeout-and-verification argument also correctly handles an algorithm guaranteed to succeed only on yes-instances. A polynomial bound on its yes-instance running time permits a polynomial timeout; on no-instances, no output can pass the exact verifier.

The rational-certificate lemma supplies the polynomially representable exact solutions needed for this computational interpretation.

Testing condition (1) for a candidate set \(S\) is sufficient even when the subsequent feasible allocation has support strictly smaller than \(S\). The support-containment property justifies this point.

Conversely, the sparse-allocation lemma guarantees that enumeration encounters a suitable set whenever a stable allocation exists.

Each feasibility problem has rational data of polynomial encoding length, at most \(\min\{m,\tau\}\) variables, and \(\tau\) balance equations. Standard polynomial-time rational linear programming therefore applies and can return an exact rational feasible point.

The number of candidate sets is
\[ \sum_{j=0}^{\min\{m,\tau\}}\binom mj. \]
Both upper bounds, \(2^m\) and \((m+1)^\tau\), are valid. The argument establishes the claimed running time for both decision and construction.

The cited result concerns a total preorder on all nonempty coalitions, with individual preferences induced by that preorder; its Theorem 3.2 gives the stated characterization. [Lucchetti–Moretti–Rea, Section 3.1](https://www.lamsade.dauphine.fr/~moretti/preprints/LMR.pdf)

The prover does not apply that theorem to the continuous problem. Its explanation of the reduction’s reliance on listed admissible templates is accurate, and the independently verified feasibility argument supports its statement that the hardness concerns stability itself.

The genuine progress is a complete hardness reduction, polynomial certificates, and a matching exact enumeration procedure. The only requested repair is an explicit nonempty-clause convention for the SAT source.

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