Answer: —
Theorem 4.14 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateAlgorithm 1 always returns an allocation that is 𝑤-maximal with positive weights (and thus PO), and satisfies the capacity constraints. The allocation is EF[1,1], and EF1 for a same-sign instance.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given finitely many complete two-agent team types \(q\) with rational masses \(\rho_q\), rational item-type supplies \(\nu_o\), category capacities, and additive utilities \(u_{q,i}(o)\), choose masses \(z_{q,P}\) over whole pair configurations \(P=(B_1,B_2)\) such that \(\sum_P z_{q,P}=\rho_q\) and \(\sum_{q,P}z_{q,P}(n_o(B_1)+n_o(B_2))=\nu_o\) for every item type \(o\). Require every used configuration to be \(\mathrm{EF[1,1]}\), or EF1 on same-sign instances, and output positive weights \(\lambda_{q,i}\) certifying that \(z\) maximizes total weighted utility over all feasible configuration-mass assignments, or report that no such assignment exists.
A society is given by its support: the list of \(\tau\) ordered two-agent team types \(q\) with positive binary-rational masses \(\rho_q\), normalized by \(\sum_q\rho_q=1\). Here \(\tau\) is the support size, not the number of possible types; each type specifies both agents’ additive rational utilities \(u_{q,i}(o)\), which may be positive, negative, or zero.
There are \(m\geq1\) item types with positive binary-rational supplies \(\nu_o\), partitioned into \(k\) nonempty categories \(C_c\). Each category has a positive binary-encoded integer capacity \(s_c\), common to all agents, with \(\sum_{o\in C_c}\nu_o\leq2s_c\). Supplies are measured per unit mass of teams.
A configuration \(P=(B_1,B_2)\) consists of two finite multisets of whole item copies, allowing repeated item types, with \(\sum_{o\in C_c}n_o(B_i)\leq s_c\) for each \(i,c\). Counts are encoded in binary; configurations are implicit, and no inventory is prescribed separately for a team.
For type \(q\), a configuration is \(\mathrm{EF[1,1]}\) if, for each ordered pair \(i\neq j\), there are submultisets \(T\subseteq B_i\), \(G\subseteq B_j\), each of cardinality at most one, satisfying \(u_{q,i}(B_i\setminus T)\geq u_{q,i}(B_j\setminus G)\); if both are nonempty, their copies must belong to the same category. Empty removals are permitted.
An instance is same-sign if, for every \(q,i,c\), all \(u_{q,i}(o)\) in \(C_c\) are nonnegative or all are nonpositive. On these instances require mixed-goods-and-chores EF1 instead.
Find nonnegative rational configuration masses \(z_{q,P}\), represented by their nonzero entries, with \(\sum_Pz_{q,P}=\rho_q\) and \(\sum_{q,P}z_{q,P}(n_o(B_1)+n_o(B_2))=\nu_o\) for every \(o\), such that every used configuration satisfies the required fairness condition.
Also output rational weights \(\lambda_{q,i}>0\), normalized by \(\sum_{q,i}\lambda_{q,i}=1\), for which \(z\) maximizes \(\sum_{q,P}z_{q,P}\sum_{i=1}^{2}\lambda_{q,i}u_{q,i}(B_i)\) over all assignments satisfying the mass, supply, and capacity constraints, including assignments using unfair configurations; report nonexistence if no such pair \((z,\lambda)\) exists.
Is this search problem solvable in polynomial time, or is it NP-hard? State running times in \(m,\tau,k,L\), where \(L\) is the total binary input length, including capacities.
For a finite inventory divided between two agents, a polynomial-time algorithm finds a capacity-feasible \(\mathrm{EF[1,1]}\) allocation maximizing utility for positive agent weights, with EF1 on same-sign instances ([Shoshan, Hazon, and Segal-Halevi](https://arxiv.org/pdf/2205.07779)).
No result settling this exact configuration-mass problem was located in the literature search.
The general problem with freely chosen positive weights remains unclassified. I prove a new polynomial-time case:
If $\tau=1$ and every supply $\nu_o$ is an integer, the requested pair always exists and can be found in $O(m^4)\operatorname{poly}(L)$ time, even with signed utilities and binary-encoded capacities.
The algorithm returns a single configuration. Its running time depends on the number of item types, rather than the possibly enormous number of item copies.
I also establish polynomial-size certificates and an exact exponential algorithm for the general problem, repairing the rational-point qualification identified in the verifier’s report.
Write
$$
n_{i,o}(P)=n_o(B_i),
\qquad
a_o(P)=n_{1,o}(P)+n_{2,o}(P).
$$
An assignment is feasible if it satisfies the prescribed type masses and supplies and uses capacity-feasible configurations. It is fair if every positively used configuration satisfies the fairness condition required by the instance.
Fix a type $q$, a configuration $P$, and an ordered pair $i\neq j$. Define
$$
D_{q,i}(P)=u_{q,i}(B_i)-u_{q,i}(B_j).
$$
For each category $c$, let
$$
A_{q,i,c}(P)
=
\max\left(
\{0\}\cup
\{-u_{q,i}(o):o\in C_c,\ n_{i,o}(P)>0\}
\right),
$$
and
$$
G_{q,i,c}(P)
=
\max\left(
\{0\}\cup
\{u_{q,i}(o):o\in C_c,\ n_{j,o}(P)>0\}
\right).
$$
Removing an own item changes the utility difference by the negative of its utility; removing an item from the other bundle changes it by its utility. The included zero corresponds to an empty removal. Thus $\mathrm{EF[1,1]}$ for this ordered pair is equivalent to
$$
D_{q,i}(P)
+
\max_c\bigl(A_{q,i,c}(P)+G_{q,i,c}(P)\bigr)
\geq 0.
$$
Mixed-goods-and-chores EF1 is equivalent to
$$
D_{q,i}(P)
+
\max\left\{
\max_c A_{q,i,c}(P),
\max_c G_{q,i,c}(P)
\right\}
\geq 0.
$$
On a same-sign instance, each category has $A_{q,i,c}(P)=0$ or $G_{q,i,c}(P)=0$: nonnegative utilities preclude a beneficial own removal, and nonpositive utilities preclude a beneficial other-bundle removal. Consequently, the two displayed tests coincide.
These formulas give polynomial-time fairness tests with binary counts.
For fixed positive rational weights $\lambda$, define expected counts
$$
x_{q,i,o}=\sum_P z_{q,P}n_{i,o}(P).
$$
Consider the linear program
$$
\max\ \sum_{q,i,o}\lambda_{q,i}u_{q,i}(o)x_{q,i,o}
$$
subject to
$$
\sum_{q,i}x_{q,i,o}=\nu_o
\quad\text{for every }o,
$$
$$
\sum_{o\in C_c}x_{q,i,o}\leq \rho_qs_c
\quad\text{for every }q,i,c,
$$
and
$$
x_{q,i,o}\geq 0.
$$
Proposition 1. The rational feasible points of this linear program are exactly the expected-count vectors of feasible rational configuration assignments.
Proof. An assignment gives a feasible vector by summing its supply and capacity equations.
Conversely, let $x$ be a rational feasible vector. For each $q$, put
$$
v_{q,i,o}=\frac{x_{q,i,o}}{\rho_q}.
$$
For a fixed agent-category block, its vector satisfies
$$
v_o\geq 0,
\qquad
\sum_{o\in C_c}v_o\leq s_c.
$$
Represent this vector by a distribution that chooses $s_ce_o$ with probability $v_o/s_c$ for each $o\in C_c$, and chooses the zero vector with the remaining probability. Every chosen vector has integer counts and respects capacity.
Couple the $2k$ block distributions using a common parameter in $[0,1]$: place each block’s choices on consecutive intervals having the prescribed probabilities. The union of all interval endpoints partitions $[0,1]$ into intervals on which every block choice is constant. Each interval therefore specifies one configuration.
There are at most $2m$ internal endpoints, hence at most $2m+1$ configurations. Their probabilities and counts are rationally representable in polynomial space. Multiplying their probabilities by $\rho_q$ gives the desired configuration masses. $\square$
The qualification “rational feasible points” is essential: irrational linear-programming points cannot be represented by finitely many rational masses.
The linear program is nonempty because
$$
x_{q,i,o}=\frac{\rho_q\nu_o}{2}
$$
is feasible. It is bounded because
$$
x_{q,i,o}\leq \rho_qs_{c(o)}.
$$
Standard rational linear programming therefore supplies a rational optimum in
$$
\operatorname{poly}(m,\tau,k,L+\ell_\lambda)
$$
time, where $\ell_\lambda$ is the encoding length of the weights. Proposition 1 shows that its value is exactly the unrestricted assignment optimum.
Proposition 2. Suppose $z$ is globally optimal for positive weights $\lambda$. Every positively used configuration of type $q$ maximizes
$$
\lambda_{q,1}u_{q,1}(B_1)+\lambda_{q,2}u_{q,2}(B_2)
$$
among capacity-feasible divisions of its own inventory.
In particular,
$$
\lambda_{q,1}D_{q,1}(P)
+
\lambda_{q,2}D_{q,2}(P)
\geq 0
$$
for every positively used configuration $P$.
Proof. Replacing a positive-mass configuration by another division of the same inventory preserves its type mass and every supply. An improvement of its weighted utility would therefore improve the global objective.
Swapping its two bundles is capacity-feasible because capacities are common to the agents. The difference between the current weighted utility and that of the swapped configuration is exactly the displayed expression. Local optimality makes it nonnegative. $\square$
Thus both agents cannot strictly envy each other in a used configuration. Society-wide optimality additionally permits inventories to move between configurations, so this local property alone does not settle the task.
Assume throughout this section that $\tau=1$ and every $\nu_o$ is a positive integer. Since type masses sum to one, $\rho_1=1$. Suppress the type index.
The finite-inventory theorem guarantees fairness together with optimality for some positive weights; it does not guarantee fairness for arbitrary prescribed weights. This is the quantifier in [Shoshan, Hazon, and Segal-Halevi, Theorem 4.14](https://arxiv.org/pdf/2205.07779). The following argument proves that, in the present integer-supply case, its weight-sweep approach can be implemented without expanding binary multiplicities.
For category $c$, define
$$
N_c=\sum_{o\in C_c}\nu_o.
$$
Add one dummy type with zero utility for both agents and multiplicity
$$
2s_c-N_c.
$$
This is a nonnegative integer by the input hypothesis.
The augmented inventory now contains exactly $2s_c$ copies in category $c$. Give each agent exactly $s_c$ augmented copies from that category. Deleting dummy copies produces an original capacity-feasible allocation.
Dummy copies do not affect utilities or either fairness test: removing a dummy has the same utility effect as an empty removal.
There are at most
$$
M=m+k\leq 2m
$$
augmented types. All multiplicities remain binary encoded.
Use unnormalized positive weights $(r,1)$, where $r>0$. For an augmented type $o$, define
$$
\delta_o(r)=r\,u_1(o)-u_2(o).
$$
For a fixed category, the weighted utility equals a constant plus
$$
\sum_{o\in C_c}\delta_o(r)n_{1,o}.
$$
Hence an optimal augmented allocation gives agent 1 the $s_c$ copies with largest $\delta_o(r)$ and gives agent 2 the remaining copies. This allocation is found by sorting types and consuming their binary multiplicities in order.
This greedy allocation is optimal even among fractional divisions of the fixed inventory. To verify this, choose a cutoff value $\alpha$ so that the greedy count vector $n_1$ fills every type with score greater than $\alpha$, uses no type with score less than $\alpha$, and possibly divides types with score $\alpha$. For every fractional feasible vector $y_1$,
$$
\sum_o n_{1,o}=\sum_o y_{1,o}=s_c.
$$
Therefore
$$
\sum_o\delta_o(r)(n_{1,o}-y_{1,o})
=
\sum_o(\delta_o(r)-\alpha)(n_{1,o}-y_{1,o})
\geq 0.
$$
Each summand is nonnegative: above the cutoff, $n_{1,o}$ is the full multiplicity; below it, $n_{1,o}=0$; at the cutoff, the coefficient vanishes.
This also certifies optimality against assignments whose configurations have different inventories. Indeed, any feasible assignment has rational expected counts $x_{i,o}$ satisfying
$$
x_{1,o}+x_{2,o}=\nu_o,
\qquad
\sum_{o\in C_c}x_{i,o}\leq s_c.
$$
Complete its expected counts with
$$
x_{i,\mathrm{dummy}(c)}
=
s_c-\sum_{o\in C_c}x_{i,o}.
$$
These dummy counts are nonnegative and sum to $2s_c-N_c$. Thus the expected vector is a fractional division of the augmented fixed inventory. The greedy bound applies to it.
Consequently, every augmented greedy optimum, and every tied optimum constructed below, is globally optimal for the original configuration-mass problem.
Two score lines in the same category can change order only at
$$
r=
\frac{u_2(a)-u_2(b)}{u_1(a)-u_1(b)},
$$
when the denominator is nonzero and the ratio is positive.
There are at most $O(M^2)$ distinct positive crossing values. They have polynomial encoding length and can be sorted exactly.
Use a fixed order of type identifiers to break persistent ties.
For $r$ above every positive crossing, the ordering first prioritizes larger $u_1$. Thus agent 1 receives the top $s_c$ copies according to its own utility in every category. Pairing these top copies with the remaining copies shows
$$
u_1(B_1)\geq u_1(B_2).
$$
The initial allocation is envy-free for agent 1.
For $r$ below every positive crossing, agent 1 receives the bottom $s_c$ copies according to $u_2$. Agent 2 therefore receives its top copies and is envy-free.
If there are no positive crossings, the greedy allocation is constant for all $r>0$ and has both endpoint properties.
Consider a crossing value $r^\ast$. Let $n_1^+$ be the canonical greedy count vector immediately above it, and let $n_1^-$ be the vector immediately below it.
In each category, changes occur only within the score group that is tied at the selection cutoff at $r^\ast$. All higher groups remain fully selected, and all lower groups remain unselected. The number selected from the cutoff group is unchanged.
Therefore the transition can be performed by repeatedly choosing, in one category,
and exchanging a copy of $a$ from agent 1 with a copy of $b$ from agent 2.
These types satisfy
$$
\delta_a(r^\ast)=\delta_b(r^\ast).
$$
Every intermediate allocation remains optimal at weights $(r^\ast,1)$.
Moreover, put
$$
\Delta_1=u_1(a)-u_1(b),
\qquad
\Delta_2=u_2(a)-u_2(b).
$$
Above $r^\ast$, the greedy ordering puts $a$ no later than $b$: some $a$ is selected while some $b$ remains unselected. Hence
$$
\Delta_1\geq 0.
$$
The tie equality gives
$$
\Delta_2=r^\ast\Delta_1\geq 0.
$$
Such an exchange changes the utility differences by
$$
D_1^{\mathrm{new}}=D_1^{\mathrm{old}}-2\Delta_1,
\qquad
D_2^{\mathrm{new}}=D_2^{\mathrm{old}}+2\Delta_2.
$$
For an augmented allocation $A$, abbreviate its $\mathrm{EF[1,1]}$ correction by
$$
R_i(A)=\max_c\bigl(A_{i,c}(A)+G_{i,c}(A)\bigr).
$$
Lemma 3. Consider one tied exchange at positive weights $(r^\ast,1)$, with $\Delta_2=r^\ast\Delta_1$ as above. If the old allocation is not fair for agent 2, then the new allocation is fair for agent 1.
Proof. In the old allocation, agent 2 owns a copy of $b$ and the other agent owns a copy of $a$, in the same category. Therefore
$$
R_2(A^{\mathrm{old}})
\geq
\max\{0,-u_2(b)\}+\max\{0,u_2(a)\}
\geq \Delta_2.
$$
Failure of fairness for agent 2 implies
$$
D_2^{\mathrm{old}}<-\Delta_2.
$$
Suppose, for contradiction, that the new allocation fails fairness for agent 1. In that allocation, agent 1 owns $b$ and agent 2 owns $a$. Hence
$$
R_1(A^{\mathrm{new}})
\geq
\max\{0,-u_1(b)\}+\max\{0,u_1(a)\}
\geq \Delta_1,
$$
and thus
$$
D_1^{\mathrm{new}}<-\Delta_1.
$$
Using the exchange equation gives
$$
D_1^{\mathrm{old}}
=
D_1^{\mathrm{new}}+2\Delta_1
<
\Delta_1.
$$
It follows that
$$
r^\ast D_1^{\mathrm{old}}+D_2^{\mathrm{old}}
<
r^\ast\Delta_1-\Delta_2
=
0.
$$
This contradicts weighted optimality of the old allocation: swapping its complete bundles is feasible, so Proposition 2 makes this expression nonnegative. $\square$
Start with the initial greedy allocation. If agent 2 is already fair, both agents are fair because agent 1 is envy-free.
Otherwise, follow the tied exchanges while decreasing $r$. The final greedy allocation is envy-free for agent 2, so there is a first exchange after which agent 2 is fair. Immediately before that exchange, agent 2 is unfair. Lemma 3 makes the resulting allocation fair for agent 1 as well.
On same-sign instances, Section 1 shows that the resulting $\mathrm{EF[1,1]}$ allocation is EF1.
It remains to avoid performing exponentially many single-copy exchanges.
For a chosen surplus type $a$ and deficit type $b$, exchange up to
$$
t=
\min\left\{
n_{1,a}-n_{1,a}^{-},
\ n_{1,b}^{-}-n_{1,b}
\right\}
$$
copies. This positive integer is binary encoded.
After $h$ exchanges,
$$
D_2(h)=D_2(0)+2h\Delta_2.
$$
For every integer
$$
1\leq h\leq t-1,
$$
the set of types present in each bundle is constant. The increasing counts are positive throughout this range, and the decreasing counts cannot reach zero before its endpoint. Consequently, $R_2(h)$ is a constant $R_2^\circ$ on this range.
For $t\geq 2$, compute $R_2^\circ$ at $h=1$. If $\Delta_2>0$, the least interior integer satisfying fairness is
$$
h=
\max\left\{
1,\
\left\lceil
\frac{-R_2^\circ-D_2(0)}{2\Delta_2}
\right\rceil
\right\},
$$
provided it does not exceed $t-1$. If $\Delta_2=0$, either all interior integers satisfy fairness or none do. Check the endpoint $h=t$ separately, because a type may disappear there.
Thus the first fair allocation in a batch is found using a constant number of fairness evaluations and exact rational calculations. If no allocation in the batch is fair for agent 2, perform the whole batch and continue.
Each completed batch brings at least one type to its target count. Counts already at their targets are never changed again during that transition. There are therefore at most $O(M)$ batches per crossing value.
There are $O(M^2)$ crossing values, and a fairness evaluation takes $O(M)$ rational arithmetic operations. Including sorting and construction of the consecutive greedy vectors, the algorithm uses
$$
O(M^4)\operatorname{poly}(L)
=
O(m^4)\operatorname{poly}(L)
$$
bit operations. Counts, crossing ratios, and intermediate utility sums all have polynomial encoding length.
Delete dummy copies from the returned allocation $P$. Output
$$
z_{1,P}=1,
\qquad
\lambda_{1,1}=\frac{r}{1+r},
\qquad
\lambda_{1,2}=\frac{1}{1+r},
$$
where $r$ is the supporting ratio at which the algorithm stops.
This proves the announced polynomial-time result.
The dual of the compact linear program uses unrestricted item prices $p_o$ and nonnegative variables $t_{q,i,c}$, with constraints
$$
p_o+t_{q,i,c(o)}
\geq
\lambda_{q,i}u_{q,i}(o).
$$
Its objective is
$$
\sum_o p_o\nu_o
+
\sum_{q,i,c}\rho_qs_ct_{q,i,c}.
$$
For a capacity-feasible configuration, define its gap
$$
g_{q,P}
=
\sum_{i,c}s_ct_{q,i,c}
-
\sum_{i,o}
\bigl(\lambda_{q,i}u_{q,i}(o)-p_o\bigr)n_{i,o}(P).
$$
Equivalently,
$$
g_{q,P}
=
\sum_{i,c}
t_{q,i,c}
\left(s_c-\sum_{o\in C_c}n_{i,o}(P)\right)
+
\sum_{i,o}
\bigl(p_o+t_{q,i,c(o)}-\lambda_{q,i}u_{q,i}(o)\bigr)
n_{i,o}(P).
$$
Every term is nonnegative, so $g_{q,P}\geq 0$.
For any feasible assignment,
$$
\text{dual objective}-\text{weighted utility}
=
\sum_{q,P}z_{q,P}g_{q,P}.
$$
Thus dual feasibility and zero gaps on all positively used configurations certify unrestricted optimality.
Conversely, the compact primal is nonempty and bounded. Rational linear-programming strong duality supplies a rational optimal dual. Equality of objectives then forces every positive-mass gap to vanish.
Proposition 4. Every yes-instance has a requested pair using at most $m+\tau$ configurations and having polynomial total encoding length.
Proof. Start with a requested pair and an optimal dual certificate. Restrict to its positively used configurations. They are fair and have zero gaps.
Their mass equations form
$$
Az=b,
\qquad z\geq 0,
$$
with $m+\tau$ rows. This polytope is nonempty and bounded, since every mass is bounded by its type mass. A basic feasible solution has at most
$$
\operatorname{rank}(A)\leq m+\tau
$$
positive entries. Keeping these columns preserves fairness and optimality.
Fix the retained support $S$. To obtain small weights and dual variables, maximize $\epsilon$ subject to
$$
\epsilon\geq 0,
\qquad
\lambda_{q,i}\geq\epsilon,
\qquad
\sum_{q,i}\lambda_{q,i}=1,
$$
the dual inequalities, and
$$
g_{q,P}=0
\quad\text{for every }(q,P)\in S.
$$
The original positive weights make this system feasible with positive $\epsilon$. Normalization bounds its objective by $1/(2\tau)$. Its coefficients have polynomial encoding length: each configuration count is at most its binary-encoded category capacity.
The standard rational linear-programming theorem states that a feasible rational linear program with finite optimal value has a polynomial-size rational optimum and can be solved in polynomial time. Applying it here gives positive normalized weights and a polynomial-size dual certificate. The bounded mass system likewise has a polynomial-size rational basic solution. $\square$
Therefore the decision version of the requested free-weight problem belongs to $\mathrm{NP}$. A verifier checks capacities, fairness, masses, supplies, positive normalized weights, dual feasibility, and zero gaps.
Put $d_c=|C_c|$. The number of capacity-feasible configurations is
$$
N=
\prod_{c=1}^k
\binom{s_c+d_c}{d_c}^{\,2}.
$$
For one agent and category, the binomial coefficient counts nonnegative integer vectors whose sum is at most $s_c$; the square accounts for both agents.
Enumerate the fair labeled configurations $(q,P)$. For every support $S$ of size at most $m+\tau$, solve:
Accept the support exactly when the first system is feasible and the second has positive optimum $\epsilon$. Zero masses may be discarded. Zero gaps certify optimality for any feasible masses on the retained columns.
Proposition 4 proves completeness of this enumeration. Its running time is at most
$$
(\tau N+1)^{m+\tau}
\operatorname{poly}(m,\tau,k,L).
$$
Since
$$
N\leq
\prod_c(s_c+1)^{2d_c},
$$
this is
$$
2^{O\left((m+\tau)
\left(\sum_c d_c\log(s_c+1)+\log(\tau+1)\right)\right)}
\operatorname{poly}(m,\tau,k,L),
$$
and in particular
$$
2^{O((m+\tau)(mL+\log(\tau+1)))}
\operatorname{poly}(m,\tau,k,L).
$$
The algorithm produces a requested pair or correctly reports nonexistence.
A second tractable class allows arbitrary $\tau$ and rational supplies.
Proposition 5. Suppose that for every type $q$ there is a positive rational number $\alpha_q$ such that
$$
u_{q,2}(o)=\alpha_q u_{q,1}(o)
\quad\text{for every }o.
$$
Then the search problem is solvable in
$$
\operatorname{poly}(m,\tau,k,L)
$$
time.
Proof. Choose weights proportional to
$$
\lambda_{q,1}=\alpha_q,
\qquad
\lambda_{q,2}=1,
$$
then normalize all weights together. The two agents of each type now have identical weighted utility coefficients.
Solve the compact unrestricted linear program. Symmetrize its rational optimal solution by setting
$$
\bar x_{q,1,o}
=
\bar x_{q,2,o}
=
\frac{x_{q,1,o}+x_{q,2,o}}{2}.
$$
Supplies are preserved. Each capacity inequality is preserved by averaging its two feasible left-hand sides. The objective is preserved because the corresponding weighted coefficients are equal.
For each $q$, decompose the rational common bundle vector
$$
v_{q,o}=\frac{\bar x_{q,1,o}}{\rho_q}
$$
using the block construction in Proposition 1, now with only $k$ blocks. Use each resulting integer bundle twice, as $P=(B,B)$.
This realizes the optimal expected counts. Identical bundles are exactly envy-free for both agents, including with signed utilities. There are at most $m+1$ configurations per type.
The proportionality condition can be checked in polynomial time by taking a ratio at a nonzero utility coordinate and verifying all coordinates; if both utility vectors are zero, take $\alpha_q=1$. All subsequent steps use polynomial-time rational arithmetic and linear programming. $\square$
The new integer-supply algorithm uses a fixed integral augmented inventory. Its greedy fractional optimum has integral counts, and tied exchanges preserve that inventory. For nonintegral supplies, this argument does not provide a supply-realizing distribution whose every configuration is fair.
With multiple team types, a society-wide optimum can also move inventory between types. The one-dimensional weight sweep above does not control those transfers.
Accordingly, the remaining target is to prove either a polynomial-time algorithm for arbitrary rational supplies and arbitrary support size, or hardness for that exact problem with freely chosen positive weights. Hardness with prescribed weights does not establish this claim.
⟨structured verdict parsed — rendered above⟩
Overall assessment: partial. The output establishes substantial results: two polynomial-time special cases, polynomial-size certificates for yes-instances, and an exact exponential-time algorithm. It does not settle the general polynomial-time-versus-hardness question in USER_TASK, and explicitly acknowledges this.
I found no false central step. The special-case algorithms are sound in substance, with two minor implementation clarifications identified below.
The formulas in Section 1 are correct.
For an ordered pair $i\neq j$, removing an own copy contributes $-u_{q,i}(o)$ to the utility difference, and removing another agent’s copy contributes $u_{q,i}(o)$. Empty removals contribute zero. Within a fixed category, these choices are independent, so their largest combined correction is exactly
$$
A_{q,i,c}(P)+G_{q,i,c}(P).
$$
Taking the maximum over categories also permits a single nonempty removal: the other removal can be empty. Thus the displayed test matches the category restriction in USER_TASK.
The EF1 test correctly permits at most one removal in total.
For a same-sign category, either beneficial own removals are impossible or beneficial other-bundle removals are impossible. Consequently,
$$
A_{q,i,c}(P)+G_{q,i,c}(P)
=
\max\{A_{q,i,c}(P),G_{q,i,c}(P)\},
$$
and the two global tests coincide.
Zero utilities, empty bundles, and repeated copies cause no problem. Binary counts suffice for both presence tests and utility calculations.
Assessment: correct.
The forward implication follows directly from summing configuration masses and capacity inequalities.
For the converse, positivity of $\rho_q$ justifies division by $\rho_q$, and positivity of $s_c$ justifies the probabilities $v_o/s_c$. Their sum is at most one, so each block distribution is valid.
The common-parameter coupling preserves every block marginal and produces capacity-feasible integer configurations. Each agent-category block has at most $|C_c|$ internal endpoints. Summing over both agents and all categories gives at most $2m$ internal endpoints and hence at most $2m+1$ configurations.
Rational input coordinates produce rational endpoints and masses. The claimed polynomial encoding bound follows from the polynomial number of rational arithmetic operations and binary-encoded capacities.
The restriction to rational feasible vectors is correct.
The proposed vector
$$
x_{q,i,o}=\frac{\rho_q\nu_o}{2}
$$
satisfies the supply equalities because the type masses sum to one. Its category totals satisfy the capacity inequalities by the input assumption.
Nonnegativity and each category bound imply
$$
x_{q,i,o}\leq \rho_qs_{c(o)},
$$
so the feasible region is bounded. Rational linear programming therefore supplies a rational optimum of polynomial encoding length.
Proposition 1 establishes equality with the unrestricted configuration-assignment optimum.
Assessment: correct.
Proposition 2 uses an admissible replacement: another division of the same inventory preserves every item supply and the relevant type mass.
Because the configuration has positive mass, any strict improvement of its weighted utility would strictly improve the global objective.
Swapping the two bundles preserves capacity feasibility because capacities are common to both agents. The weighted difference is indeed
$$
\lambda_{q,1}D_{q,1}(P)+\lambda_{q,2}D_{q,2}(P).
$$
Its nonnegativity excludes simultaneous strict envy.
The output correctly warns that this local condition does not establish society-wide optimality or solve the general problem.
Assessment: correct.
The description of Theorem 4.14 is accurate: it guarantees an allocation maximizing weighted utility for positive weights selected by the algorithm, together with capacity feasibility and the stated fairness properties. It does not assert fairness for every prescribed positive weight vector. The relevant hypotheses are additive utilities, two agents, common category capacities, and a finite feasible inventory. These match the integer-supply setting when copies are viewed individually. [Shoshan, Hazon, and Segal-Halevi, Theorem 4.14](https://arxiv.org/pdf/2205.07779).
The compressed running-time claim is supported by the output’s own argument, rather than by applying the finite-copy running-time bound directly.
The dummy multiplicity is a nonnegative integer. Exact augmented bundle sizes become $s_c$ for each agent and category.
Deleting dummies preserves original capacities and utility differences. A zero-utility dummy removal has the same utility effect as an empty removal, so it does not create a fairness witness unavailable under the original definition.
The bound $M\leq 2m$ follows from nonempty categories.
The score
$$
\delta_o(r)=ru_1(o)-u_2(o)
$$
is the correct coefficient of the agent-one count after eliminating agent-two counts.
The cutoff calculation is valid, including tied types and fractional divisions. Above the cutoff, the greedy count is maximal; below it, the greedy count is zero. Thus every summand in the displayed optimality calculation is nonnegative.
The expected-count dummy completion is also valid: the two dummy counts sum to the available dummy multiplicity. This establishes optimality against assignments with varying inventories, which is essential for USER_TASK.
The crossing formula is correct when its denominator is nonzero. Identical score lines create persistent ties rather than missing events.
The extreme-order arguments establish the stated envy-free endpoint properties, including equal utility values and signed utilities.
At a crossing, only a cutoff tie group can change its selected counts. Surplus-to-deficit exchanges preserve category totals and remain optimal at the crossing weight.
The sign claims for $\Delta_1$ and $\Delta_2$ are valid: surplus and deficit types retain their respective relationships to the above-crossing greedy selection, even while the transition is processed. The displayed changes in $D_1$ and $D_2$ have the correct signs and factors of two.
Both lower bounds on the fairness corrections are valid. Failure of fairness gives strict inequalities, and the contradiction calculation correctly uses
$$
\Delta_2=r^\ast\Delta_1.
$$
Swapping the old bundles is an admissible comparison at the supporting positive weight.
The first exchange producing fairness for agent two therefore produces fairness for both agents. The endpoint argument guarantees that such an exchange exists unless the initial allocation already succeeds.
The presence sets are constant for integer indices $1\leq h\leq t-1$. Counts can become zero only at the separately tested endpoint.
The ceiling formula correctly finds the first fair interior integer when $\Delta_2>0$. The separate treatment of $\Delta_2=0$ and $t=1$ is sufficient. Checking the endpoint separately also handles changes in the correction term caused by disappearing types.
Each completed batch fixes at least one remaining surplus or deficit count. Hence the claimed polynomial batch bound is justified.
The resulting arithmetic-operation and bit-length bounds support
$$
O(m^4)\operatorname{poly}(L).
$$
Minor issue: Sections 3.3 and 3.6 do not explicitly specify how rational weights are chosen for the initial interval, the no-crossing case, and the “immediately above/below” greedy computations.
Minimum clarification: specify polynomial-bit rational representatives for those intervals and state which representative supplies the output weight if the algorithm stops initially. This is a routine implementation clarification, not a missing mathematical argument.
Assessment: sound in substance.
The compact dual has the correct signs and objective coefficients. Its item-price variables are unrestricted because supplies are equality constraints; its capacity multipliers are nonnegative.
The expanded gap expression is correct. Every term is nonnegative under capacity and dual feasibility. Summing gaps against masses gives exactly the dual-objective minus primal-objective difference.
Strong duality applies because the compact primal is feasible and bounded. Equality of objectives then forces every positively weighted gap to vanish.
For Proposition 4:
The rational linear-programming theorem invoked here is stated sufficiently precisely, and its hypotheses hold even though the auxiliary feasible region need not be bounded.
These arguments establish polynomial-size rational masses, weights, configurations, and dual witnesses. The listed verification checks are polynomial-time checks.
Assessment: correct; the associated existence decision problem belongs to $\mathrm{NP}$. This does not classify the search problem as polynomial-time solvable or hard.
The configuration count
$$
N=\prod_c\binom{s_c+d_c}{d_c}^{\,2}
$$
correctly counts capacity-feasible binary-count configurations.
Enumerating supports of size at most $m+\tau$ is complete by Proposition 4. The two feasibility tests are sufficient: zero gaps certify optimality for any supply-realizing masses on the selected columns.
Discarding zero masses is harmless.
The upper bound
$$
N\leq\prod_c(s_c+1)^{2d_c}
$$
is valid, since each coordinate lies between zero and its category capacity. The subsequent exponential bounds are consistent with binary capacity encoding.
Assessment: correct. This establishes decidability with the stated exponential bound, not the requested complexity classification.
The selected weights equalize the two weighted utility coefficients within each type. Symmetrization therefore preserves the objective, supplies, and capacity inequalities.
Applying the block decomposition to the common expected bundle and using each resulting bundle twice realizes the expected counts. Identical bundles are envy-free under signed utilities as well.
The support and running-time bounds are valid.
Minor issue: the proportionality-check description leaves the zero-coordinate cases implicit. In particular, an identically zero first utility vector and a nonzero second utility vector must be rejected, and a candidate ratio must be strictly positive.
Minimum clarification: state these rejection conditions and how zero coordinates are checked. The proposition’s proof under its stated hypothesis is unaffected.
Assessment: sound in substance.
The general target remains unresolved. The output proves neither a polynomial-time algorithm for arbitrary rational supplies and arbitrary support size nor hardness for freely chosen positive weights.
This is a major task-completion gap, explicitly acknowledged by the prover, rather than a contradiction in its subsidiary arguments.
The minimum requested follow-up is:
No demonstrated counterexample refutes the established special cases or certificate arguments.
⟨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.