← back to the atlas

Weighted Envy-Freeness for Submodular Valuations (aaai24-28847)

Answer: Polynomial-time solvable in \(m,\tau,R,L\); the decision problem belongs to \(\mathrm P\).

The anchor (named result in the paper)

Theorem 11 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateSuppose that all agents have matroid-rank valuations, and let x ∈[0, 1]. Algorithm 1 with param- eter x returns a clean TWEF(x, 1 −x) (and therefore WMEF(x, 1 −x)) allocation that maximizes the unweighted utilitarian welfare among all allocations in polynomial time. Since any allocation maximizing the unweighted utilitar- ian welfare is PO, the allocation output by Algorithm 1 is also PO. In the unweighted setting, Benabbou et al. (2021) exhibited polynomial-time termination of their algorithm using the potential function Φ(A) := P i∈N vi(Ai)2.

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

The continuous mirror question, as graded

Given rational masses over finitely many complete entitlement-and-valuation types, clone-symmetric matroid-rank valuations over finitely many good classes, and rational per-capita supplies, choose fractions \(q_{t,B}\) of each type receiving whole bundles, respecting supplies and clean support, to maximize mass-weighted utilitarian welfare subject to the paper's \(\mathrm{TWEF}(x,1-x)\) inequality for every pair of positive-support bundle states.

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

A society is given by its support: the list of the \(\tau\) types with positive mass \(\mu_t\), each a binary rational, with \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types. Each type includes a positive binary-rational entitlement \(w_t\) and its valuation.
There are \(m\) good classes with nonnegative binary-rational per-capita supplies \(s_c\). A unary integer \(R\ge1\) bounds valuation ranks. Each valuation \(v_t\) is specified by an evaluation circuit on class-count vectors, promised to represent a matroid-rank valuation of rank at most \(R\) on \(2R\) distinct clones per class, invariant under permutations within each class. Let \(L\) be the total input bit length, including these circuits.
Whole bundles are vectors \(b\in\mathbb Z_{\ge0}^m\) with \(\sum_c b_c\le R\). A bundle is clean for type \(t\) when \(v_t(b)=\sum_c b_c\). Adding bundles means taking distinct clones, so their union is represented by \(b+d\), even when their class counts coincide.
Choose nonnegative rational fractions \(q_{t,b}\), with \(\sum_bq_{t,b}=1\), supported only on clean bundles, and satisfying \(\sum_{t,b}\mu_tq_{t,b}b_c\le s_c\) for every class \(c\); unused supply is allowed. Welfare is \(\sum_{t,b}\mu_tq_{t,b}v_t(b)\), without entitlement factors.
Given a binary-rational \(x\in[0,1]\), require for every ordered pair of states \((t,b),(u,d)\) with \(q_{t,b}q_{u,d}>0\), including states of the same type, either \(v_t(b)=v_t(b+d)\), or some class \(c\) with \(d_c>0\) satisfies \(\frac{v_t(b)+(1-x)(v_t(b+e_c)-v_t(b))}{w_t}\ge\frac{v_t(d)-x(v_t(d)-v_t(d-e_c))}{w_u}\), where \(e_c\) is the class unit vector.

Given a nonnegative binary-rational threshold \(H\), is deciding whether such fractions achieve welfare at least \(H\) solvable in polynomial time in \(m,\tau,R,L\), or is it NP-hard?

