← back to the atlas

d4-conf-atal-2011-0331 (d4-conf-atal-2011-0331)

Answer: Polynomial-time solvable in \(\tau,k,L\) by setting \(x_{tj}=\mu_t/k\). A succinct solution is computable in polynomial time in \(L\); explicit output necessarily depends on \(k\).

The anchor (named result in the paper)

Theorem 2 — class: hardness

The continuous mirror question, as graded

Given a finite type set \(T\), rational masses \(\mu_t\), symmetric rational weights \(w_{ts}\), an integer \(k\ge2\), and a rational threshold \(\theta\in[0,1)\), find a rational allocation \(x_{tj}\ge0\) to at most \(k\) teams with \(\sum_j x_{tj}=\mu_t\). Define \(U_t(j)=\sum_s w_{ts}x_{sj}\) and \(q_t(j)=\frac{\sum_{s:w_{ts}<0}x_{sj}}{\sum_{s:w_{ts}\ne0}x_{sj}}\), taking \(q_t(j)=1\) when the denominator is zero. Require that for every type \(t\) with \(x_{tj}>0\), no available destination \(\ell\)—including an empty team if fewer than \(k\) teams are occupied—has both \(U_t(\ell)>U_t(j)\) and \(q_t(j)\ge\theta\).

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\), normalized by \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types.
Input also includes symmetric weights \(w_{ts}=w_{st}\in\mathbb Q\), allowing either sign and zero, an integer \(k\ge2\), and a rational threshold \(\theta\in[0,1)\). Diagonal weights describe interactions between distinct individuals of the same type and may be nonzero.
An allocation consists of rational masses \(x_{tj}\ge0\), for \(1\le j\le k\), with \(\sum_jx_{tj}=\mu_t\). A team is occupied exactly when \(\sum_tx_{tj}>0\).
Define \(U_t(j)=\sum_sw_{ts}x_{sj}\) and \(q_t(j)=\frac{\sum_{s:w_{ts}<0}x_{sj}}{\sum_{s:w_{ts}\ne0}x_{sj}}\), setting \(q_t(j)=1\) when its denominator is zero.
Deviations are by infinitesimal individuals, so these quantities are evaluated at the current allocation. Every occupied team is an available destination, and an empty team is available whenever fewer than \(k\) teams are occupied; there is no entry restriction.
An allocation is vote-out stable if, for every \(t,j\) with \(x_{tj}>0\), no available destination \(\ell\) satisfies both \(U_t(\ell)>U_t(j)\) and \(q_t(j)\ge\theta\). Utility ties do not permit deviations.

Is finding a rational vote-out stable allocation solvable in polynomial time, or is it NP-hard as a search problem? State running times in \(\tau,k,L\), where \(L\) is the total binary input length; this model has no separate \(m\) parameter.

For finite indivisible agents with symmetric additive utilities, finding a vote-out stable partition into at most \(k\) teams is PLS-complete for every fixed \(k\ge2\) and threshold \(0\le\theta<1\); stable partitions always exist. [Gairing and Savani](https://arxiv.org/html/1509.05322#S7.Thmtheorem2)
No result settling this exact continuous mass-allocation problem was located.

Modeling choices made when packaging the task

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

Conclusion

Equal splitting gives an exact rational vote-out stable allocation for every input. The algorithm runs in time polynomial in \(\tau,k,L\).

When \(k\) is binary encoded, an explicit output can have exponential length in \(L\). This is an output-size issue; the allocation has a succinct description computable in polynomial time in \(L\).

Construction and proof

For every type \(t\in T\) and team \(j\in\{1,\ldots,k\}\), set \(x_{tj}=\mu_t/k\).

These masses are positive and rational. They satisfy \(\sum_{j=1}^{k}x_{tj}=\mu_t\), so the allocation is feasible. Every team has total mass \(\sum_t x_{tj}=1/k>0\). Thus all \(k\) teams are occupied, and no empty team is available.

For every type \(t\) and every team \(j\), its utility is
\[ U_t(j)=\sum_s w_{ts}\frac{\mu_s}{k} =\frac{1}{k}\sum_s w_{ts}\mu_s. \]
This expression does not depend on \(j\). Consequently, for every available destination \(\ell\), we have \(U_t(\ell)=U_t(j)\). The required strict inequality \(U_t(\ell)>U_t(j)\) never holds.

Therefore the allocation is vote-out stable, regardless of the voting fractions, threshold, signs of the weights, or diagonal weights.

This construction uses precisely the permitted splitting of types and the exclusion of utility ties from profitable deviations.

Running time

Write each input mass as \(\mu_t=a_t/b_t\), with positive integers \(a_t,b_t\). Output \(x_{tj}=a_t/(kb_t)\).

Both integers in each output fraction have bit length \(O(L)\), since the binary encoding of \(k\) is included in \(L\). Unreduced fractions represent rational numbers exactly.

Using elementary integer multiplication, computing the denominators once per type and writing all entries takes \(O(\tau L^2+\tau kL)\) bit operations. The explicit output has length \(O(\tau kL)\). Hence the running time is polynomial in \(\tau,k,L\). The succinct instruction \(x_{tj}=\mu_t/k\) has polynomial length in \(L\).

Why the dependence on \(k\) is necessary

Consider the valid instance with one type, mass \(\mu_1=1\), and weight \(w_{11}=-1\). Let \(y_j=x_{1j}\).

In every occupied team, \(U_1(j)=-y_j<0\) and \(q_1(j)=1\).

If fewer than \(k\) teams are occupied, an empty team is available and offers utility zero. Since \(1\ge\theta\), this gives an allowed strictly improving deviation. Thus every stable allocation must occupy all \(k\) teams.

If two occupied teams have \(y_j>y_\ell\), then \(-y_\ell>-y_j\), again giving an allowed strictly improving deviation. Therefore all masses must be equal, and their sum forces \(y_j=1/k\) for every \(j\).

An explicit stable allocation consequently requires at least \(k\) entries even in this one-type instance. Taking \(k=2^r\) gives input length \(L=O(r)\), so polynomial time in \(L\) alone is impossible for expanded output. Under the requested dependence on \(\tau,k,L\), equal splitting completely resolves the problem.

⟨structured verdict parsed — rendered above⟩

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

The output fully resolves the task under the requested running-time dependence on \(\tau,k,L\). The construction is correct, the stability proof is complete, and the distinction between explicit and succinct output is justified. No mathematical or complexity gaps were found.

\[ \sum_t x_{tj}=\frac{1}{k}>0. \]
Hence all \(k\) teams are occupied. The assertion that no empty team is available is correct: there are no empty teams among the \(k\) team labels.

\[ U_t(j)=\frac{1}{k}\sum_s w_{ts}\mu_s. \]
This is independent of \(j\), for every type \(t\). The calculation includes diagonal terms and permits negative, positive, and zero weights. It correctly uses utilities evaluated at the current allocation, as required for infinitesimal deviations.

\[ O(\tau L^2+\tau kL) \]
is valid for explicit output. Unreduced fractions suffice under the task’s rational-output requirement. The succinct formula also has polynomial description length and is computable in polynomial time in \(L\).

The binary encoding caveat does not undermine the result: the task expressly requests running times in \(\tau,k,L\), and the prover states the representation limitation accurately. No additional 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.