← back to the atlas

d4-conf-ijcai-2021-0414 (d4-conf-ijcai-2021-0414)

Answer: Every instance admits a \(2\)-improvement-core stable allocation. Existence decision and construction are polynomial-time solvable; a stable allocation with at most \(\tau\) templates is computable in \(O(\tau^3L^2)\) bit operations.

The anchor (named result in the paper)

Theorem 6 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateEvery S-FHG admits a k-improvement core sta- ble coalition structure that can be computed in polynomial time, for every k ≥2(1 −1/n).

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\) summing to \(1\), and a symmetric nonnegative rational affinity matrix \(W\), does every instance admit, and can one compute in time polynomial in \(|T|\) and the input bit length, a finite-support allocation that is \(2\)-improvement-core stable? Represent an allocation by masses \(\alpha_q\) assigned to finite coalition templates \(q\in\mathbb{Z}_{\ge 0}^{T}\setminus\{0\}\), with \(\sum_q \alpha_q q_t/|q|=\mu_t\); a type-\(t\) member in template \(q\) has utility \(u_t(q)=(\sum_s W_{ts}q_s-W_{tt})/|q|\). A blocker may draw either finitely many members or positive mass from source cohorts \((q,t)\); in both cases, every participant must receive strictly more than twice their utility in that source cohort. For a positive-mass block drawing \(y_{q,t}\le\alpha_q q_t/|q|\), its type-\(t\) utility is \(\sum_s W_{ts}y_s/\sum_s y_s\), where \(y_s=\sum_q y_{q,s}\); the diagonal affinity applies to other members of the same type, while an individual’s self-value is zero.

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. The affinity matrix \(W\in\mathbb{Q}_{\ge0}^{T\times T}\) is symmetric; \(L\) is the total input bit length. There is no separate \(m\) parameter; state running times in \(\tau,L\).
An allocation is a finite list of templates \(q\in\mathbb{Z}_{\ge0}^{T}\setminus\{0\}\) with positive rational masses \(\alpha_q\), encoded in binary, satisfying \(\sum_q\alpha_q q_t/|q|=\mu_t\), where \(|q|=\sum_tq_t\). Cohort \((q,t)\) has mass \(a_{q,t}=\alpha_q q_t/|q|\) and, when \(q_t>0\), utility \(u_t(q)=(\sum_sW_{ts}q_s-W_{tt})/|q|\). Each positive cohort contains arbitrarily many distinct individuals; diagonal affinities value other individuals of the same type, while self-value is zero.
A finite deviation selects counts \(b_{q,t}\in\mathbb{Z}_{\ge0}\), with \(b_{q,t}=0\) whenever \(a_{q,t}=0\). Write \(b_t=\sum_qb_{q,t}\) and require \(|b|=\sum_tb_t>0\); each selected type-\(t\) individual receives \((\sum_sW_{ts}b_s-W_{tt})/|b|\). There is no count bound within a positive cohort.
A positive-mass deviation selects real masses \(0\le y_{q,t}\le a_{q,t}\), with \(y_t=\sum_qy_{q,t}\) and \(Y=\sum_ty_t>0\); participating type-\(t\) individuals receive \(\sum_sW_{ts}y_s/Y\). Either deviation blocks precisely when its utility is strictly greater than \(2u_t(q)\) for every contributing cohort \((q,t)\). An allocation is \(2\)-improvement-core stable if neither kind blocks.

Does every instance admit such an allocation? Is deciding existence and computing a stable allocation when one exists polynomial-time solvable in \(\tau,L\), or NP-hard?

