← back to the atlas

Stability in Online Coalition Formation (aaai24-28809)

Answer: polynomial-time solvable

The anchor (named result in the paper)

Theorem 3 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateThere exists a deterministic online algorithm, which always outputs a PO partition for strict ASHGs.

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\), a strict rational interaction matrix \(v\) with \(v_{t,t}>0\), and an adversarial finite sequence of positive rational-mass cohorts whose total mass is one, construct a deterministic online policy that irrevocably assigns each arriving cohort to an existing or new coalition so that after every prefix the typed mass partition is Pareto-optimal, where \(U_t(K)=\sum_s v_{t,s}z_s(K)\) and domination means weak improvement almost everywhere and strict improvement on positive mass.

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

A society is given by its support: the list \(T\) of the \(\tau\) types with positive mass, each with its mass \(p_t\) as a binary rational, with \(\sum_{t\in T}p_t=1\). Here \(\tau\) is the support size, not the number of possible types.
The known interaction matrix satisfies \(v\in\mathbb{Q}^{T\times T}\), \(v_{t,s}\ne0\) for every pair, and \(v_{t,t}>0\); symmetry is not required. “Strict” means nonzero entries, and coalition utilities may tie.
An adversary reveals \(m\) cohorts sequentially, each a pair \((t_i,a_i)\) with \(t_i\in T\) and positive binary-rational mass \(a_i\), satisfying \(\sum_{i:t_i=t}a_i=p_t\). The society and matrix are known initially; future cohorts and the horizon are hidden.
Each cohort consists of atomless individuals of its stated type. A deterministic online policy must immediately put the entire cohort into one existing coalition or one new coalition; it cannot split cohorts, move previous individuals, or merge previous coalitions.
A typed mass partition is a finite measurable partition of the arrived individuals into positive-mass coalitions. Write \(z_s(K)\) for the mass of type \(s\) in coalition \(K\); every type-\(t\) individual there receives \(U_t(K)=\sum_{s\in T}v_{t,s}z_s(K)\).
A partition is Pareto-optimal if no other finite measurable partition of the same arrived individuals weakly improves utility almost everywhere and strictly improves it on positive mass. Competing partitions may split cohorts and type masses arbitrarily, using real masses.
Let \(L\) be the total binary encoding length of the support, matrix, and cohort sequence; prefix utilities use arrived masses without renormalization.

Is maintaining Pareto-optimality after every prefix solvable by a deterministic online policy in time polynomial in \(m,\tau,L\), or is this computational task NP-hard?

