← back to the atlas

Fair Division Under Cardinality Constraints (d4-conf-ijcai-2018-0652)

Answer: Polynomial-time solvable: the \(1/3\) guarantee is universally achievable, with exact allocation of every supply and polynomial-size sparse output.

The anchor (named result in the paper)

Theorem 2 — class: algorithmic

The continuous mirror question, as graded

Given valuation types \(t\) with masses \(\mu_t\), good types \(q\) partitioned into categories \(\mathcal Q_h\), cardinality limits \(k_h\), and per-capita supplies \(\lambda_q\), let \(\mathcal B\) be the integral bundles satisfying \(\sum_{q\in\mathcal Q_h}b_q\le k_h\). Compute a mass assignment \(x_{t,b}\) satisfying \(\sum_b x_{t,b}=\mu_t\) and \(\sum_{t,b}b_qx_{t,b}=\lambda_q\), together with the largest \(\alpha\) such that every used bundle satisfies \(v_t(b)\ge\alpha z_t^\infty\), where \(z_t^\infty=\max_\rho\min_{\rho_b>0}v_t(b)\) over distributions \(\rho\) on \(\mathcal B\) with the same per-capita supplies; decide whether \(\alpha\ge 1/3\).

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

A society is given by its support: \(\tau\) valuation types with positive binary-rational masses \(\mu_t\), where \(\sum_t\mu_t=1\); \(\tau\) counts supported types, not all possible types.
There are \(m\ge1\) good types, partitioned into nonempty categories \(\mathcal Q_1,\ldots,\mathcal Q_\ell\), with integer limits \(k_h\ge0\). Values \(v_{tq}\ge0\) and per-capita supplies \(\lambda_q\ge0\) are binary rationals; assume \(\sum_{q\in\mathcal Q_h}\lambda_q\le k_h\) for every category.
Bundles contain integral numbers of copies: \(\mathcal B=\{b\in\mathbb Z_{\ge0}^{m}:\sum_{q\in\mathcal Q_h}b_q\le k_h\text{ for every }h\}\), with additive value \(v_t(b)=\sum_qv_{tq}b_q\).
Let \(\mathcal D(\lambda)=\{\rho\in\mathbb R_{\ge0}^{\mathcal B}:\sum_b\rho_b=1,\ \sum_b b_q\rho_b=\lambda_q\text{ for every }q\}\) and define \(z_t^\infty=\max_{\rho\in\mathcal D(\lambda)}\min_{b:\rho_b>0}v_t(b)\).
A feasible mass assignment has \(x_{t,b}\ge0\), \(\sum_bx_{t,b}=\mu_t\), and \(\sum_{t,b}b_qx_{t,b}=\lambda_q\); thus all supplies are allocated. It provides factor \(\alpha\ge0\) when \(x_{t,b}>0\) implies \(v_t(b)\ge\alpha z_t^\infty\).
Let \(L\) be the total binary input length; state running times in \(m,\tau,\ell,L\), and the limits \(k_h\).

Is the \(1/3\) guarantee universally achievable by an algorithm polynomial in the binary input size that computes a feasible mass assignment with \(v_t(b)\ge z_t^\infty/3\) for every used bundle, or can this guarantee fail existentially or computationally?

