← back to the atlas

Guaranteeing Maximin Shares: Some Agents Left Behind (d4-conf-ijcai-2021-0025)

Answer: \(\mathsf P\): every valid instance admits a qualifying allocation.

The anchor (named result in the paper)

Theorem 2 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateGiven any instance of n agents, (n−1 n , 1 2(n+2 n−1))-MMS can be computed in polynomial time.

statement extracted from the paper’s text layer; consult the paper for the exact wording

The continuous mirror question, as graded

Given a finite set of additive valuation types \(T\) with distribution \( \mu \), finite indivisible good classes \(G\), per-capita supplies \(b_g\), and an integer benchmark scale \(K\), define \(q_{t,K}(b)\) as the maximum minimum value over partitions of \(K b_g\) good copies into \(K\) integral bundles. Decide whether there is a mass allocation \(x_{t,a}\ge 0\) over integral bundle configurations \(a\) satisfying \( \sum_a x_{t,a}=\mu_t \) and \( \sum_{t,a} a_g x_{t,a}=b_g \), in which at least \(1-1/K\) of the population receives value at least \( \frac{K+2}{2(K-1)}q_{t,K}(b) \).

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

A society is given by its support: a list \(T\) of \(\tau\) additive valuation 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.
There are \(m=|G|\) indivisible good classes; each type has nonnegative binary rational values \(v_{t,g}\). Supplies \(b_g>0\) are binary rationals, and the binary encoded integer \(K\ge4\) satisfies \(c_g:=Kb_g\in\mathbb Z_{>0}\) and \(\sum_g c_g>K\).
The integral bundle configurations are \(\mathcal A=\{a\in\mathbb Z_{\ge0}^{G}:a_g\le c_g\}\), including the empty bundle, with \(v_t(a)=\sum_gv_{t,g}a_g\). Configurations are implicit, not listed in the input.
Define \(q_{t,K}(b)=\max\{\min_{1\le j\le K}v_t(a^j):a^1,\ldots,a^K\in\mathcal A,\ \sum_{j=1}^{K}a^j=c\}\); empty bundles are allowed. These benchmarks are defined by the input, not supplied separately.
An allocation assigns real masses \(x_{t,a}\ge0\) satisfying \(\sum_{a\in\mathcal A}x_{t,a}=\mu_t\) and \(\sum_{t,a}a_gx_{t,a}=b_g\) for every \(g\). It qualifies when \(\sum_{t}\sum_{a:v_t(a)\ge\frac{K+2}{2(K-1)}q_{t,K}(b)}x_{t,a}\ge1-\frac1K\).

Is deciding whether a qualifying allocation exists solvable in polynomial time, or is it NP-hard? State running times in \(m\), \(\tau\), \(K\), and the total input bit length \(L\), with polynomial time measured against the binary input encoding.

