← back to the atlas

Fair Allocation of Two Types of Chores (aamas23-00024)

Answer: Polynomial-time solvable for \(m=2\); every instance admits an EF1 and fPO allocation. A bit-complexity bound is \(O((\tau+L)\log(\tau+1)L^2)\), with at most \(2\tau+2\) positive-mass cohorts.

The anchor (named result in the paper)

Theorem 4.7 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateGiven a two chore types instance, Algorithm 1 finds an allocation that is EF1 and fPO in polynomial-time.

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

The continuous mirror question, as graded

Given finitely many valuation types \(\Theta\subseteq\mathbb{Q}_{<0}^{2}\), masses \(\mu\), and rational per-agent supplies \((\bar a,\bar b)\), find a finite-support mass allocation \(\lambda_{\theta,a,b}\) over integral bundles \((a,b)\in\mathbb{Z}_{\ge 0}^{2}\) satisfying \(\sum_{a,b}\lambda_{\theta,a,b}=\mu_{\theta}\), \(\sum_{\theta,a,b}a\lambda_{\theta,a,b}=\bar a\), and \(\sum_{\theta,a,b}b\lambda_{\theta,a,b}=\bar b\), such that every positive-mass cohort is EF1 and the allocation is \(fPO\) against all supply-preserving fractional reallocations.

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