For finite agents and indivisible goods with matroid-rank valuations, a clean \(\mathrm{TWEF}(x,1-x)\) allocation maximizing unweighted utilitarian welfare can be computed in polynomial time with valuation-oracle access ([Montanari et al.](https://link.springer.com/article/10.1007/s00355-025-01599-6)). No result settling the exact mass-allocation problem above was located in the literature search.

Modeling choices made when packaging the task

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

Result. The decision problem is polynomial-time solvable in \(m,\tau,R,L\). In fact, the maximum welfare attainable under the stated fairness condition equals the maximum welfare attainable using only cleanness and supply constraints.

The proof has two parts: a potential argument establishes this equality, and matroid greedy optimization provides a polynomial-time separation oracle for the welfare LP.

1. The welfare LP without fairness.

Write \(|b|=\sum_c b_c\), and let
\[ \mathcal B_t=\{b\in\mathbb Z_{\ge0}^m: |b|\le R,\ v_t(b)=|b|\}. \]

Replace conditional fractions by population masses:
\[ y_{t,b}=\mu_tq_{t,b}. \]
Because every \(\mu_t>0\), this change of variables preserves which states have positive mass.

Without fairness, welfare maximization is the finite LP
\[ \begin{aligned} W^*=\max\quad &\sum_t\sum_{b\in\mathcal B_t}|b|y_{t,b}\\ \text{subject to}\quad &\sum_{b\in\mathcal B_t}y_{t,b}=\mu_t &&\text{for every }t,\\ &\sum_t\sum_{b\in\mathcal B_t}b_cy_{t,b}\le s_c &&\text{for every }c,\\ &y_{t,b}\ge0. \end{aligned} \tag{P} \]

This LP is feasible: give everyone the empty bundle. Its feasible region is compact, since \(0\le y_{t,b}\le\mu_t\). Moreover, \(0\le W^*\le R\). All coefficients are rational, so an optimal rational solution exists.

The number of bundles may be exponential. We will handle that in Section 3.

2. A welfare optimum satisfying every pairwise fairness condition.

For each type define
\[ F_t(k)=\frac{k^2+(1-2x)k}{w_t}, \qquad 0\le k\le R, \]
and define the linear potential
\[ \Phi(y)=\sum_t\sum_{b\in\mathcal B_t}y_{t,b}F_t(|b|). \]

This uses the quadratic transfer potential appearing in [Montanari et al., Section 5](https://link.springer.com/article/10.1007/s00355-025-01599-6). The following argument establishes its consequence directly for population masses.

Among all solutions of (P) attaining \(W^*\), choose \(y^*\) minimizing \(\Phi\). Such a minimizer exists by compactness and can be chosen rational, because this secondary optimization is a rational LP.

We prove that \(y^*\) satisfies the requested fairness condition.

Suppose, to the contrary, that supported states \((t,b)\) and \((u,d)\) violate the condition. Put \(k=|b|\) and \(\ell=|d|\). Cleanness gives
\[ v_t(b)=k,\qquad v_u(d)=\ell. \]
Violation means that
\[ v_t(b+d)>v_t(b) \tag{1} \]
and, for every class \(c\) with \(d_c>0\),
\[ \frac{k+(1-x)(v_t(b+e_c)-v_t(b))}{w_t} < \frac{v_t(d)-x(v_t(d)-v_t(d-e_c))}{w_u}. \tag{2} \]

An augmenting class exists. Represent \(b\) and \(d\) by disjoint clone sets \(B,D\). This is possible because \(b_c+d_c\le2R\) for every class.

If every clone in \(D\) had zero marginal rank at \(B\), diminishing returns would imply that all successive additions from \(D\) also had zero marginal rank. This would contradict (1). Consequently, some class \(c\) with \(d_c>0\) satisfies
\[ v_t(b+e_c)-v_t(b)=1. \tag{3} \]
Here we used that matroid-rank marginals belong to \(\{0,1\}\).

For this class, let
\[ \delta=v_t(d)-v_t(d-e_c)\in\{0,1\}. \]
Since rank never exceeds cardinality and \(1-x\ge0\),
\[ \begin{aligned} v_t(d)-x\delta &=v_t(d-e_c)+(1-x)\delta\\ &\le(\ell-1)+(1-x)\\ &=\ell-x. \end{aligned} \tag{4} \]
Combining (2), (3), and (4) yields
\[ \frac{k+1-x}{w_t}<\frac{\ell-x}{w_u}. \tag{5} \]

Transfer a positive population mass. The bundle \(b+e_c\) is clean for type \(t\), by (3). Its size is at most \(R\), because its rank is \(k+1\) and the valuation has rank at most \(R\). The bundle \(d-e_c\) is clean for type \(u\), because a subset of a matroid-independent set is independent.

Choose a positive rational
\[ \varepsilon<\tfrac12\min\{y^*_{t,b},y^*_{u,d}\}. \]
Remove mass \(\varepsilon\) from each of \((t,b),(u,d)\), and add mass \(\varepsilon\) to each of
\[ (t,b+e_c),\qquad (u,d-e_c). \]
Additions and removals are aggregated if configuration coordinates coincide. The choice of \(\varepsilon\) guarantees nonnegativity even when a source coordinate occurs twice.

This operation preserves every type’s total mass. It also preserves every class’s consumption, since
\[ (b+e_c)+(d-e_c)=b+d. \]
It preserves welfare, since
\[ (k+1)+(\ell-1)=k+\ell. \]
Thus the modified allocation is another feasible solution attaining \(W^*\).

Its potential change is
\[ \begin{aligned} \Delta\Phi &=\varepsilon\bigl(F_t(k+1)-F_t(k) +F_u(\ell-1)-F_u(\ell)\bigr)\\ &=2\varepsilon \left(\frac{k+1-x}{w_t}-\frac{\ell-x}{w_u}\right)\\ &<0, \end{aligned} \]
where the last inequality is (5). This contradicts the choice of \(y^*\).

The argument applies when \(t=u\) as well: both removals and both additions then occur within the same type. An identical state paired with itself cannot violate fairness, because (5) would become
\[ \frac{k+1-x}{w_t}<\frac{k-x}{w_t}, \]
which is impossible. No division by \(x\) or \(1-x\) occurred, so both endpoints \(x=0,1\) are covered.

Therefore \(y^*\) satisfies every required ordered-pair condition. Setting
\[ q_{t,b}=y^*_{t,b}/\mu_t \]
gives rational fractions satisfying the original requirements and attaining \(W^*\).

We have proved
\[ \boxed{\text{Maximum fair welfare}=W^*.} \tag{6} \]

3. Computing \(W^*\) exactly in polynomial time.

The dual of (P) is
\[ \begin{aligned} \min\quad &\sum_c s_c\alpha_c+\sum_t\mu_t\beta_t\\ \text{subject to}\quad &\beta_t+\sum_c\alpha_cb_c\ge |b| &&\text{for every }t,\ b\in\mathcal B_t,\\ &\alpha_c\ge0, \end{aligned} \tag{D} \]
where the \(\beta_t\) are initially unrestricted. The empty-bundle constraints imply \(\beta_t\ge0\). Strong LP duality applies because (P) is feasible and bounded.

For fixed nonnegative \(\alpha\), define
\[ f_t(\alpha)=\max_{b\in\mathcal B_t}\sum_c(1-\alpha_c)b_c. \]
The bundle constraints for type \(t\) are precisely \(\beta_t\ge f_t(\alpha)\).

A bounded dual suffices. We may restrict (D) to
\[ 0\le\alpha_c\le1,\qquad 0\le\beta_t\le R. \tag{7} \]

To verify this, replace any \(\alpha_c>1\) by \(1\). Before replacement, every unit of that class has negative coefficient in the maximization defining \(f_t\); afterward it has coefficient zero. Removing all units of that class preserves cleanness. Hence the maximum \(f_t\) is unchanged by the replacement. Because \(s_c\ge0\), the dual objective cannot increase.

After all such replacements, set \(\beta_t=f_t(\alpha)\). This maintains feasibility and cannot increase the objective, because \(\mu_t>0\). Finally,
\[ 0\le f_t(\alpha)\le R \]
when \(\alpha\in[0,1]^m\). This proves (7).

We therefore optimize over a nonempty bounded rational polytope in dimension \(m+\tau\). Its defining inequalities have integer coefficients of absolute value at most \(R\), apart from the rational objective coefficients.

Separation is matroid greedy optimization. First check the bounds (7). For a point satisfying those bounds, assign every clone of class \(c\) weight \(1-\alpha_c\).

For each type \(t\), the promised matroid has \(2Rm\) clones. A clone subset \(I\) is independent exactly when
\[ v_t(b(I))=|I|, \]
where \(b(I)\) is its class-count vector. Thus the evaluation circuit supplies a polynomial-time independence oracle.

Run the matroid greedy algorithm: process clones in nonincreasing weight order and add a clone whenever independence is preserved. Its resulting independent set has maximum total weight. For completeness, after every prefix of this order, the accepted set is a maximal independent subset of that prefix, hence has its rank. Every other independent set has no larger prefix cardinality. Expressing total weight as a nonnegative linear combination of prefix cardinalities proves greedy optimality.

Every independent clone set has size at most \(R\), and its count vector belongs to \(\mathcal B_t\). Conversely, every bundle in \(\mathcal B_t\) is represented by an independent clone set. Within-class invariance makes its value independent of the particular clone representatives. Consequently, greedy computes exactly \(f_t(\alpha)\).

If the maximizing bundle \(b\) satisfies
\[ f_t(\alpha)>\beta_t, \]
return the violated inequality
\[ \beta_t+\sum_c\alpha_cb_c\ge |b|. \]
If no type has such a violation, the candidate is feasible.

This is an exact separation oracle using at most \(2Rm\) independence tests per type, together with polynomial-time sorting and rational arithmetic. Circuit evaluation takes polynomial time in \(L\) and the count-vector encoding length.

We now apply the standard rational-polytope separation-to-optimization theorem: a bounded rational polytope with a known polynomial bound on inequality encoding lengths can be optimized exactly in polynomial time using a polynomial-time strong separation oracle. This is the exact rational version of the ellipsoid framework of [Grötschel, Lovász, and Schrijver](https://www.zib.de/userpage/groetschel/pubnew/paper/groetschellovaszschrijver1981a.pdf).

Its hypotheses hold here:

Thus the optimum of (D), and therefore \(W^*\), is computable exactly in polynomial time in \(m,\tau,R,L\). Unary encoding of \(R\) ensures that the \(2Rm\)-clone representation has polynomial size.

4. Decision procedure and conclusion.

Compute \(W^*\) using the bounded dual and its separation oracle, and accept exactly when
\[ W^*\ge H. \]

If the algorithm accepts, Section 2 supplies rational fair fractions attaining \(W^*\). If it rejects, even an allocation without fairness constraints cannot attain \(H\).

Therefore the target decision problem belongs to \(\mathrm P\). In particular, its optimal welfare is independent of the positive entitlements and of the choice of \(x\in[0,1]\), although the fair allocation attaining it can depend on both.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Verdict: proved. The output resolves the stated decision problem. The potential argument establishes that fairness does not reduce maximum attainable welfare, and the bounded-dual separation oracle establishes polynomial-time computation of that welfare. I found no major or minor issues requiring repair.

1. Formulation of the welfare LP

The configuration sets \(\mathcal B_t\) are finite and exactly describe the permitted clean bundles. On these bundles, valuation equals cardinality, so the objective of \((P)\) is the required unweighted welfare.

The substitution \(y_{t,b}=\mu_tq_{t,b}\) is valid because every listed type has strictly positive mass. It preserves support and converts normalization and supply constraints exactly as stated.

Feasibility, compactness, and rational attainment are correctly justified:

The possibly exponential number of configurations does not invalidate these existence arguments.

2. Selection of a potential-minimizing welfare optimum

The potential coefficients are rational because \(x\) and the positive entitlements \(w_t\) are rational.

The welfare-optimal face is nonempty and compact. Minimizing the linear potential over that face therefore attains a minimum. Because \(W^*\) and all coefficients are rational, a rational minimizer exists.

This step asserts existence, not efficient computation of the secondary minimizer. Existence is sufficient for the subsequent decision procedure.

3. Negation of fairness and the augmenting class

The output correctly negates the required condition: a violating supported pair must have strictly increasing union value, and every eligible class must fail the fairness inequality strictly. Monotonicity justifies replacing failure of union-value equality by strict inequality.

The disjoint-clone representation is valid. For each class, the combined count is at most \(2R\), exactly within the promised clone domain. Within-class invariance makes these representatives consistent with the circuit evaluations.

The augmenting-class argument is correct. If every clone of the donor bundle had zero marginal at the recipient bundle, diminishing returns would force zero marginal throughout their successive addition. This contradicts the strictly increasing union value.

Consequently, an eligible class has marginal rank one. The argument correctly uses the matroid-rank restriction that single-element marginals belong to \(\{0,1\}\).

4. The critical inequality

For the selected class, the donor bundle is nonempty and its removal marginal \(\delta\) belongs to \(\{0,1\}\). The calculation

\(v_t(d)-x\delta=v_t(d-e_c)+(1-x)\delta\le(\ell-1)+(1-x)=\ell-x\)

is valid:

Combining this upper bound with the strictly violated fairness inequality correctly gives

\(\dfrac{k+1-x}{w_t}<\dfrac{\ell-x}{w_u}\).

Both denominators are strictly positive by the task’s assumptions.

5. Validity of the population-mass transfer

Both destination bundles are allowed:

A positive rational \(\varepsilon\) satisfying the stated bound exists because both source masses are positive rational numbers.

The transfer preserves type masses, class consumption, and welfare exactly. These checks correctly concern population masses \(y\); entitlement factors do not enter either consumption or welfare.

The treatment of coinciding coordinates is sound. Aggregating the signed updates preserves the calculations, while the bound on \(\varepsilon\) guarantees nonnegativity even if a coordinate receives two removals.

6. Potential decrease and pairwise coverage

The potential differences are correctly computed:

\(F_t(k+1)-F_t(k)=\dfrac{2(k+1-x)}{w_t}\),

\(F_u(\ell-1)-F_u(\ell)=-\dfrac{2(\ell-x)}{w_u}\).

Thus the transfer strictly decreases potential while retaining optimal welfare, contradicting the selected minimizer.

The argument covers all required ordered pairs, including pairs of the same type. For an identical state paired with itself, the derived strict inequality would require

\(\dfrac{k+1-x}{w_t}<\dfrac{k-x}{w_t}\),

which is impossible.

The endpoint cases \(x=0\) and \(x=1\) are covered: every sign condition remains valid, and no division by either parameter occurs.

Converting the resulting rational masses back to fractions preserves support and satisfies all original constraints. Therefore the claimed equality between maximum fair welfare and \(W^*\) is established.

The attribution of the potential is also accurate: the same quadratic expression appears in [Montanari et al., Section 5](https://link.springer.com/article/10.1007/s00355-025-01599-6). The population-mass conclusion is proved directly here rather than assumed from the finite-agent theorem.

7. Dual formulation and bounded restriction

The dual signs and variables are correct. Supply inequalities yield nonnegative variables \(\alpha_c\); type equalities yield initially unrestricted variables \(\beta_t\). Empty-bundle constraints imply \(\beta_t\ge0\).

Strong duality applies because the finite primal LP is feasible and bounded.

The clipping argument for \(\alpha_c>1\) is valid. Before clipping, units of that class have negative weight; afterward they have zero weight. Removing those units preserves independence, so they cannot improve the maximum defining \(f_t\) in either case. Hence clipping leaves \(f_t\) unchanged and cannot increase the objective because supplies are nonnegative.

Setting \(\beta_t=f_t(\alpha)\) then preserves feasibility and cannot increase the objective. Nonnegative clone weights bounded by one, together with rank at most \(R\), give \(0\le f_t(\alpha)\le R\).

Thus the bounded restriction preserves the optimum.

8. Exact separation by matroid greedy optimization

The evaluation circuit correctly provides an independence oracle: a clone set is independent exactly when its rank equals its cardinality. All count vectors queried lie within the promised clone domain.

The greedy argument is valid for the nonnegative weights \(1-\alpha_c\). Its prefix-cardinality justification establishes maximum-weight independence, including tied and zero weights.

The correspondence between independent clone sets and clean configurations holds in both directions. Consequently, greedy computes exactly \(f_t(\alpha)\), and a maximizing configuration produces a genuinely violated dual constraint whenever \(f_t(\alpha)>\beta_t\).

The oracle is strong and exact, rather than approximate. It uses at most \(2Rm\) independence queries per type, with polynomial-time circuit evaluation, sorting, and rational arithmetic.

9. Polynomial-time optimization and decision

The stated separation-to-optimization theorem applies: the bounded dual has known dimension, an explicit bounding box, polynomial inequality encoding length, rational objective coefficients, and a polynomial-time strong separation oracle. This is the standard rational-polyhedron setting of [Grötschel, Lovász, and Schrijver](https://www.zib.de/userpage/groetschel/pubnew/paper/groetschellovaszschrijver1988.pdf).

Unary encoding of \(R\) ensures polynomial size of the explicit clone ground set. The procedure does not replicate population masses according to their potentially large denominators.

Exact optimization permits an exact comparison with the binary-rational threshold \(H\). Acceptance implies existence of rational fair fractions by Section 2; rejection excludes even an unfair feasible allocation meeting the threshold.

Zero supplies, rank-zero types, empty bundles, and thresholds outside the attainable welfare range introduce no exception to the argument.

Required feedback

No repair or additional clarification is needed for the claimed decision result. The output establishes polynomial-time decision and the welfare equality; efficient construction of the fair fractions is not required by the task.

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