For explicitly listed discrete agents and goods, a polynomial-time algorithm gives at least \(n-1\) of \(n\ge4\) agents value at least \(\frac{n+2}{2(n-1)}\) times their \(n\)-maximin share ([Hosseini and Searns](https://www.ijcai.org/proceedings/2021/0034.pdf)).
No result settling this exact continuous decision problem was identified in the literature search.

Modeling choices made when packaging the task

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

Conclusion

Every valid instance admits a qualifying allocation. Thus the decision problem is polynomial-time solvable, even when \(K\) and the supplies are binary encoded.

The key is that type masses may be split: averaging suitable allocations for finite profiles preserves both the prescribed type masses and the supplies.

1. The finite theorem applies with exactly the given benchmarks

Write \(\beta_K=(K+2)/(2(K-1))\), and form the finite set of labelled goods

\(M=\{(g,r):g\in G,\ 1\le r\le c_g\}\).

Each copy \((g,r)\) has value \(v_{t,g}\) for type \(t\). This expansion is used only for the existence proof.

A partition of \(M\) among \(K\) agents gives configurations \(a^1,\ldots,a^K\) satisfying \(\sum_j a^j=c\). Conversely, any such configuration tuple can be realized by distributing the labelled copies accordingly. Bundle values agree under this correspondence. Consequently, the finite \(K\)-maximin share of an agent of type \(t\) is exactly \(q_{t,K}(b)\).

This equality also holds if finite partitions are required to have nonempty parts. If \(q_{t,K}(b)>0\), an optimal partition already has no empty part. If \(q_{t,K}(b)=0\), a nonempty \(K\)-partition exists because \(|M|=\sum_g c_g>K\), and its minimum value is necessarily zero.

Theorem 2 of [Hosseini and Searns](https://www.ijcai.org/proceedings/2021/0034.pdf) guarantees an allocation giving at least \(K-1\) agents value at least \(\beta_K\) times their \(K\)-maximin share. Its hypotheses hold here: there are \(K\ge4\) agents, finitely many goods, more goods than agents, and nonnegative additive valuations.

Therefore, for every ordered type profile \(s=(s_1,\ldots,s_K)\in T^K\), choose an allocation with configurations \(a^1(s),\ldots,a^K(s)\) such that

\(\displaystyle \sum_{j=1}^K a^j(s)=c,\qquad \left|\{j:v_{s_j}(a^j(s))\ge\beta_Kq_{s_j,K}(b)\}\right|\ge K-1.\)

Any unallocated goods can be assigned to an agent without reducing these guarantees, since valuations are nonnegative.

2. Average over profiles

Give profile \(s\in T^K\) weight

\(\displaystyle w_s=\prod_{j=1}^K\mu_{s_j}.\)

These weights are nonnegative and sum to one because \(\sum_t\mu_t=1\).

For each type \(t\) and configuration \(a\), define

\(\displaystyle x_{t,a}=\frac1K\sum_{s\in T^K}w_s \sum_{j=1}^K\mathbf 1\{s_j=t,\ a^j(s)=a\}.\)

This is a finite, nonnegative rational allocation. We verify every required condition.

Type masses. For each position \(j\), summing the product weights over profiles with \(s_j=t\) gives \(\mu_t\). Hence

\(\displaystyle \sum_{a\in\mathcal A}x_{t,a} =\frac1K\sum_{j=1}^K\sum_{s:s_j=t}w_s =\frac1K\sum_{j=1}^K\mu_t =\mu_t. \)

Supplies. Every chosen finite allocation uses exactly \(c_g\) copies of class \(g\). Therefore

\(\displaystyle \sum_{t,a}a_gx_{t,a} =\frac1K\sum_s w_s\sum_{j=1}^K a^j_g(s) =\frac{c_g}{K}\sum_s w_s =b_g. \)

Qualifying mass. Let \(H(s)\) be the number of agents meeting their threshold in the chosen allocation for profile \(s\). By the finite theorem, \(H(s)\ge K-1\). Thus

\(\displaystyle \sum_t\sum_{a:v_t(a)\ge\beta_Kq_{t,K}(b)}x_{t,a} =\frac1K\sum_s w_sH(s) \ge\frac{K-1}{K}\sum_s w_s =1-\frac1K. \)

The constructed allocation qualifies.

The argument allows arbitrary positive rational masses; it requires no integrality assumption on \(K\mu_t\).

3. Running time under binary encoding

On inputs promised to satisfy the stated hypotheses, the decision algorithm simply returns YES:

For the last bound, validity checks include nonnegativity, positivity, \(\sum_t\mu_t=1\), integrality of each \(Kb_g\), and \(\sum_g Kb_g>K\). Intermediate integers can be kept at \(O(L)\) bits; at most \(O(L)\) elementary arithmetic operations are needed.

Thus the running time is polynomial in the binary input length, with no dependence on the numerical magnitude of \(K\) beyond its encoding length \(\log K\). In particular, it is polynomial in \(m\), \(\tau\), \(\log K\), and \(L\).

The existence proof expands goods and averages over \(\tau^K\) profiles, but the decision algorithm performs neither expansion. No exact benchmark computation or allocation construction is required to answer the stated decision question.

⟨structured verdict parsed — rendered above⟩

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

Verdict

The prover resolves the stated decision problem. The argument establishes that every valid instance admits a qualifying allocation, so returning YES is correct on the promised input domain. I found no major or minor mathematical issues.

This conclusion concerns deciding existence; the write-up does not claim a polynomial-time algorithm for constructing an allocation.

Step-by-step verification

1. Expanded goods and benchmark correspondence

Each \(c_g=Kb_g\) is a positive integer, so the labelled set \(M\) is well-defined and finite. Its size can be exponentially large in the binary input length, but the prover explicitly uses it only for existence.

Every partition of \(M\) into \(K\) bundles determines configurations satisfying \(a_g^j\ge0\), \(a_g^j\le c_g\), and \(\sum_j a_g^j=c_g\). Conversely, every configuration tuple satisfying these constraints can be realized by distributing the labelled copies of each class. Additivity makes the corresponding bundle values identical.

Thus the finite \(K\)-maximin share equals the input-defined benchmark \(q_{t,K}(b)\). In particular, this benchmark depends on the type’s valuation and the common goods, not on the other types appearing in a profile.

The treatment of nonempty partitions is also correct:

There is no discrepancy between the two partition conventions.

2. Application of the finite theorem

I checked Theorem 2 and the relevant definitions in [Hosseini and Searns](https://www.ijcai.org/proceedings/2021/0034.pdf). The theorem supplies the claimed guarantee with parameters \(\alpha=(n-1)/n\) and \(\beta=(n+2)/(2(n-1))\). The paper’s setting permits nonnegative additive valuations and assumes more goods than agents.

For every ordered profile, the instantiated hypotheses hold:

The guaranteed number of satisfied agents is at least \(\lfloor\alpha K\rfloor=K-1\). The benchmark correspondence therefore gives exactly the threshold required by the task.

The paper defines allocations as partitions of the goods. The prover’s additional observation about assigning any leftovers is valid as well: adding goods cannot lower an agent’s value under nonnegative valuations.

3. Profile weights and allocation definition

The set \(T^K\) is finite. The weights \(w_s=\prod_j\mu_{s_j}\) are nonnegative rational numbers, and their sum is \((\sum_t\mu_t)^K=1\).

Choosing one guaranteed finite allocation for each profile therefore requires only finitely many choices. Every selected bundle belongs to \(\mathcal A\).

The definition of \(x_{t,a}\) consequently gives finite, nonnegative rational coordinates. No bound on their encoding length is necessary for this existence argument.

4. Type masses

For any fixed position \(j\), the total weight of profiles having \(s_j=t\) is \(\mu_t\): the remaining coordinates contribute factors summing to one.

Summing \(x_{t,a}\) over configurations counts each position carrying type \(t\) exactly once. Averaging over the \(K\) positions gives precisely \(\mu_t\).

This verifies the prescribed type masses without requiring \(K\mu_t\) to be integral.

5. Supplies

For every profile, the selected allocation uses exactly \(c_g\) copies of class \(g\). Accordingly, the weighted average, divided by \(K\), uses \(c_g/K=b_g\).

All sums are finite, so their rearrangement is legitimate. The argument establishes the required supply equalities, rather than merely supply inequalities.

6. Qualifying mass

Expanding the definition of \(x_{t,a}\), each position contributes to qualifying mass exactly when its selected bundle meets its own type’s threshold. Hence the qualifying mass equals \(\frac1K\sum_s w_sH(s)\).

The finite theorem gives \(H(s)\ge K-1\) for every profile. Since the weights sum to one, the qualifying mass is at least \((K-1)/K=1-1/K\).

This is exactly the task’s qualification condition. Types with zero benchmarks create no exception: their threshold is zero, and all their bundles meet it.

7. Binary-encoding complexity

Once universal existence has been established, the promised decision problem needs no benchmark computation, goods expansion, or profile enumeration.

The stated bounds are correct:

The arithmetic size claim is consistent with the encoding. Products of input denominators have bit length bounded by their total encoded length; accumulating the masses therefore needs only \(O(L)\)-bit integers. Each product \(Kb_g\), and the accumulated integer supply total, likewise has \(O(L)\) bits. The checks require at most \(O(L)\) arithmetic operations.

These bounds satisfy the requested dependence on \(m\), \(\tau\), \(K\), and \(L\): the decision algorithm has no dependence on the numerical magnitude of \(K\), and reading or validation is polynomial in the binary input length.

Repair feedback

None required. The theorem application, benchmark identification, averaging identities, edge cases, and distinction between decision and construction are sufficiently justified.

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