A society is given by its support: a nonempty list \(\Theta\subseteq\mathbb Q_{<0}^{2}\) of \(\tau\) valuation types with positive binary-rational masses \(\mu_\theta\), where \(\sum_\theta\mu_\theta=1\). Here \(\tau\) is the support size, not the number of possible types. There are \(m=2\) chore types; utility is additive, \(u_\theta(a,b)=\theta_Aa+\theta_Bb\), and per-agent supplies \((\bar a,\bar b)\in\mathbb Q_{\ge0}^{2}\) are encoded in binary.
An allocation has finitely many nonzero binary-rational masses \(\lambda_{\theta,a,b}\ge0\), indexed by integral bundles \((a,b)\in\mathbb Z_{\ge0}^{2}\), satisfying \(\sum_{a,b}\lambda_{\theta,a,b}=\mu_\theta\), \(\sum_{\theta,a,b}a\lambda_{\theta,a,b}=\bar a\), and \(\sum_{\theta,a,b}b\lambda_{\theta,a,b}=\bar b\). A positive-mass cohort consists of the agents of type \(\theta\) receiving bundle \((a,b)\).
EF1 is required between every ordered pair of positive-mass cohorts, including cohorts of the same type: an empty own bundle satisfies it automatically; otherwise, deleting one chore from the envious cohort's own bundle must make its utility at least its utility for the other cohort's bundle.
Fractional Pareto optimality (fPO) excludes any supply-preserving reassignment of nonnegative real bundles to the agents that weakly improves utility almost everywhere and strictly improves utility on a set of positive mass; cohorts may be subdivided in such a reassignment.
Is finding such an EF1 and fPO allocation, or determining that none exists, solvable in polynomial time, or is it NP-hard? State running times in \(m=2\), \(\tau\), and the total binary input length \(L\).
For finitely listed agents and explicitly listed chores of two types, an EF1 and fPO allocation always exists and is computable in polynomial time ([Aziz et al.](https://arxiv.org/html/2211.00879v2)); this extends to weighted EF1 and fPO for finite agents ([Garg et al.](https://www.ijcai.org/proceedings/2024/0310.pdf)).
No result settling exactly the mass-allocation problem defined 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 problem is polynomial-time solvable for \(m=2\), and every instance admits an EF1 and fPO allocation.

Here, “binary-rational” means a rational encoded by binary numerator and denominator. The algorithm below outputs at most \(2\tau+2\) positive-mass cohorts, with total encoding length \(O(\tau L)\). Using schoolbook integer arithmetic, its running time is

\(O\!\left((\tau+L)\log(\tau+1)L^2\right).\)

The proof is direct and does not expand the society into individual agents.

1. A family of allocations indexed by a population cut

Write \(a=\bar a\), \(b=\bar b\), and replace negative utilities by positive disutilities:

\(d_{iA}=-\theta_{iA}>0,\qquad d_{iB}=-\theta_{iB}>0,\qquad r_i=d_{iA}/d_{iB}.\)

Sort the supported types so that \(r_1\leq\cdots\leq r_\tau\), breaking ties arbitrarily. Let

\(s_0=0,\qquad s_i=\sum_{j=1}^{i}\mu_j.\)

First suppose \(a,b>0\). For a cut \(\alpha\in(0,1)\), put

\(\mu_i^A=\min\{\mu_i,\max\{0,\alpha-s_{i-1}\}\},\qquad \mu_i^B=\mu_i-\mu_i^A.\)

Thus the first \(\alpha\) units of population mass receive only A chores, and the remaining \(1-\alpha\) receive only B chores. At most one type is split between these parts.

Define

\(q_A=a/\alpha,\qquad q_B=b/(1-\alpha),\)

\(k_A=\lfloor q_A\rfloor,\qquad k_B=\lfloor q_B\rfloor,\)

\(\delta_A=q_A-k_A,\qquad \delta_B=q_B-k_B.\)

For each type \(i\), assign the following masses:

| Bundle | Mass |
|---|---|
| \((k_A,0)\) | \(\mu_i^A(1-\delta_A)\) |
| \((k_A+1,0)\) | \(\mu_i^A\delta_A\) |
| \((0,k_B)\) | \(\mu_i^B(1-\delta_B)\) |
| \((0,k_B+1)\) | \(\mu_i^B\delta_B\) |

Discard zero masses and combine identical bundles.

Every type receives its prescribed mass. Moreover, the total A supply is

\(\sum_i\mu_i^A(k_A+\delta_A)=\alpha q_A=a,\)

and similarly the total B supply is \(b\). Therefore this is a feasible allocation, denoted \(X(\alpha)\).

2. Every cut allocation is fPO

Let

\(r_A(\alpha)=\max\{r_i:\mu_i^A>0\},\qquad r_B(\alpha)=\min\{r_i:\mu_i^B>0\}.\)

Sorting implies \(r_A(\alpha)\leq r_B(\alpha)\). Choose any \(r\) in this interval and define the positive linear functional

\(p(x,y)=rx+y.\)

For type \(i\), put

\(\kappa_i=\min\{d_{iA}/r,d_{iB}\}>0.\)

Every nonnegative real bundle \(z\) satisfies

\(d_i(z)\geq\kappa_i p(z).\)

Every bundle allocated to type \(i\) in \(X(\alpha)\) satisfies equality:

Suppose a supply-preserving real reassignment gives each agent a bundle \(z\), weakly decreasing disutility almost everywhere. If its original bundle was \(x\), then

\(\kappa_i p(z)\leq d_i(z)\leq d_i(x)=\kappa_i p(x),\)

hence \(p(z)\leq p(x)\). Wherever utility strictly improves, the last inequality is strict.

Consequently, strict improvement on a set of positive mass implies a strict decrease in the integral of \(p\). Indeed, \(p(x)-p(z)\) is nonnegative almost everywhere and positive on a set of positive mass. But supply preservation fixes that integral at \(ra+b\), a contradiction.

Thus \(X(\alpha)\) is fPO. This argument allows arbitrary cohort subdivision.

3. An exact EF1 test

Define

\(c_A=\lceil q_A\rceil-1,\qquad c_B=\lceil q_B\rceil-1.\)

Since \(a,b>0\), both \(c_A,c_B\) are nonnegative. Also,

\(c_A\leq k_A,\qquad c_B\leq k_B.\)

Within the A-only part, bundle sizes differ by at most one. Deleting one A chore from any nonempty own bundle leaves at most \(k_A\) chores, while every other A-only bundle contains at least \(k_A\). Therefore every ordered comparison within this part satisfies EF1. The same holds within the B-only part.

For comparisons across the parts, the largest remaining A-only bundle after deletion contains exactly \(c_A\) chores, while the smallest B-only bundle contains \(k_B\). Every type with positive A mass receives the same bundle-size support, so the worst A-to-B comparison occurs at ratio \(r_A(\alpha)\). Thus A-to-B EF1 holds exactly when

\(r_A(\alpha)c_A\leq k_B.\)

Similarly, B-to-A EF1 holds exactly when

\(c_B\leq r_B(\alpha)k_A.\)

These tests include comparisons between cohorts of the same type.

Call the cut A-bad if the first inequality fails, B-bad if the second fails, and fair if neither fails. A cut cannot be both A-bad and B-bad: otherwise,

\(r_Ak_A\geq r_Ac_A>k_B\geq c_B>r_Bk_A,\)

contradicting \(r_A\leq r_B\).

Hence every cut has exactly one of these three statuses.

4. A transition from A-bad to B-bad contains a fair cut

The quantities in the EF1 test are locally constant except at cuts of the forms

\(s_i,\qquad a/k,\qquad 1-b/\ell,\)

where \(k,\ell\) are positive integers.

We now check the status at such a breakpoint \(z\in(0,1)\). Superscripts \({}^-\) and \({}^+\) denote values immediately to its left and right.

Because \(q_A=a/\alpha\) decreases with \(\alpha\),

\(c_A(z)=c_A^+,\qquad k_A(z)=k_A^-.\)

Because \(q_B=b/(1-\alpha)\) increases with \(\alpha\),

\(k_B(z)=k_B^+,\qquad c_B(z)=c_B^-.\)

These identities also hold when the corresponding quantity has no jump. Sorting the types gives

\(r_A(z)\leq r_A^+,\qquad r_B(z)\geq r_B^-.\)

Therefore:

\(r_A(z)c_A(z)\leq r_A^+c_A^+\leq k_B^+=k_B(z)\).

\(c_B(z)=c_B^-\leq r_B^-k_A^-\leq r_B(z)k_A(z)\).

In particular, if the left side is A-bad and the right side is B-bad, neither side has the other bad status, by Section 3. Both implications apply, so the exact breakpoint \(z\) is fair.

We will also use the contrapositives: an A-bad breakpoint has an A-bad right side, and a B-bad breakpoint has a B-bad left side.

5. Finding a fair cut in polynomial time

Initial bracket

Let \(r_{\min}=r_1\), \(r_{\max}=r_\tau\), and choose

\(\displaystyle \varepsilon=\min\left\{\frac14,\frac{ar_{\min}}{2(2b+r_{\min}+1)},\frac{b}{2(2r_{\max}a+1)}\right\}.\)

This is a positive rational of \(O(L)\) bits.

At \(\alpha=\varepsilon\), we have \(k_B\leq 2b\), whereas

\(\displaystyle r_Ac_A\geq r_{\min}\left(\frac a\varepsilon-1\right)\geq 4b+r_{\min}+2>2b.\)

Thus this cut is A-bad.

At \(\alpha=1-\varepsilon\), we have \(k_A\leq 2a\), whereas

\(\displaystyle c_B\geq\frac b\varepsilon-1\geq4r_{\max}a+1>2r_{\max}a\geq r_Bk_A.\)

Thus this cut is B-bad.

Start with the bracket \([u,v]=[\varepsilon,1-\varepsilon]\).

Bisection

Evaluate the status of the midpoint:

The endpoints remain A-bad and B-bad, respectively. No global monotonicity assumption is needed.

To bound the number of iterations, let \(d_a,d_b,d_i\) be the input denominators of \(a,b,\mu_i\), and set

\(\displaystyle U=1+\left\lceil\frac{\max\{a,b\}}{\varepsilon}\right\rceil,\qquad D=U\,d_a d_b\prod_{i=1}^{\tau}d_i.\)

Every breakpoint in \([\varepsilon,1-\varepsilon]\) has reduced denominator at most \(D\):

Distinct rationals with denominators at most \(D\) differ by at least \(1/D^2\). Furthermore, \(\log D=O(L)\). Consequently, after \(O(L)\) bisections, either a fair midpoint has been found or

\(v-u<1/D^2.\)

In the latter case, the closed bracket contains at most one distinct breakpoint. It contains at least one, because the status is constant on intervals without breakpoints and the endpoint statuses differ.

That breakpoint cannot equal \(u\): an A-bad breakpoint has an A-bad right side, which would force \(v\) to be A-bad. Likewise, it cannot equal \(v\). Thus there is exactly one breakpoint \(z\in(u,v)\); its left side is A-bad and its right side is B-bad. Section 4 proves that \(z\) is fair.

Exact extraction of the breakpoint

Extraction uses only rational arithmetic:

\(\lceil a/v\rceil\leq k\leq\lfloor a/u\rfloor\).

\(\lceil b/(1-u)\rceil\leq\ell\leq\lfloor b/(1-v)\rfloor\).

Each integer range contains at most one integer; two would give two distinct breakpoints in the bracket. Deduplicating the candidates yields \(z\).

The algorithm therefore finds an exact rational fair cut.

6. Zero supplies and encoding bounds

If \(b=0\), assign every type only A bundles of sizes \(\lfloor a\rfloor\) and \(\lceil a\rceil\), using the same proportions for every type to obtain mean \(a\). Bundle sizes differ by at most one, so the allocation is EF1.

For fPO, any supply-preserving reassignment has zero B quantity almost everywhere. Since all A disutilities are positive, weak improvement requires each agent’s A quantity to weakly decrease; strict improvement on positive mass would strictly decrease total A supply. This is impossible. The case \(a=0\) is symmetric; if both supplies vanish, assign everyone the empty bundle.

For positive supplies, every cut examined lies in \([\varepsilon,1-\varepsilon]\), so all output bundle coordinates are bounded by \(U\) and have \(O(L)\) bits. Bisection endpoints can be stored on successive dyadic refinements of the initial rational bracket; after \(O(L)\) iterations they still have \(O(L)\) bits. The extracted breakpoint and all output masses likewise have \(O(L)\) bits.

Each unsplit type receives at most two bundles, and at most one split type receives four. Thus the output has at most \(2\tau+2\) positive cohorts and total length \(O(\tau L)\).

Sorting takes \(O(\tau\log(\tau+1))\) rational comparisons. Each of the \(O(L)\) bisections locates the cut among cumulative masses using \(O(\log(\tau+1))\) comparisons, then performs a constant number of rational operations. Breakpoint extraction and output construction use \(O(\tau)\) further operations. All operands have \(O(L)\) bits. With schoolbook arithmetic, this proves the stated bound

\(O\!\left((\tau+L)\log(\tau+1)L^2\right).\)

Thus the search problem belongs to polynomial time for \(m=2\), with unrestricted support size \(\tau\) and binary-encoded supplies. Under the stated assumptions, there are no nonexistence instances.

⟨structured verdict parsed — rendered above⟩

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

Verdict

The prover resolves the task correctly under its explicitly stated interpretation of “binary-rational” as a rational represented by binary numerator and denominator. The construction produces an EF1 and fPO allocation for every permitted instance and has polynomial bit complexity for \(m=2\).

I found no major or minor issues requiring repair.

Step-by-step verification

1. Feasibility of the cut allocation

The conversion from negative utilities to positive disutilities preserves both the EF1 comparisons and Pareto comparisons, with the inequality directions reversed appropriately.

Because all masses are positive, the cumulative masses strictly increase from \(s_0=0\) to \(s_\tau=1\). The definitions of \(\mu_i^A\) and \(\mu_i^B\) therefore give

\[ \sum_i\mu_i^A=\alpha,\qquad \sum_i\mu_i^B=1-\alpha, \]

and split at most one supported type.

For positive supplies and \(\alpha\in(0,1)\), both means \(q_A,q_B\) are positive. Their fractional parts lie in \([0,1)\), so all listed cohort masses are nonnegative. The two masses assigned within each part sum to that type’s mass in the part. Their mean bundle sizes are exactly \(q_A\) and \(q_B\), respectively.

Thus the type-mass constraints and both supply constraints hold exactly. For rational \(\alpha\), the construction uses finitely many rational masses and integral nonnegative bundles. Discarding zero masses and combining identical bundles preserves feasibility.

Assessment: Correct.

2. Fractional Pareto optimality

Both population parts have positive mass, so \(r_A(\alpha)\) and \(r_B(\alpha)\) are defined. Sorting ensures \(r_A(\alpha)\leq r_B(\alpha)\), including when a type is split or valuation ratios coincide.

The chosen \(r\) is positive. The definition of \(\kappa_i\) gives the asserted inequality for every nonnegative real bundle. Equality holds on every allocated bundle:

For a weakly improving reassignment, the displayed inequality correctly implies \(p(z)\leq p(x)\) almost everywhere. Strict utility improvement implies strict inequality there because \(\kappa_i>0\).

The integral argument is valid. Supply preservation makes both nonnegative coordinates integrable, and consequently fixes the integral of \(p\). A nonnegative measurable difference that is positive on a set of positive mass has positive integral. Hence the asserted strict improvement contradicts supply preservation.

The argument applies agent by agent and therefore covers cohort subdivision and arbitrary nonnegative real reassignment bundles.

Assessment: Correct; it establishes the stated fPO notion.

3. Exact EF1 characterization

Within either part, positive-mass bundle sizes differ by at most one. Deleting a chore from a nonempty own bundle therefore leaves no more chores than any comparison bundle in that same part.

For cross-part comparisons, the largest positive-mass own bundle after deletion has size \(c_A\) or \(c_B\). This remains correct when the mean is integral: the larger listed bundle then has zero mass, and the remaining size is the integral mean minus one. When the mean is below one, the only nonempty bundle has size one, so deletion leaves zero.

The smallest positive-mass comparison bundle has size \(k_A\) or \(k_B\). Every type with positive mass in a part receives the same bundle-size support. Consequently, the extrema used in the EF1 test are attained by positive-mass cohorts.

The two inequalities are therefore necessary and sufficient for all cross-part ordered comparisons, including comparisons within a split type.

The proof that both inequalities cannot fail is also valid. All quantities involved are nonnegative, and the displayed strict chain contradicts \(r_A\leq r_B\), including when \(k_A=0\).

Assessment: Correct.

4. Breakpoint behavior

The listed breakpoints cover every possible change in the floor, ceiling, and supported-type extrema. On the compact initial bracket, only finitely many such breakpoints occur.

The one-sided identities are correct:

These conclusions remain valid when several breakpoint events coincide.

Each implication about the breakpoint status follows with the correct inequality direction. Thus an A-bad left side and a B-bad right side imply that the exact breakpoint is fair. The stated contrapositives follow as well.

Assessment: Correct.

5. Initial bracket and bisection

The chosen \(\varepsilon\) is positive and at most one quarter. Therefore both initial endpoints lie strictly inside \((0,1)\).

The initial estimates are correct. In particular,

\[ r_{\min}\left(\frac a\varepsilon-1\right) \geq 4b+r_{\min}+2, \]

and

\[ \frac b\varepsilon-1\geq 4r_{\max}a+1. \]

Together with the stated upper bounds on the opposite part’s floor, these establish that the left endpoint is A-bad and the right endpoint is B-bad.

Each bisection update preserves those endpoint statuses. The argument does not require global monotonicity.

The denominator bound is valid for all three breakpoint families. Distinct rationals with reduced denominators at most \(D\) are separated by at least \(1/D^2\). Since \(\log D=O(L)\), the bracket reaches smaller width after \(O(L)\) bisections.

At that width, differing endpoint statuses force a breakpoint to exist, and separation permits at most one. The contrapositives from Section 4 exclude either endpoint from being that breakpoint. The unique interior breakpoint therefore has the required left and right statuses and is fair.

Assessment: Correct.

6. Exact breakpoint extraction

Both integer-range tests correctly invert the corresponding breakpoint formulas, with the inequality directions preserved.

Each integer range contains at most one integer because distinct positive integers produce distinct breakpoints within that family. Scanning cumulative masses and deduplicating coincident candidates therefore identifies the unique breakpoint exactly.

No enumeration proportional to the numerical supply or bundle size is required.

Assessment: Correct.

7. Zero supplies

With one zero supply, the proposed floor/ceiling allocation is feasible and EF1, including empty own bundles.

In any nonnegative real supply-preserving reassignment, the zero-supply chore coordinate must vanish almost everywhere. Since the remaining chore has strictly positive disutility for every type, weak improvement requires its quantity to decrease weakly agent by agent. Strict improvement on positive mass would contradict preservation of its total supply.

When both supplies vanish, the empty allocation is feasible, EF1, and fPO.

Assessment: Correct.

8. Encoding and running time

The quantities \(\varepsilon\), \(U\), and \(D\) have \(O(L)\)-bit representations. The denominator product contributes at most the sum of the input denominator lengths.

After \(O(L)\) bisections, the endpoints still have \(O(L)\) bits. Extracted breakpoints, bundle coordinates, and output masses also have \(O(L)\) bits. Exact rational operations can maintain these bounds using reduced representations.

The cohort count is valid: every unsplit type contributes at most two cohorts, and the sole possible split type contributes at most four. Combining identical bundles only decreases this count.

The sorting, binary searches, extraction, and output construction fit the claimed bound

\[ O\!\left((\tau+L)\log(\tau+1)L^2\right) \]

with schoolbook exact arithmetic. The output length is \(O(\tau L)\).

Assessment: Correct.

The construction settles the requested search problem for \(m=2\) and unrestricted support size \(\tau\). No repair or additional lemma 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.