For finite societies with \(n\ge2\), symmetric nonnegative affinities and zero self-values, a stable partition exists and is computable in polynomial time for every improvement factor \(k\ge2(1-1/n)\), hence for \(k=2\). [Verified discrete result](https://www.ijcai.org/proceedings/2021/0026.pdf). No result settling exactly the continuous model above was located.

Modeling choices made when packaging the task

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

Result. Every instance admits a \(2\)-improvement-core stable allocation. A stable allocation with at most \(\tau\) templates, all of size \(2\), can be computed in \(O(\tau^3L^2)\) bit operations. Thus existence always holds, and construction is polynomial-time solvable.

The construction adapts the maximum-affinity pairing idea in Theorem 6 of the [cited discrete paper](https://www.ijcai.org/proceedings/2021/0026.pdf). The proof below directly covers both deviation notions in the stated continuous model.

1. Construction

Let \(e_t\) denote the unit vector for type \(t\). Initialize residual masses \(r_t=\mu_t\). At each stage, let \(A=\{t:r_t>0\}\). If \(A\) is empty, stop. Otherwise, choose \(s,t\in A\), allowing \(s=t\), maximizing \(W_{st}\). Write \(M=W_{st}\).

Every added mass is positive. Every stage exhausts at least one active type, so there are at most \(\tau\) stages.

For a cross-type template, each of its two cohorts has mass \(\alpha_q/2=\delta\). For a same-type template, its sole cohort has mass \(\alpha_q=r_t\). Thus the mass assigned to each type equals its decrease in residual mass. At termination, all residual masses are zero, proving

\(\displaystyle \sum_q\alpha_q\frac{q_t}{|q|}=\mu_t\qquad\text{for every }t\in T.\)

Consequently, the output is a valid allocation.

Every cohort created at a stage with selected affinity \(M\) has utility exactly \(M/2\). Indeed, for \(q=e_s+e_t\) with \(s\ne t\),

\(\displaystyle u_s(q)=\frac{W_{ss}+W_{st}-W_{ss}}2=\frac M2,\)

and symmetry gives \(u_t(q)=M/2\). For \(q=2e_t\),

\(\displaystyle u_t(q)=\frac{2W_{tt}-W_{tt}}2=\frac M2.\)

In particular, the diagonal subtraction is respected exactly.

2. The earliest participating cohort

Index the stages by \(j\), and write \(A_j\), \(M_j\), and \(q^{(j)}\) for their active sets, selected affinities, and templates. By construction,

\(\displaystyle W_{vs}\le M_j\qquad\text{for every }v,s\in A_j.\)

Also, the active sets only shrink. Therefore, every type appearing in a template created at stage \(i\ge j\) belongs to \(A_j\).

Consider any proposed deviation of either kind. Let \(j\) be the earliest stage whose template supplies a contributing cohort, and choose a type \(v\) contributing from \(q^{(j)}\). Its current utility is \(M_j/2\).

Every participating type \(s\) contributes from some stage \(i\ge j\), hence belongs to \(A_j\). Since \(v\in A_j\), it follows that \(W_{vs}\le M_j\) for every participating type.

3. Neither deviation notion blocks

For a positive-mass deviation, the selected cohort of type \(v\) receives

\(\displaystyle \frac{\sum_sW_{vs}y_s}{Y}\le\frac{\sum_sM_jy_s}{Y}=M_j=2u_v(q^{(j)}).\)

This contradicts the strict improvement required for blocking.

For a finite deviation, write \(N=|b|>0\). Since \(W_{vv}\ge0\), the selected type-\(v\) individuals receive

\(\displaystyle \frac{\sum_sW_{vs}b_s-W_{vv}}N\le\frac{\sum_sM_jb_s}N=M_j=2u_v(q^{(j)}).\)

Again, strict improvement fails for a contributing cohort.

These bounds impose no count restriction and no additional restriction on selected masses. They therefore exclude every deviation allowed in the question. The constructed allocation is \(2\)-improvement-core stable.

4. Encoding and running time

For the mass calculations, write each input mass as \(\mu_t=p_t/d_t\), and use the common denominator \(D=\prod_td_t\). Its binary length is \(O(L)\), because the sum of the input denominator lengths is at most \(L\).

Represent residual masses by integers \(R_t=Dr_t\). A cross-type stage uses \(h=\min\{R_s,R_t\}\), outputs mass \(2h/D\), and subtracts \(h\) from both residual numerators. A same-type stage outputs \(R_t/D\) and clears that numerator. All numerators remain between \(0\) and \(D\): each output mass is at most the total residual mass, which is at most \(1\). Hence every output mass has encoding length \(O(L)\).

There are at most \(\tau\) stages. Scanning the active matrix entries costs \(O(\tau^2)\) rational comparisons per stage. Each comparison costs \(O(L^2)\) bit operations using ordinary integer arithmetic. Common-denominator initialization and residual updates also fit within the resulting bound \(O(\tau^3L^2)\).

The output has at most \(\tau\) templates, each with entries in \(\{0,1,2\}\), and total encoding length \(O(\tau^2+\tau L)\). No expansion into a finite population is needed.

⟨structured verdict parsed — rendered above⟩

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

Verdict

The prover resolves the task correctly. The construction produces a valid allocation, excludes both permitted deviation notions, and has the claimed polynomial bit complexity. No major or minor mathematical issues were found.

Step-by-step verification

1. Construction and termination

The maximization is well-defined whenever the active set is nonempty: it is a finite set, and diagonal choices are permitted.

In a cross-type stage, both residual masses are positive, so \(\delta>0\). Subtracting their minimum preserves nonnegativity and exhausts at least one type. In a same-type stage, the positive residual mass is assigned completely and that type is exhausted.

Consequently, the algorithm terminates after at most \(\tau\) stages, with every residual mass zero. Every output template is nonzero, integral, nonnegative, and has size \(2\); every output mass is positive and rational.

The template indexing by stage is unambiguous. A cross-type template cannot recur because at least one of its two types is exhausted when it is created. A same-type template cannot recur because its type is exhausted immediately.

2. Allocation feasibility

For a cross-type template, the assigned mass of each participating type is \((2\delta)/2=\delta\), exactly its residual decrease. For a same-type template, the assigned type mass is \(\alpha_q(2/2)=r_t\), again exactly its residual decrease.

Thus the stated conservation identities hold for every type. They also imply that the total template mass is \(1\). The construction satisfies the allocation definition exactly.

3. Current cohort utilities

The utility computations are correct.

For a cross-type template, the diagonal contribution cancels the self-value subtraction, giving the first type utility \(W_{st}/2\). Symmetry gives the other type the same utility.

For a same-type template, the numerator is \(2W_{tt}-W_{tt}=W_{tt}\), giving utility \(W_{tt}/2\). This correctly values the other same-type individual while excluding self-value.

Therefore every cohort created at stage \(j\) has utility \(M_j/2\).

4. Earliest participating cohort

Every permitted nonempty deviation has a contributing cohort, so an earliest contributing stage exists.

All participating types occur in templates created at that stage or later. Since the active sets only shrink, all those types belong to \(A_j\). The chosen witness type \(v\) also belongs to \(A_j\).

The stage maximization therefore supplies the required bound \(W_{vs}\le M_j\) for every participating type \(s\), including \(s=v\). This argument remains valid when a type has cohorts in several templates: the earliest stage is selected among contributing cohorts, not among types.

5. Positive-mass deviations

The denominator \(Y\) is positive by definition. All participating masses are nonnegative, so the affinity bounds imply that the witness cohort's deviation utility is at most \(M_j\).

Its blocking threshold is exactly \(2u_v(q^{(j)})=M_j\). Hence this contributing cohort fails the required strict inequality.

The argument applies to every admissible real mass selection. It needs no assumption about rationality or a positive lower bound on selected masses.

6. Finite deviations

The denominator \(N\) is positive by definition. Nonnegative counts and the affinity bounds give \(\sum_sW_{vs}b_s\le M_jN\). The assumption \(W_{vv}\ge0\) justifies discarding the subtracted diagonal term when taking an upper bound.

Thus the witness cohort's deviation utility is at most \(M_j\), again preventing strict improvement beyond its blocking threshold.

No cohort count bound is introduced. The argument covers the arbitrary finite counts permitted by the task.

7. Edge cases

The proof covers all relevant boundary cases:

8. Encoding and running time

The common denominator \(D=\prod_td_t\) has binary length \(O(L)\). Every initial residual numerator is an integer because each \(d_t\) divides \(D\).

Residual updates preserve integral numerators between \(0\) and \(D\). In a cross-type stage, \(2h\le R_s+R_t\le D\), so the output numerator also has the claimed bound. Same-type output numerators are already bounded by \(D\). Thus each output mass has encoding length \(O(L)\).

There are at most \(\tau\) stages and \(O(\tau^2)\) rational comparisons per stage. Comparing input affinities by integer cross-products costs \(O(L^2)\) bit operations with ordinary arithmetic. Common-denominator initialization and residual updates fit within the claimed total \(O(\tau^3L^2)\).

The output-length estimate \(O(\tau^2+\tau L)\) is valid for dense template vectors. No finite-population expansion is used.

9. Role of the cited theorem

The maximum-affinity pairing attribution agrees with the algorithm in Theorem 6 of the [cited paper](https://www.ijcai.org/proceedings/2021/0026.pdf). The continuous conclusion does not rely on applying that finite-society theorem: the prover supplies a direct argument for both continuous-model deviation notions. There is therefore no unverified theorem application.

Repair feedback

None required. The proof establishes universal existence and polynomial-time construction on the promised input domain; existence decision consequently always returns yes.

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