← back to the atlas

Fair Division with Binary Valuations: One Rule to Rule Them All (d4-conf-wine-2020-0003)

Answer: —

The anchor (named result in the paper)

Corollary 1 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateUnder binary additive valuations, the fractional maximum Nash welfare rule is ex ante envy-free, ex ante Pareto optimal, ex ante group strategyproof, ex post envy-free up to one good, and polynomial-time computable.

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

The continuous mirror question, as graded

Given a finite good set \(G\), an explicit type set \(T\subseteq 2^G\), rational masses \(\mu_t\) with \(\sum_t\mu_t=1\), and rational per-capita supplies \(\rho_g\) satisfying \(0\le\rho_g\le\sum_{t:g\in t}\mu_t\), compute in time \(\operatorname{poly}(m,\tau,L)\) a mass assignment \(\lambda_{t,B}\ge0\) for \(B\subseteq t\), satisfying \(\sum_{B\subseteq t}\lambda_{t,B}=\mu_t\) and \(\sum_{t,B:g\in B}\lambda_{t,B}=\rho_g\), together with a polynomial-size distribution \(\mathcal D\) over integral-bundle mass assignments implementing these marginals, such that \(u_t=\mu_t^{-1}\sum_{B\subseteq t}|B|\lambda_{t,B}\) maximizes \(\sum_{t:\mu_t>0}\mu_t\log u_t\), the aggregate rule is ex ante EF, ex ante PO, and ex ante GSP, and every supported integral assignment is ex post EF1.

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

Let \(G\) be a finite good set and \(T\subseteq 2^G\) an explicit set of binary-valuation types; type \(t\) values \(B\subseteq G\) by \(v_t(B)=|t\cap B|\). Type \(t\) has rational mass \(\mu_t\), with \(\sum_t\mu_t=1\), and good \(g\) has rational per-capita supply \(\rho_g\leq\sum_{t:g\in t}\mu_t\).

A type-mass allocation is \(\lambda_{t,B}\geq0\) for \(B\subseteq t\), with \(\sum_{B\subseteq t}\lambda_{t,B}=\mu_t\) and \(\sum_{t,B:g\in B}\lambda_{t,B}=\rho_g\). Its per-capita utility is \(u_t=\mu_t^{-1}\sum_{B\subseteq t}|B|\lambda_{t,B}\) for \(\mu_t>0\). An integral-bundle mass assignment gives every population member an entire bundle \(B\subseteq t\); a distribution implements \(\lambda\) when its expected type-bundle masses are \(\lambda\).

Target. Is there a polynomial-time algorithm, in \(m=|G|\), \(\tau=|T|\), and input bit-length \(L\), that returns such a \(\lambda\) maximizing \(\sum_{t:\mu_t>0}\mu_t\log u_t\), together with a polynomial-size implementing distribution that is ex ante EF, ex ante PO, ex ante GSP, and ex post EF1; or is this problem NP-hard?

Nearest known results. For finitely many individual agents with binary additive valuations, the fractional maximum-Nash-welfare rule is polynomial-time computable and is ex ante EF, ex ante PO, ex ante GSP, and ex post EF1.

Prover output (gpt-6-astra / medium, Bolzano prover prompt)

Under the standard interpretation—each realized assignment respects supply, ex ante EF compares individual population members, and a polynomial-size distribution explicitly lists its deterministic outcomes—the requested polynomial-size distribution need not exist. This is an output-size obstruction, not an NP-hardness proof. A succinct randomized implementation is a different output requirement.

Here is a precise obstruction, followed by a compact formulation of the allocation problem.

Proved obstruction. For any positive integer \(k\), take
\(G=\{g\}\), \(T=\{t\}\), \(t=\{g\}\), \(\mu_t=1\), and \(\rho_g=2^{-k}\).
These data satisfy the supply hypothesis, and their binary encoding has length \(O(k)\).

There are only two permissible bundles. Consequently, feasibility uniquely determines
\(\lambda_{t,\{g\}}=2^{-k}\) and
\(\lambda_{t,\varnothing}=1-2^{-k}\).
The unique feasible utility is \(u_t=2^{-k}>0\). Thus this allocation maximizes the stated logarithmic objective; there is no optimization difficulty in this example.

Model the population by a probability space \((X,\nu)\). A deterministic feasible assignment gives \(g\) to a measurable recipient set of mass at most \(2^{-k}\).

Suppose an implementing lottery has deterministic outcomes indexed by \(j\in\{1,\ldots,K\}\), with positive probabilities \(p_j\). Let \(A_j\subseteq X\) be the recipient set in outcome \(j\). A member \(a\in X\) receives expected utility
\(q(a)=\sum_{j=1}^{K}p_j\mathbf{1}_{A_j}(a)\).

All members have identical valuations. Individual ex ante EF therefore requires \(q(a)\geq q(b)\) for every ordered pair of members \(a,b\), so their expected utilities are equal. The same conclusion holds almost everywhere if fairness is imposed almost everywhere.