For finite agents and indivisible goods, nonnegative additive valuations and feasible category limits admit a polynomial-time \(1/3\)-MMS allocation, using the constrained MMS benchmark ([Biswas–Barman](https://www.ijcai.org/Proceedings/2018/0013.pdf)).
No result settling the exact distributional model above was identified in the literature search.

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

1. Proven result. The guarantee is universally achievable in polynomial time in the binary input size. In fact, the construction below achieves factor \(\frac{729}{2000}>\frac13\).

The assignment is returned sparsely, as a list of nonzero entries \((t,b,x_{t,b})\). It uses at most \(\tau+m\) such entries. Its running time is

\[ (m+1)^{10}\operatorname{poly}\!\left(m,\tau,\ell,L,\sum_{h=1}^{\ell}\log(k_h+1)\right) \]

bit operations. Thus the dependence on each limit is through its binary encoding, not its numerical value.

The proof uses a stronger finite-agent result than the supplied \(\frac13\) theorem: Hummel–Hetland’s Theorem 5 gives a feasible allocation attaining factor \(\frac{n}{2n-1}\), hence at least \(\frac12\), of constrained MMS. Its setting has nonnegative additive valuations, category limits, and allocation of every item. [Hummel–Hetland, *Maximin shares under cardinality constraints*, Theorem 5](https://link.springer.com/article/10.1007/s10458-026-09731-1)

We use that theorem only to prove existence. The algorithm below never expands the population or the supplies.

2. Exact transfer of the finite existence theorem. Let

\[ P=\left\{u\in\mathbb R_{\ge0}^{m}:\sum_{q\in\mathcal Q_h}u_q\le k_h\text{ for every }h\right\}. \]

Each category contributes a simplex whose vertices are integral: zero and the vectors placing all \(k_h\) copies on one good type. Therefore \(P=\operatorname{conv}(\mathcal B)\). The supply hypothesis implies \(\lambda\in P\), so \(\mathcal D(\lambda)\) is nonempty.

For a type \(t\), every distribution’s minimum supported value belongs to the finite set \(\{v_t(b):b\in\mathcal B\}\). Consequently \(z_t^\infty\) is attained. Moreover, there is a rational attaining distribution \(\rho^{(t)}\): restrict the defining linear system to bundles satisfying \(v_t(b)\ge z_t^\infty\), and take a rational basic feasible solution.

Choose a positive integer \(N\) clearing the denominators of all masses, supplies, and the distributions \(\rho^{(t)}\). Construct a finite instance with:

Categories containing no items may be omitted. If there are no items at all, every benchmark is zero and the empty assignment solves the problem.

For each \(t\), the counts \(N\rho_b^{(t)}\) describe a partition of these items into \(N\) feasible bundles, each worth at least \(z_t^\infty\) to \(t\). Indeed, their total number is \(N\), and their total count of each good type is \(N\lambda_q\). Labeled copies can therefore be assigned to these bundles exactly.

Conversely, any feasible partition into \(N\) bundles induces a distribution in \(\mathcal D(\lambda)\) by giving each bundle probability \(1/N\). Hence the constrained finite MMS of every agent of type \(t\) is exactly \(z_t^\infty\).

The finite \(\frac12\) theorem applies: valuations are nonnegative and additive, and the displayed partitions verify feasibility. Aggregating its allocation by type and bundle gives a mass assignment satisfying

\[ x_{t,b}>0\quad\Longrightarrow\quad v_t(b)\ge \frac12z_t^\infty. \]

This proves universal existence of a \(\frac12\) assignment. Clearing denominators alone does not give the required binary-polynomial algorithm; the next steps supply it.

3. A polynomial bundle oracle with value loss and no cost loss. Fix \(\varepsilon=\frac1{10}\). For a nonnegative additive valuation \(v\), threshold \(a\ge0\), and arbitrary rational prices \(p\in\mathbb Q^m\), we construct an oracle with the following properties:

\[ p\cdot b\le \min\{p\cdot c:c\in\mathcal B,\ v(c)\ge a\}. \]

Prices may have either sign. This is essential for preserving supplies as equalities later.

For \(a=0\), minimize \(p\cdot b\) directly: in each category, allocate its entire capacity to a cheapest type if that price is negative, and otherwise allocate nothing.

Suppose \(a>0\). Call a good type *large* if \(v_q>\varepsilon a\), and *small* otherwise. Enumerate all integer vectors \(h\), supported on large types, with \(\sum_qh_q\le10\), discarding those violating a category limit.

If \(\sum_qh_q=10\), then \(v(h)>a\). Find a cheapest integral extension of \(h\). This is again done category by category: fill the remaining capacity with a cheapest negative-price type, or leave it unused. Record that extension.

If \(\sum_qh_q<10\), fix the large-type coordinates exactly to \(h\), and permit only small types in the remainder. Solve the linear program

\[ \min p\cdot(h+u) \]

subject to

\[ u\ge0,\qquad \sum_{\substack{q\in\mathcal Q_h\\q\text{ small}}}u_q \le k_h-\sum_{q\in\mathcal Q_h}h_q,\qquad v(h+u)\ge a. \]

Skip this vector \(h\) if the program is infeasible. Otherwise obtain an optimal vertex.

To justify rounding that vertex, let \(Q\) be the product of the residual category simplices, before imposing the value inequality. Its vertices are integral. A vertex of \(Q\cap\{u:v(h+u)\ge a\}\) is either a vertex of \(Q\), or lies on an edge of \(Q\). Indeed, if its smallest containing face in \(Q\) had dimension at least two, one additional active inequality would leave a nontrivial local segment, contradicting extremality.

An edge changes only one category. Its direction is either \(e_q\) or \(e_q-e_r\), up to scaling. A nonintegral point on that edge lies between two neighboring integral points. They differ by adding one small copy or exchanging two small types. Their values consequently differ by at most \(\varepsilon a\).

Choose the cheaper of these two integral points. Its cost is no greater than the fractional point’s cost, because the latter is their convex combination. Its value is at least the fractional point’s value minus \(\varepsilon a\). Adding \(h\) therefore produces a feasible bundle worth at least \((1-\varepsilon)a\). Record it.

Return a cheapest recorded candidate. If there is none, declare the original threshold unattainable.

To prove the cost guarantee, take a cheapest original bundle \(c\) worth at least \(a\).

Thus an original qualifying bundle always supplies a candidate of no greater cost. This also proves that a declaration of unattainability is sound.

There are \(O((m+1)^{10})\) enumerated vectors. Each LP has at most \(m\) variables and \(O(m+\ell)\) constraints, with binary-encoded capacities. The oracle therefore runs in \(O((m+1)^{10}\operatorname{poly}(m,\ell,\text{input bit length}))\) bit operations.

4. Turning the oracle into exact mass feasibility. For thresholds \(a=(a_t)\), define

\[ G_t(a_t)=\{b\in\mathcal B:v_t(b)\ge a_t\}. \]

We now prove a polynomial procedure that returns either:

These outcomes deliberately allow overlap: the procedure is not an exact threshold-decision algorithm.

Put \(d=\tau+m\), \(y=(\mu,\lambda)\), and associate the integer column

\[ A_{t,b}=(e_t,b)\in\mathbb Z_{\ge0}^{d} \]

with each type–bundle pair. Original threshold feasibility is precisely the existence of nonnegative coefficients satisfying \(\sum_{t,b}x_{t,b}A_{t,b}=y\), using only \(b\in G_t(a_t)\).

By Farkas’ lemma, infeasibility is equivalent to the existence of \(u=(r,p)\) satisfying

\[ r_t+p\cdot b\ge0\quad\text{for all original qualifying pairs},\qquad u\cdot y\le-1. \]

The normalization to \(-1\) follows by scaling any strictly separating vector.

We run an ellipsoid cutting procedure in this dual space. The following explicit bounds justify polynomial termination and extraction of a primal solution.

Let \(C=\max(1,k_1,\ldots,k_\ell)\), and let \(D\) clear the denominators of \(y\). Then every coordinate of every column and of \(y\) is at most \(C\), and \(Dy\) is integral. Set

\[ F=(2d)!(DC)^{2d},\qquad H=16(F+1). \]

For any finite set \(S\) of possible columns, if \(y\) is outside their generated cone, there is a normalized separating vector \(u_0\) with every coordinate of absolute value at most \(F\). Here is the bit-bound justification. Split each coordinate of \(u_0\) into two nonnegative variables. The resulting feasible LP has \(2d\) variables and integral coefficients bounded by \(DC\), after clearing the normalization inequality’s denominator. It has a vertex: minimizing the sum of its nonnegative variables yields a nonempty compact optimal face. At a vertex, choose \(2d\) independent active equations. Cramer’s rule, with right-hand sides bounded by \(DC\), bounds each coordinate by \((2d)!(DC)^{2d}\). The difference of two nonnegative coordinates has the same absolute bound.

Let \(f=(\mathbf1_\tau,0_m)\). Since \(f\cdot A_{t,b}=1\) and \(f\cdot y=1\), the vector \(\widehat u=4u_0+f\) satisfies

\[ \widehat u\cdot A\ge1\quad(A\in S),\qquad \widehat u\cdot y\le-3,\qquad |\widehat u_j|\le H/2. \]

Thus the system

\[ |u_j|\le H,\qquad u\cdot y\le-1,\qquad u\cdot A\ge0\quad(A\in S) \]

contains a Euclidean ball of radius \(\eta=1/(4dC)\). To check this, perturb \(\widehat u\) by a vector of Euclidean norm at most \(\eta\). Each column and \(y\) has norm at most \(\sqrt d\,C\), so every relevant dot product changes by at most \(1/4\). The box bounds also remain satisfied.

Start the ellipsoid with a ball of radius \(dH\), containing the box. At a query point \(u=(r,p)\):

The last declaration is sound. For every original qualifying bundle \(c\), the oracle’s cost guarantee gives

\[ r_t+p\cdot c\ge r_t+p\cdot b\ge0. \]

If that type’s original qualifying set is empty, the assertion is vacuous. Hence the query point is a genuine Farkas certificate for original infeasibility.

The standard rational ellipsoid cutting theorem reduces the enclosing volume below that of an \(\eta\)-ball after \(O(d^2\log(dH/\eta))\) central cuts. It uses polynomial-bit arithmetic here: the constraint coefficients, \(\log H\), and \(\log(1/\eta)\) all have polynomial encoding length.

If no infeasibility declaration occurs by then, let \(S\) be the recorded columns. Necessarily \(y\) belongs to their generated cone. Otherwise, the ball constructed above satisfies every recorded inequality and every box and normalization constraint. Every ellipsoid cut contains that ball, contradicting the final volume bound.

Solve the finite rational LP \(\sum_{A\in S}x_AA=y\), \(x_A\ge0\). Every recorded bundle satisfies its relaxed threshold, so this is the promised exact mass assignment. There are polynomially many recorded columns.

In particular, whenever the original threshold assignment exists, the procedure must return a relaxed assignment.

5. Polynomially computable lower estimates of the benchmarks. We compute numbers \(w_t\) satisfying

\[ \frac{81}{100}z_t^\infty\le w_t\le z_t^\infty. \]

If all values of type \(t\) are zero, set \(w_t=0\). Otherwise let \(u_t\) be its smallest strictly positive single-copy value, and put

\[ U_t=\sum_h k_h\max_{q\in\mathcal Q_h}v_{tq}. \]

Every feasible bundle has value at most \(U_t\). Also, if \(z_t^\infty>0\), then \(z_t^\infty\ge u_t\), because every positive bundle value is at least \(u_t\).

Apply the preceding feasibility procedure to the one-type society of mass one with valuation \(v_t\) and supplies \(\lambda\). Maintain lower endpoint \(l=0\) and upper endpoint \(h=U_t+u_t\). Query their midpoint repeatedly:

Stop when \(h-l\le u_t/10\), and set \(w_t=9l/10\).

The procedure’s outcomes need not be monotone. The argument uses only these two sound invariants:

At termination, \(l\ge z_t^\infty-u_t/10\). If the benchmark is positive, this gives

\[ w_t\ge\frac9{10}\left(z_t^\infty-\frac{u_t}{10}\right) \ge\frac{81}{100}z_t^\infty. \]

If the benchmark is zero, nonnegativity and \(w_t\le z_t^\infty\) give \(w_t=0\).

The number of queries is \(O(1+\log((U_t+u_t)/u_t))\), polynomial in the binary input length. All queried thresholds have polynomial encoding length.

6. Final assignment and complexity. Run the mass-feasibility procedure with thresholds \(a_t=w_t/2\).

Section 2 proves that an assignment exists giving every type at least \(z_t^\infty/2\). Since \(w_t\le z_t^\infty\), the original thresholds \(a_t\) are feasible. The procedure therefore returns an exact assignment, and every used bundle satisfies

\[ v_t(b)\ge\frac9{10}\frac{w_t}{2} \ge\frac{729}{2000}z_t^\infty \ge\frac13z_t^\infty. \]

Its defining linear system gives exactly \(\sum_bx_{t,b}=\mu_t\) and \(\sum_{t,b}b_qx_{t,b}=\lambda_q\). Thus every supply is allocated.

Choose a basic feasible solution of the final finite LP. It has at most \(d=\tau+m\) positive entries. Its matrix consists of integer columns bounded by \(C\), and its right-hand side is the original rational vector \(y\). Cramer’s rule gives polynomial encoding length for its nonzero masses; each bundle also has polynomial encoding length because \(b_q\le k_h\).

Combining the polynomial number of ellipsoid queries and benchmark queries with the bundle oracle’s enumeration bound yields

\[ (m+1)^{10}\operatorname{poly}\!\left(m,\tau,\ell,L,\sum_h\log(k_h+1)\right) \]

bit operations. This resolves both the existential and computational parts of the stated question.

⟨structured verdict parsed — rendered above⟩

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

The argument is sound in substance and resolves the binary-input polynomial-time question, subject to two minor clarifications of degenerate cases. I found no major mathematical gap or false central step. The claimed factor \(\frac{729}{2000}\), exact supply equalities, and sparse output bound survive the audit.

1. Finite theorem and its applicability

The external theorem is correctly identified. Hummel–Hetland’s Theorem 5 guarantees a constrained MMS approximation factor \(\frac{n}{2n-1}\). Its model uses nonnegative additive valuations, category cardinality limits, and allocations that partition all items into possibly empty bundles. Its feasibility condition is that each category contain at most \(nk_h\) items. Zero-total-value agents are covered by the paper’s stated reduction convention. [Theorem 5, preliminaries, and Note 6](https://link.springer.com/article/10.1007/s10458-026-09731-1)

For the constructed instance, \(n=N\), and category \(h\) contains
\[ N\sum_{q\in\mathcal Q_h}\lambda_q\le Nk_h \]
items. Thus the feasibility hypothesis is satisfied. Labeling copies causes no valuation mismatch: each copy retains its good type’s value. Categories with no items can be omitted.

The invocation of this theorem is verified, including its requirement to allocate every item.

2. Attainment and exact transfer

The polytope \(P\) is a product of category simplices with integral vertices. This remains true when a limit is zero: the corresponding simplex is a singleton. Hence the claimed equality \(P=\operatorname{conv}(\mathcal B)\) is correct, and the supply assumption establishes that \(\mathcal D(\lambda)\) is nonempty.

The attainment argument is valid. The bundle set is finite, and each distribution has nonempty support. Its minimum supported value belongs to a finite set, so the maximum over achievable minimum values is attained.

Restricting the distribution system to bundles meeting the attained threshold gives a nonempty rational polytope. A rational basic feasible solution therefore exists. Clearing the denominators of these distributions, the supplies, and the masses is legitimate for an existence proof; no polynomial bound on \(N\) is needed here.

Both directions of the finite correspondence check out:

Consequently, the finite constrained MMS equals \(z_t^\infty\), rather than merely bounding it in one direction. Aggregating the finite allocation and dividing agent counts by \(N\) preserves type masses and all supply equalities.

Minor issue: The phrase “the empty assignment solves the problem” is ambiguous and literally false if it means returning no nonzero assignment entries. For example, with one supported type of mass one and zero supplies, an empty list violates the type-mass equality.

Minimum clarification: Specify that the zero-item branch assigns each type’s mass to the empty bundle, rather than returning an empty mass assignment.

3. Bundle oracle

The zero-threshold optimization is correct, including negative prices and zero capacities. Separability across categories justifies filling a category with a cheapest negative-price type and otherwise leaving it unused.

For positive thresholds, the strict definition of a large type is used correctly: ten large copies have value strictly greater than \(a\). The enumeration covers every vector of at most ten large copies.

The geometric rounding argument is valid:

This proves the stated relaxed value bound without a cost increase, for prices of either sign.

Minor issue: The procedural description explicitly gives a rounding rule only for a nonintegral vertex. An optimal vertex can already be integral, in which case the referenced “two integral points” need not be specified.

Minimum clarification: State what the oracle records when its optimal vertex is already integral.

The cost guarantee against an original qualifying bundle is otherwise fully established. The two cases—at least ten large copies, or fewer than ten—exhaust all possibilities. Each supplies an enumerated candidate costing no more than the original optimum. Therefore declaring unattainability when no candidate exists is sound.

The enumeration and LP size bounds are polynomial in the binary encoding, with no iteration through a capacity’s numerical magnitude.

4. Farkas formulation and separator bounds

The column formulation correctly encodes both type masses and exact supplies. There are finitely many possible columns, so Farkas’ lemma applies to their generated cone. A strict separator can be scaled to satisfy the displayed normalization.

The coordinate bounds are correct: bundle coordinates and supply coordinates are at most \(C\), while masses are at most one. Clearing the right-hand-side denominator gives integral coefficients bounded by \(DC\).

The split-variable separator LP has a vertex. The argument using minimization of the sum of nonnegative variables produces a nonempty compact optimal face. Selecting independent active equations and applying Cramer’s rule gives the stated bound \(F\). Taking the difference of two coordinates in \([0,F]\) preserves the absolute bound \(F\).

The vector \(f\) has the asserted dot products because every column contains exactly one type indicator and the masses sum to one. Consequently, the margins for \(\widehat u\) are correct.

The ball-radius calculation is also correct. A perturbation of norm at most \(\eta\) changes each relevant dot product by at most
\[ \sqrt d\,C\eta=\frac{1}{4\sqrt d}\le\frac14. \]
The box margins are ample. No constant or range error occurs here.

5. Ellipsoid procedure and primal extraction

Both infeasibility declarations are sound.

An unattainable original threshold for a supported type precludes an assignment because its mass is strictly positive.

When no returned bundle violates its inequality, the oracle’s cost guarantee establishes every original qualifying inequality. Together with the normalization constraint, this gives a genuine Farkas certificate. This reasoning does not require an exact threshold-decision oracle.

The recorded cuts can involve relaxed bundles. That does not invalidate the extraction argument: the contradiction is formulated for the cone generated by those recorded columns themselves.

If \(y\) were outside that cone, the separator bound would give an \(\eta\)-ball satisfying all recorded constraints, the box, and the normalization. Every central cut retains that ball, contradicting the terminal volume bound. Thus the finite primal LP is feasible.

The stated rational ellipsoid complexity applies here: dimension, initial radius, retained-ball radius, and cut-coefficient encoding lengths have polynomial bounds. Query prices can consequently have polynomial encoding length, as required by the bundle oracle.

All recorded columns satisfy their relaxed thresholds. Solving their finite rational LP therefore yields an exact feasible assignment with the claimed relaxed value guarantees.

6. Benchmark estimates

The upper bundle-value bound \(U_t\) is correct. The positive-benchmark lower bound \(z_t^\infty\ge u_t\) follows from nonnegative additivity and integral copy counts. It remains valid when the smallest positive single-copy value belongs to a type that cannot occur in a feasible bundle.

The bisection does not rely on monotone oracle outcomes. Its stated invariants suffice:

At termination, \(h>z_t^\infty\) and \(h-l\le u_t/10\) imply the claimed lower bound on \(l\). For a positive benchmark, the calculation establishing \(w_t\ge\frac{81}{100}z_t^\infty\) is correct. For a zero benchmark, the certified upper bound and nonnegativity force \(w_t=0\).

The cases of all-zero valuations and zero usable capacity are covered. The query count and midpoint encoding lengths are polynomial in the binary input length.

7. Final factor, sparsity, and complexity

The existence result makes the original thresholds \(w_t/2\) feasible, so the final procedure must return an assignment.

The factor calculation is correct:
\[ \frac9{10}\cdot\frac12\cdot\frac{81}{100} =\frac{729}{2000} >\frac13. \]

The finite LP imposes the original mass and supply equalities exactly. A basic feasible solution has at most \(\tau+m\) positive entries, including when the equality matrix has smaller rank. Integer column bounds and the rational right-hand side give polynomial encoding lengths for the returned masses. Bundle coordinates also have polynomial encoding length.

Combining polynomially many oracle calls with the enumeration bound yields the claimed binary-polynomial running time. The potentially enormous finite population is used only for existence and is never expanded by the algorithm.

The two identified issues require routine clarification; neither requires new mathematics or changes the computational conclusion.

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