For finite individual agents with nonzero rational pairwise values, a deterministic polynomial-time online algorithm maintains Pareto-optimality after every prefix ([source](https://arxiv.org/html/2312.09119v2)).
No result settling this exact continuous online problem was found in the search.

Modeling choices made when packaging the task

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

Result

Maintaining Pareto-optimality after every prefix is solvable by a deterministic online policy in polynomial time.

The policy extends the serial dictatorship used for finite agents in [Bullinger and Romen, Theorem 4.4 and Algorithm 2](https://arxiv.org/html/2312.09119v2#S4.SS2). The proof below establishes its validity against the arbitrary measurable mass splits allowed here.

Online policy

Maintain coalitions \(C_1,\ldots,C_k\) in creation order. Each coalition \(C_j\) has a founding type \(d_j\): the type of the cohort that created it.

When a cohort \((t,a)\) arrives:

This is deterministic and uses no information about future cohorts or the horizon.

Structure at a fixed prefix

Fix an arbitrary nonempty prefix. Write \(q_s\) for its total arrived mass of type \(s\), and let \(A=\{s\in T:q_s>0\}\).

First, all arrived cohorts of each type belong to one coalition. Indeed, suppose the first cohort of type \(s\) was assigned to \(C_j\). Every earlier founding type rejected it, whereas \(v_{d_j,s}>0\). This last inequality also holds if that cohort created \(C_j\), because then \(d_j=s\) and \(v_{s,s}>0\). On every later arrival of type \(s\), the earliest accepting founding type is consequently still \(d_j\).

In particular, founding types are distinct: a previously arrived type already has an accepting coalition and cannot create another one.

Define the sets of types remaining after successive coalitions by
\(R_1=A\) and
\(R_{j+1}=R_j\setminus S_j\), where

\[ \]
\(S_j=\{s\in R_j:v_{d_j,s}>0\}.\)

We claim that \(C_j\) contains exactly all arrived individuals whose types lie in \(S_j\).

To verify this, consider a type \(s\) assigned to \(C_h\). Its assignment gives \(v_{d_i,s}<0\) for every \(i<h\), and \(v_{d_h,s}>0\). These inequalities remain true for the final list of founding types at this prefix. Thus \(h\) is its earliest accepting index, precisely as specified by the sets \(S_j\).

Also, \(d_j\in R_j\), since all earlier founding types rejected the cohort creating \(C_j\). Positive diagonal entries give \(d_j\in S_j\) and \(q_{d_j}>0\).

Therefore each type-\(d_j\) individual in \(C_j\) receives

\(M_j=\sum_{\substack{s\in R_j\\v_{d_j,s}>0}}v_{d_j,s}q_s.\)

A coalition forced by its founding type

Consider the residual population consisting of all arrived individuals with types in \(R_j\). For any coalition \(K\) drawn from this population, \(0\leq z_s(K)\leq q_s\). Hence

\(M_j-U_{d_j}(K) =\sum_{\substack{s\in R_j\\v_{d_j,s}>0}}v_{d_j,s}\bigl(q_s-z_s(K)\bigr) +\sum_{\substack{s\in R_j\\v_{d_j,s}<0}}(-v_{d_j,s})z_s(K).\)

Every summand is nonnegative. Consequently \(U_{d_j}(K)\leq M_j\).

Because every matrix entry is nonzero, equality holds if and only if both conditions hold:

These conditions say exactly that \(K=C_j\) up to a null set: \(K\) contains the entire arrived mass of every type in \(S_j\), and no positive mass of any other residual type.

This conclusion permits arbitrary real mass splits. It does not require coalition utilities to be distinct.

Pareto-optimality proof

Let \(\mathcal P'\) be any finite measurable partition that weakly improves utility almost everywhere relative to the policy’s partition. We prove successively that \(\mathcal P'\) contains each \(C_j\), up to null sets.

For \(j=1\), some coalition \(K\in\mathcal P'\) contains positive mass of type \(d_1\), since that type has positive arrived mass and \(\mathcal P'\) is finite. All those individuals originally received \(M_1\). Their utility in \(K\) is constant, so weak improvement almost everywhere implies \(U_{d_1}(K)\geq M_1\).

The preceding bound gives the reverse inequality. Its equality characterization therefore forces \(K=C_1\) up to a null set.

Now suppose that \(C_1,\ldots,C_{j-1}\) have been forced. Remove their corresponding coalitions from both partitions, disregarding null sets. The remaining population consists exactly of the types in \(R_j\), and weak improvement almost everywhere still holds there.

Some remaining coalition contains positive mass of type \(d_j\). These individuals originally received \(M_j\), so the same argument forces that coalition to be \(C_j\) up to a null set.

Induction forces every coalition of the policy’s partition. Since these coalitions cover the arrived population, \(\mathcal P'\) coincides with that partition almost everywhere. Utilities consequently coincide almost everywhere, precluding strict improvement on positive mass.

Thus the policy’s partition is Pareto-optimal. The prefix was arbitrary, so this holds after every prefix.

Running time

Founding types are distinct, so there are at most \(\tau\) coalitions. Each arrival requires at most \(\tau\) sign lookups and one assignment. Preprocessing the rational matrix’s signs takes polynomial time in its encoding length.

Over the sequence, the policy performs \(O(m\tau)\) sign lookups and outputs one coalition index per cohort. It requires no utility computations or optimization over competing partitions. Its bit running time is therefore polynomial in \(m,\tau,L\).

⟨structured verdict parsed — rendered above⟩

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

Verification report

Verdict: proved. The output resolves the stated continuous online problem with a deterministic polynomial-time policy. The proof applies to finite measurable competing partitions with arbitrary real mass splits. No mathematical gaps or false steps were found.

Step-by-step audit

The decision uses only the arriving type, the known interaction matrix, and existing founding types in creation order. It assigns the whole cohort to exactly one existing or new coalition. It never splits cohorts, moves individuals, or merges coalitions.

Choosing the smallest accepting index makes the policy deterministic. Neither future cohorts nor the horizon are used. Each created coalition has positive mass because its founding cohort has positive mass.

Suppose the first cohort of type \(s\) enters \(C_j\). Every existing coalition with smaller index rejected it. Since entries are nonzero, rejection means \(v_{d_i,s}<0\). The accepting coalition satisfies \(v_{d_j,s}>0\); if it was newly created, this follows from \(d_j=s\) and the positive diagonal.

Founding types and their matrix entries never change. Subsequent coalitions have larger indices, so none can supersede \(C_j\) as the earliest accepting coalition. Every later cohort of type \(s\) therefore enters \(C_j\).

The deduction that founding types are distinct is valid: a type that has already arrived has an accepting coalition and cannot subsequently found another.

For a type assigned to \(C_h\), every founder with index smaller than \(h\) existed at its first assignment and rejected it. Thus its earliest positive entry in the final founding sequence is exactly at index \(h\).

Consequently, the recursively defined \(S_j\) consists exactly of the types assigned to \(C_j\). The sets are disjoint and exhaust the arrived types, because every arrived cohort was assigned somewhere.

The founding cohort of \(C_j\) was rejected by every earlier founder, so \(d_j\in R_j\). Positive diagonal entries imply \(d_j\in S_j\), and the positive founding mass implies \(q_{d_j}>0\).

Hence the stated utility
\(M_j=\sum_{\{s\in R_j:\,v_{d_j,s}>0\}}v_{d_j,s}q_s\)
is exactly the utility originally received by every arrived individual of type \(d_j\).

For any coalition \(K\) drawn from the residual population, each coordinate satisfies \(0\leq z_s(K)\leq q_s\). Expanding \(M_j-U_{d_j}(K)\) separately over positive and negative entries gives exactly the identity in the output.

Every summand is nonnegative. The sum is finite, and every coefficient occurring in it is strictly positive. Therefore equality holds precisely when every positive-entry type contributes its entire arrived mass and every negative-entry type contributes zero mass.

These coordinate conditions imply equality with \(C_j\) up to a null set: for each type in \(S_j\), the omitted mass is zero; for every other residual type, the included mass is zero. There are finitely many types, so the combined exceptional set is null.

This argument accommodates arbitrary real mass splits. It does not presume that coalition utilities are distinct. Nonzero entries are used to characterize equality in this particular upper bound, which is sufficient.

Since \(q_{d_1}>0\) and the competing partition is finite, some competing coalition contains positive mass of type \(d_1\).

All such individuals originally received \(M_1\), and their utility within the competing coalition is constant. If that utility were below \(M_1\), weak improvement would fail on positive mass. Thus weak improvement almost everywhere implies \(U_{d_1}(K)\geq M_1\).

The residual bound supplies \(U_{d_1}(K)\leq M_1\), and its equality characterization forces \(K=C_1\) up to a null set.

The induction is justified. Once earlier coalitions have been forced, disjointness of the competing partition means the remaining coalitions contain no positive mass from those earlier coalitions. Removing the corresponding coalitions therefore leaves exactly the residual population, modulo null sets. Such removal does not change coalition masses or utilities for the remaining individuals.

Since \(d_j\in R_j\) and \(q_{d_j}>0\), the same positive-mass argument applies at each induction stage. Every policy coalition is forced.

Finally, the forced coalitions cover the arrived population. A competing partition into positive-mass coalitions cannot contain any additional positive-mass coalition. Thus the two partitions coincide almost everywhere, and their utilities coincide almost everywhere. Strict improvement on positive mass is impossible.

The prefix is arbitrary, and the proof does not depend on future arrivals or completion of the society’s masses. It uses the actual prefix masses without renormalization.

A prefix with one cohort, or any prefix producing only one coalition, is covered by the first forcing step. Types not yet present are excluded through \(A\), so no positive-mass assertion is made about them.

If the empty prefix is included, its Pareto requirement is vacuous because no positive mass exists. This does not require an additional mathematical argument.

Symmetry is never used. The proof uses the founding type’s directed row of the matrix, as permitted by the task.

Distinct founding types imply at most \(\tau\) coalitions. Each arrival examines at most \(\tau\) precomputed signs and outputs one coalition index.

Rational signs can be extracted in time polynomial in the matrix’s binary encoding length. Type identifiers, indices, input parsing, and output writing also have polynomial bit cost. The policy needs no arithmetic on prefix utilities and no optimization over real partitions.

Thus the claimed \(O(m\tau)\) sign-lookups bound supports polynomial total bit running time in \(m,\tau,L\).

Citation and repair requirements

The attribution to the finite-agent serial dictatorship agrees with [Bullinger and Romen, Theorem 4.4 and Algorithm 2](https://arxiv.org/html/2312.09119v2#S4.SS2). The continuous conclusion is established by the supplied proof itself; it does not rely on applying the finite-agent theorem to an atomless population.

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.