Implementation gives
\(\int_X q(a)\,d\nu(a)=2^{-k}\).
Hence \(q(a)=2^{-k}>0\) almost everywhere. Every such member belongs to at least one recipient set, and therefore
\(1=\nu(\bigcup_{j=1}^{K}A_j)\leq\sum_{j=1}^{K}\nu(A_j)\leq K2^{-k}\).
It follows that \(K\geq 2^k\).

Thus the number of explicitly listed deterministic outcomes must be exponential in the input length. This lower bound already follows from feasibility and ex ante EF, independently of the other requested properties.

The obstruction is tight in this example. Partition the population into \(2^k\) equal-mass sets and choose one uniformly to receive \(g\). Every member receives it with probability \(2^{-k}\). Every outcome is EF1: removing the sole good from any envied bundle leaves an empty bundle.

Equivalently, realize the instance using \(N=2^k\) equally weighted individuals and one physical good. Ex ante EF requires each individual to win with probability \(1/N\), while each deterministic allocation has one winner. At least \(N\) outcomes are necessary.

Why this does not contradict the finite-agent result. The finite-agent theorem uses an explicit individual-agent input and establishes polynomial-time implementation in that setting. Here the population can be exponentially larger than its type-mass encoding. The same support bound is linear in the explicit population size but exponential in the compressed input length. The cited paper also defines ex ante EF through comparisons of individual agents’ expected valuations. [Halpern, Procaccia, Psomas, and Shah, *Fair Division with Binary Valuations: One Rule to Rule Them All*](https://www.cs.toronto.edu/~nisarg/papers/binaryMNW.pdf).

A separate proved simplification. The exponentially indexed bundle variables are not themselves necessary for describing feasible marginals.

For each \(t\in T\) and \(g\in t\), define
\(x_{t,g}=\sum_{B\subseteq t:\,g\in B}\lambda_{t,B}\).
Every feasible allocation satisfies
\(0\leq x_{t,g}\leq\mu_t\) and
\(\sum_{t:\,g\in t}x_{t,g}=\rho_g\).
Moreover, \(u_t=\mu_t^{-1}\sum_{g\in t}x_{t,g}\) whenever \(\mu_t>0\).

Conversely, every vector satisfying these marginal constraints comes from a feasible bundle-mass allocation. To prove this, fix a positive-mass type and set \(z_g=x_{t,g}/\mu_t\). For a uniform parameter \(r\in[0,1]\), define
\(B_t(r)=\{g\in t:r<z_g\}\).
Then \(\Pr(g\in B_t(r))=z_g\). Assign mass
\(\lambda_{t,B}=\mu_t\Pr(B_t(r)=B)\).
These masses sum to \(\mu_t\), have the prescribed marginals, and therefore satisfy every supply equality.

The bundle changes only at the distinct thresholds \(z_g\), so this construction uses at most \(|t|+1\) positive bundle masses for type \(t\). Zero-mass types receive zero bundle masses. For rational marginals, sorting the thresholds and taking consecutive differences constructs this sparse representation in polynomial time in their encoding length.

Consequently, the welfare objective can be written using at most \(m\tau\) marginal variables. This observation does not by itself prove exact polynomial-time welfare optimization or provide a fair individual-level implementation. In particular, sparse bundle masses do not bound the support needed to randomize fairly over named population members.

Remaining interpretation issue. The question defines implementation through expected type-bundle masses, but those expectations alone do not determine individual ex ante EF. In the one-type example, always serving the same population subset implements the required masses but violates individual ex ante EF.

The exponential bound applies to an explicit lottery over feasible deterministic assignments. It does not exclude a short sampling description: “choose one of the \(2^k\) equal blocks uniformly” has a compact description despite its exponential support. Likewise, allowing supply to be respected only in expectation changes the problem.

Thus an explicit polynomial-support interpretation has a rigorous negative answer. The complexity of the variant permitting succinct randomized implementations, including its strategyproof mechanism requirement, remains unsettled here.

⟨structured verdict parsed — rendered above⟩

Adversarial review (gpt-6-astra / low, Bolzano verifier prompt)

Assessment: partial, with a correct conditional obstruction. The support lower bound and the sparse marginal representation are sound. The output does not classify the original continuous problem as polynomial-time solvable or NP-hard. It explicitly acknowledges this limitation. No central mathematical step is refuted.

For every positive integer \(k\), the proposed instance satisfies the supply inequality. Under ordinary binary rational encoding, its length is \(\Theta(k)\): the denominator \(2^k\) requires \(k+1\) binary digits, and the remaining data have constant size.

The two feasibility equalities force \(\lambda_{t,\{g\}}=2^{-k}\) and \(\lambda_{t,\varnothing}=1-2^{-k}\). Thus \(u_t=2^{-k}>0\), and the logarithmic objective is well-defined and constant over the singleton feasible set. The maximization claim is correct.

If each realized assignment must respect supply, its recipient set satisfies \(\nu(A_j)\leq 2^{-k}\). Exact realized supply equality would also imply this inequality, so using an upper bound does not weaken the obstruction improperly.

However, the target explicitly specifies supply equalities for expected type-bundle masses; it does not separately formalize realized feasibility. The prover announces this additional interpretation rather than deriving it.

Major scope issue: the resulting theorem is conditional on realized supply feasibility, individual-level fairness, and explicit enumeration of outcomes. These conditions must be fixed before this becomes an unconditional answer to the target. This is an acknowledged limitation, not a false step in the conditional proof.

In this instance, every member values another member’s random bundle by that member’s probability of receiving the sole good. Consequently, individual ex ante EF gives \(q(a)\geq q(b)\) for every ordered pair, and reversing the pair gives equality.

The almost-everywhere version is also sound under the usual interpretation that the comparison holds for almost every ordered pair with respect to product measure. The intended convention could be stated explicitly, but it does not create a substantive gap.

Implementation implies \(\int_X q\,d\nu=2^{-k}\). Since the population has total mass one and \(q\) is constant almost everywhere, its almost-everywhere value is \(2^{-k}\).

Every member with positive \(q\) lies in the union of the recipient sets. Finite subadditivity and realized feasibility therefore give
\(1=\nu(\bigcup_{j=1}^K A_j)\leq\sum_{j=1}^K\nu(A_j)\leq K2^{-k}\).
Hence \(K\geq 2^k\).

All constants and quantifiers are correct. Since the instance length is \(\Theta(k)\), this excludes polynomial support, and therefore polynomial-length explicit enumeration, on this family. The argument needs none of the PO, GSP, or EF1 requirements.

This establishes an output-size obstruction. It does not establish NP-hardness, and the prover correctly avoids that inference.

If the population admits the stated equal-mass partition, uniformly selecting one block gives the required individual winning probabilities and realizes the prescribed masses. Every resulting assignment is EF1: the only possible envied nonempty bundle contains the sole good.

Minor issue: an arbitrary probability space need not admit a partition into \(2^k\) equal-mass measurable sets. For example, a one-point probability space has no measurable set of mass \(2^{-k}\) when \(k\geq1\). Thus the tightness statement requires a population admitting that partition.

Minimum clarification: qualify tightness by the equal-partition assumption, or explicitly restrict this paragraph to the equally weighted finite population already described in the output.

The finite realization with \(N=2^k\) individuals and one physical good is correct. Its per-capita supply is \(1/N\), and individual EF requires every person to win with probability \(1/N\). This realization supports the tightness claim without asserting equivalence for every probability space.

The cited paper’s Theorem 3 establishes ex ante EF and PO for fractional MNW allocations, and ex ante GSP for its minimally complete fractional MNW rule. Theorem 4 provides polynomial-time implementation supported on deterministic MNW allocations; Corollary 1 states the combined guarantees. These results concern explicitly represented finite agents with binary additive valuations. [Halpern, Procaccia, Psomas, and Shah](https://www.cs.toronto.edu/~nisarg/papers/binaryMNW.pdf).

The finite instance in the output satisfies those hypotheses. A support requirement linear in the explicit number of individuals is compatible with exponential support relative to the compressed type-mass encoding.

Minor exposition issue: the output should identify the precise theorem statements and the minimally complete rule qualification when summarizing GSP. This citation is contextual; the support obstruction does not depend on it.

Each \(x_{t,g}\) is a sum of nonnegative bundle masses bounded by the total type mass, so \(0\leq x_{t,g}\leq\mu_t\). Summing over types gives the prescribed supply equality.

The utility identity follows by interchanging finite sums: each bundle contributes once for every good it contains. No assumption about correlations between goods is needed.

For a positive-mass type, the marginal bounds ensure \(z_g\in[0,1]\). The threshold construction gives \(\Pr(r<z_g)=z_g\), including the endpoints zero and one. Consequently, the constructed bundle masses sum to \(\mu_t\) and reproduce every marginal.

At most \(|t|+1\) bundles have positive probability. Repeated thresholds and endpoint thresholds can only reduce this number. An empty positive-mass type receives the empty bundle. For a zero-mass type, the marginal bounds already force all its marginals to zero, consistent with assigning zero bundle masses.

Sorting rational thresholds and taking differences is polynomial-time in their supplied encoding length. The output correctly does not infer that optimal marginals have already been computed, that their encoding length has been bounded, or that this construction supplies a fair lottery over individuals.

The established content is a conditional impossibility of polynomial explicit support and a polynomial-size description of feasible bundle masses from given marginals.

No exact welfare-optimization algorithm, hardness reduction, or mechanism for the succinct-implementation variant is supplied. The latter would also require a reporting and coalition model for GSP. These omissions are explicitly acknowledged, so the appropriate verdict is partial rather than refuted.

The minimum next clarification is to fix the population model, realized supply requirement, fairness comparison, and output representation. Under the explicit-outcome interpretation used in the proof, the conditional negative answer already stands; under other interpretations, further substantive work 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.