← back to the atlas

d4-conf-aaai-2012-0380 (d4-conf-aaai-2012-0380)

Answer: Every instance admits a welfare-maximizing optimistic-core outcome, computable in time polynomial in \(m=M\), \(\tau\), and \(L\).

The anchor (named result in the paper)

Theorem 5.2 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateLet G = (N, ω, T ) be a linear bottleneck game, and let CS and x be the coalition structure and the payoff vector constructed above. Then x ∈I(CS) and (CS, x) is in the optimistic core of G.

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\), per-unit resource weights \(\omega_t\), and an explicit task list \(j=1,\ldots,M\), with distinct required type sets \(A_j\subseteq T\) and a singleton task for each type, find a welfare-maximizing allocation \(W_j\geq 0\) satisfying \(\sum_{j:t\in A_j}W_j\leq\mu_t\omega_t\), together with an optimistic-core payoff allocation. In the continuous society, a coalition may withdraw resources from any measurable submass of each type, form new task throughput, and compensate affected nondeviators according to the optimistic arbitration rule; does the allocation admit a payoff that no such coalition can profitably block, and can an allocation and such payoff be computed in time polynomial in \(\tau\), \(M\), and the input bit length?

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

A society is given by its support: a list \(T\) of \(\tau\) types with positive binary-rational masses \(\mu_t\), summing to \(1\). The support size \(\tau\) counts listed types, not possible types. Represent type \(t\) by an atomless interval of measure \(\mu_t\), with resource density \(\omega_t\geq0\). There are \(m=M\) explicitly listed tasks, with distinct nonempty required sets \(A_j\subseteq T\), revenue rates \(\pi_j\geq0\), and a singleton task \(k(t)\) for every type. All numerical input is binary rational; \(L\) is its total bit length.
For a coalition's aggregate resource vector \(r\geq0\), define \(v(0)=0\); otherwise \(v(r)=\pi_j\min_{t\in A_j}r_t\) if \(\operatorname{supp}(r)=A_j\), and \(v(r)=0\) if no such task exists. Resources may be split among finitely many coalitions, and task repetitions are allowed.
An initial allocation consists of throughputs \(W_j\geq0\) satisfying \(\sum_{j:t\in A_j}W_j\leq\mu_t\omega_t\), with welfare \(\sum_j\pi_jW_j\). Each positive-throughput task receives contribution density \(W_j/\mu_t\) from each required type \(t\).
A payoff allocation is specified by type totals \(x_{tj}\geq0\), distributed uniformly within each type: \(x_{tj}=0\) for \(t\notin A_j\), \(\sum_t x_{tj}=\pi_jW_j\), and \(\sum_jx_{tj}\geq\mu_t\omega_t\pi_{k(t)}\). Thus type \(t\)'s payoff density from task \(j\) is \(x_{tj}/\mu_t\).
A deviating coalition is any measurable set \(S\) of positive measure, with type masses \(s_t\). It may reclaim all resources from tasks wholly controlled by \(S\), use its unused resources, abandon any mixed task by withdrawing all its contributions and forfeiting its payoff there, and withdraw arbitrary measurable portions of its contributions from other mixed tasks.
For a retained mixed task, let \(d_{tj}\) be the aggregate withdrawal, so \(0\leq d_{tj}\leq s_tW_j/\mu_t\). Optimistic arbitration gives \(S\) the residual payment \(\max\{0,v(r^j-d^j)-\sum_t(1-s_t/\mu_t)x_{tj}\}\), where \(r^j_t=W_j\) for \(t\in A_j\) and is zero otherwise. The coalition may form new coalitions using its available resources and redistribute its resulting revenue and residual payments. It blocks if almost every member receives strictly more than its initial payoff density; an optimistic-core outcome admits no such block.
Does every instance admit a welfare-maximizing optimistic-core outcome, and is finding such an outcome or determining nonexistence polynomial-time solvable in \(m=M\), \(\tau\), and \(L\), or NP-hard?
Finite-agent linear bottleneck games admit a welfare-maximizing optimistic-core outcome computable in polynomial time ([verified result](https://ojs.aaai.org/index.php/AAAI/article/download/8256/8115)). A [later treatment](https://arxiv.org/pdf/1407.0420) also establishes this for finitely many players with divisible resources; it does not formulate the atomless measurable-submass model above.

Modeling choices made when packaging the task

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

Result. Every instance admits a welfare-maximizing optimistic-core outcome, and such an outcome can be computed in time polynomial in \(m=M\), \(\tau\), and \(L\).

The construction uses optimal resource prices, as in the finite-player result in [Section 7 of the later treatment](https://arxiv.org/pdf/1407.0420). The argument below proves stability directly for the stated measurable-submass model, including unequal withdrawals and withdrawals that change a task’s support.

1. Welfare optimization and resource prices. Put \(b_t=\mu_t\omega_t\), the total resource of type \(t\). Consider the primal linear program

\[ \max_{W\geq 0}\ \sum_j\pi_jW_j, \qquad \sum_{j:t\in A_j}W_j\leq b_t\quad(t\in T), \]

and its dual

\[ \min_{\gamma\geq 0}\ \sum_t b_t\gamma_t, \qquad \sum_{t\in A_j}\gamma_t\geq\pi_j\quad(j=1,\ldots,m). \]

The primal is feasible, since \(W=0\) is feasible. Its feasible region is bounded: because every \(A_j\) is nonempty, each variable satisfies \(W_j\leq\min_{t\in A_j}b_t\). The dual is feasible, for example by taking every \(\gamma_t=\max_j\pi_j\). Thus optimal solutions exist, and linear-programming strong duality applies.

Fix optimal solutions \(W\) and \(\gamma\), and define

\[ C_t=\sum_{j:t\in A_j}W_j, \qquad u_t=b_t-C_t. \]

Equality of the optimal objective values gives

\[ 0=\sum_t\gamma_tu_t+ \sum_jW_j\left(\sum_{t\in A_j}\gamma_t-\pi_j\right). \]

Every summand is nonnegative. Consequently,

\[ \gamma_tu_t=0\quad(t\in T), \qquad W_j\left(\sum_{t\in A_j}\gamma_t-\pi_j\right)=0 \quad(j=1,\ldots,m). \]

The primal also captures welfare obtainable through arbitrary finite task repetitions. Indeed, from any production coalition with resource vector \(q\) and listed support \(A_j\), retain throughput \(\min_{t\in A_j}q_t\). Summing these throughputs over repetitions gives feasible primal variables and preserves their revenue. Coalitions with unlisted support have zero revenue and can be discarded. Conversely, any feasible \(W\) is realized by the specified uniform contribution densities \(W_j/\mu_t\). Therefore the chosen allocation maximizes welfare under the model’s production rules.

2. Construction of a valid payoff allocation. Define

\[ x_{tj}= \begin{cases} \gamma_tW_j,&t\in A_j,\\ 0,&t\notin A_j. \end{cases} \]

These payments are nonnegative and have the required support. The identities above imply

\[ \sum_t x_{tj} =W_j\sum_{t\in A_j}\gamma_t =\pi_jW_j. \]

Moreover,

\[ \sum_jx_{tj}=\gamma_tC_t=\gamma_tb_t. \]

The singleton dual constraint is \(\gamma_t\geq\pi_{k(t)}\). Hence

\[ \sum_jx_{tj}\geq b_t\pi_{k(t)}, \]

which verifies individual rationality. In particular, the initial total payoff density within type \(t\) is

\[ p_t=\frac{\sum_jx_{tj}}{\mu_t} =\gamma_t\omega_t. \]

3. A valuation bound valid for every support. Write \(\gamma\cdot q=\sum_t\gamma_tq_t\). For every nonnegative resource vector \(q\),

\[ v(q)\leq\gamma\cdot q. \]

To prove this, the cases \(q=0\) and unlisted support follow from \(v(q)=0\) and \(\gamma\geq0\). Otherwise, let \(\operatorname{supp}(q)=A_j\) and \(z=\min_{t\in A_j}q_t\). Dual feasibility and nonnegativity give

\[ v(q)=\pi_jz \leq z\sum_{t\in A_j}\gamma_t \leq\sum_{t\in A_j}\gamma_tq_t =\gamma\cdot q. \]

It follows that any finite collection of new coalitions using aggregate resources at most \(a\) earns total revenue at most \(\gamma\cdot a\).

This bound also applies when withdrawal changes an existing task’s support: it does not assume that the remainder still performs the original task.

4. Stability against every measurable deviation. Fix any measurable deviating coalition \(S\) of positive measure. Let \(s_t\) be its type masses and put

\[ \alpha_t=\frac{s_t}{\mu_t}\in[0,1]. \]

For each positive-throughput initial task, write

\[ r^j_t= \begin{cases} W_j,&t\in A_j,\\ 0,&t\notin A_j, \end{cases} \qquad B^j_t=\alpha_tr^j_t. \]

Uniform contributions imply that \(B^j\) is exactly the aggregate resource vector contributed by members of \(S\) to task \(j\).

Partition the positive-throughput tasks into \(F\), the wholly controlled or abandoned tasks, and \(R\), the retained mixed tasks. A wholly controlled task that is preserved can equivalently be reproduced using its reclaimed resources and counted among the coalition’s new production.

For each \(j\in R\), let \(d^j\) be the withdrawal vector. By the stipulated withdrawal limits,

\[ 0\leq d^j\leq B^j. \]

The outsiders’ initial payment from this task is

\[ H_j=\sum_t(1-\alpha_t)x_{tj} =\gamma\cdot(r^j-B^j). \]

The preceding valuation bound gives

\[ v(r^j-d^j)-H_j \leq\gamma\cdot(r^j-d^j)-\gamma\cdot(r^j-B^j) =\gamma\cdot(B^j-d^j). \]

The final expression is nonnegative. Thus optimistic arbitration’s residual payment satisfies

\[ \max\{0,v(r^j-d^j)-H_j\} \leq\gamma\cdot(B^j-d^j). \]

This proves the required bound for arbitrary withdrawals, including those that remove types from the remaining support.

The unused resources belonging to \(S\) form the vector \(U\), where \(U_t=\alpha_tu_t\). Resources available for new production are therefore at most

\[ a=U+\sum_{j\in F}B^j+\sum_{j\in R}d^j. \]

Let \(Q\) be the coalition’s total revenue from new production and residual payments. Abandoned tasks provide no residual payment, so

\[ Q\leq\gamma\cdot a+ \sum_{j\in R}\gamma\cdot(B^j-d^j) =\gamma\cdot U+\sum_{j\in F\cup R}\gamma\cdot B^j. \]

Because \(\gamma_tu_t=0\), we have \(\gamma\cdot U=0\). Consequently,

\[ Q\leq\sum_t\alpha_t\gamma_tC_t =\sum_t\alpha_t\sum_jx_{tj} =\sum_ts_tp_t. \]

The right-hand side is exactly \(S\)’s initial aggregate payoff.

To finish, let \(f\) be any measurable payoff density obtainable after the deviation. If almost every member strictly improved, then \(h=f-p\) would be positive almost everywhere on \(S\), where \(p\) is the initial density. Since \(S\) has positive measure, some measurable set \(\{h\geq1/n\}\) has positive measure: these sets, over positive integers \(n\), cover \(S\) up to a null set. Therefore \(\int_Sh>0\), and hence

\[ \int_Sf>\int_Sp=\sum_ts_tp_t. \]

This contradicts the aggregate revenue bound. Thus no measurable coalition blocks, proving that the constructed outcome belongs to the optimistic core.

5. Polynomial-time construction. The primal has \(m\) variables and \(\tau\) resource constraints; the dual has \(\tau\) variables and \(m\) task constraints. Their incidence coefficients are explicit zeros and ones. Forming the rational products \(b_t=\mu_t\omega_t\) produces an encoding of size polynomial in \(L\).

The standard polynomial-time theorem for rational linear programming yields exact rational optimal solutions of polynomial encoding length in time polynomial in the LP dimensions and encoding length. Its hypotheses hold here by the feasibility and finite optimum verified above. Computing the products \(x_{tj}=\gamma_tW_j\) then takes polynomial time and produces a polynomial-size output.

Thus the requested search problem is polynomial-time solvable. On every input satisfying the stated hypotheses, a welfare-maximizing optimistic-core outcome exists.

⟨structured verdict parsed — rendered above⟩

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

The prover’s claim is proved. The construction establishes welfare optimality, satisfies all payoff requirements, and excludes every permitted measurable deviation. The polynomial-time claim is also justified. I found no major or minor issues requiring repair.

1. Welfare optimization and duality

The primal correctly uses total type resources \(b_t=\mu_t\omega_t\). Its constraints account for all initial task contributions.

The feasibility and boundedness checks are valid:

Thus the primal has a finite attained optimum, and the stated application of linear-programming strong duality is justified.

The displayed objective-gap identity is correct. Its terms are nonnegative by primal feasibility, dual feasibility, and nonnegativity of the variables. Consequently, both complementary-slackness identities follow individually.

The reduction from arbitrary finite production to primal throughputs is also valid. For a coalition whose resource vector has listed support \(A_j\), its throughput is at most its contribution in every required coordinate. Summing throughputs over repetitions therefore respects the resource budgets and preserves revenue. Discarding coalitions with unlisted support loses no revenue. Conversely, uniform densities realize every feasible primal solution because their total contribution density within type \(t\) is \(C_t/\mu_t\leq\omega_t\).

The welfare claim therefore covers the production rules in the task, including repetitions.

2. Payoff construction

The definition \(x_{tj}=\gamma_tW_j\) on required types gives nonnegative payments with the prescribed support.

Task budget balance follows from complementary slackness. This includes zero-throughput tasks: both their total payment and revenue are zero.

For each type, the calculation
\[ \sum_jx_{tj}=\gamma_tC_t=\gamma_tb_t \]
is correct because \(\gamma_t(b_t-C_t)=0\). The singleton dual constraint then establishes the required individual-rationality inequality.

Division by \(\mu_t\) is legitimate because every listed mass is positive. The resulting initial payoff density \(p_t=\gamma_t\omega_t\) is correct.

3. Valuation bound

The bound \(v(q)\leq\gamma\cdot q\) is proved for every nonnegative resource vector:

Distinct required sets ensure that the listed task associated with a support is unambiguous.

Summing this inequality over a finite collection of new coalitions correctly bounds their total revenue by the price of their aggregate resources. The argument does not require the valuation to be monotone under support changes. This is sufficient for the discontinuities caused by withdrawing an entire type’s contribution.

4. Resource accounting for deviations

The proof fixes an arbitrary measurable coalition of positive measure. The fractions \(\alpha_t=s_t/\mu_t\) lie in the claimed interval, and uniform initial contributions give exactly \(B_t^j=\alpha_tr_t^j\).

The partition into reclaimed or abandoned tasks and retained mixed tasks covers the permitted choices. Reproducing a preserved wholly controlled task using reclaimed resources preserves its resources and revenue, so counting it as new production is valid.

For retained mixed tasks, the stipulated bounds give \(0\leq d^j\leq B^j\). The outsiders’ payment identity
\[ H_j=\gamma\cdot(r^j-B^j) \]
follows directly from the constructed payments.

Applying the valuation bound to the remaining resource vector gives
\[ v(r^j-d^j)-H_j\leq\gamma\cdot(B^j-d^j). \]
The remaining resource vector is nonnegative. The right-hand side is also nonnegative, so taking the maximum with zero preserves the asserted upper bound on residual payment. This checks the critical optimistic-arbitration step, including unequal withdrawals and changed supports.

The available-resource bound accounts for every permitted source: unused resources, reclaimed contributions, and withdrawals from retained mixed tasks. Abandoned tasks contribute no residual payment, as required by the task.

Combining production and residual-payment bounds cancels the withdrawal terms correctly. Complementary slackness eliminates the priced unused-resource term, leaving
\[ Q\leq\sum_ts_tp_t. \]
Thus every admissible deviation has aggregate payoff at most its initial aggregate payoff. No restriction to rational masses or rational withdrawals is used.

5. Strict improvement almost everywhere

The final measure-theoretic step is valid. If a measurable payoff density strictly improves almost everywhere on a positive-measure coalition, its difference from the initial density is positive almost everywhere. The countable family of sets where that difference is at least \(1/n\) covers the coalition up to a null set; at least one such set must have positive measure.

The resulting integral difference is strictly positive. An admissible redistribution of the coalition’s finite revenue has total payment at most \(Q\), so this contradicts the aggregate bound.

This establishes the exact blocking criterion in the task, rather than merely ruling out aggregate improvements.

6. Polynomial-time construction

The invoked rational-linear-programming theorem is stated sufficiently precisely: exact rational optima of polynomial encoding length can be obtained in polynomial time for feasible rational programs with finite optimum. The preceding checks establish its hypotheses for both programs.

The dimensions depend on the explicitly listed tasks and types. Forming \(b_t\), solving the programs, and forming the payments all have polynomial bit complexity. There are at most \(m\tau\) payment entries, and the uniform densities are also finitely specified by rational quotients.

Zero resource densities, zero revenues, zero throughputs, and unused resources do not invalidate any step. Positive masses ensure that all density formulas remain defined.

Because existence is established for every valid input, determining nonexistence on the promised input domain requires no additional algorithm.

The cited [Section 7](https://arxiv.org/pdf/1407.0420) provides finite-player background; the submitted stability argument supplies the needed measurable-submass verification directly.

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.