← back to the atlas

Approval-Based Voting with Mixed Goods (aaai23-25717)

Answer: Exact computation is possible in time polynomial in \(m,\tau,k,L\). Every output satisfies \(\mathrm{mass\text{-}EJR\text{-}1}\), and also its strong analogue.

The anchor (named result in the paper)

Theorem 3.11 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateGeneralized MES satisfies EJR-1 and can be implemented in polynomial time. For indivisible-goods instances, Generalized MES re- duces to the original MES of Peters and Skowron (2020), which satisfies indivisible-goods EJR. We prove that the analog holds for cake instances.

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

The continuous mirror question, as graded

Given mixed divisible and indivisible goods, capacity alpha, finitely many approval types with rational masses, compute the deterministic mass-Generalized-MES allocation and establish its mass-EJR-1 guarantee in time polynomial in the type count, resource description, and encoding length.

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

A society is given by its support: \(\tau\ge1\) approval types with positive binary-rational masses \(w_i\), normalized by \(\sum_i w_i=1\); \(\tau\) is the support size, not the number of possible types.
The resource is \(R=([0,c],G)\), with \(c\ge0\), \(m=|G|\), \(c+m>0\), and rational capacity \(0<\alpha\le c+m\). Type \(i\) approves \(R_i=(C_i,G_i)\), where \(C_i\) is an explicitly listed finite union of intervals with rational endpoints and \(G_i\subseteq G\). Each indivisible good has size and cost \(1\); cake has size and cost equal to length.
An allocation \(A=(D,H)\) is collectively shared, with \(s(A)=\ell(D)+|H|\le\alpha\) and \(u_i(A)=\ell(C_i\cap D)+|G_i\cap H|\). Interval endpoints are immaterial. Partition the cake at all approval endpoints into \(k\) positive-length cells, ordered from left to right; label goods in input order. Let \(L\) be the total input bit length.
Define mass-Generalized-MES as follows. Start with empty allocation and remaining budget density \(b_i=\alpha\) for every type; its remaining total budget is \(w_i b_i\). Exhausted types do not participate further.
For a remaining good \(g\), let \(S_g=\{i:b_i>0,\ g\in G_i\}\); it is \(\rho\)-affordable when \(\rho\ge0\) and \(\sum_{i\in S_g}w_i\min\{b_i,\rho\}=1\).
For a remaining cell interval \(I=[a,d]\), let \(S_I=\{i:b_i>0,\ I\subseteq C_i\}\); its prefix of length \(q\in(0,d-a]\) is \((q,\rho)\)-affordable when \(\rho\ge0\) and \(\sum_{i\in S_I}w_i\min\{b_i,q\rho\}=q\).
At each step select a good or cell attaining the least affordable \(\rho\), breaking ties by placing goods before cells and then using their specified orders; for the selected cell take the largest affordable \(q\) at that \(\rho\). Add the good or prefix, remove it from the remaining resource, and deduct \(\min\{b_i,\rho\}\) or \(\min\{b_i,q\rho\}\), respectively, from each approving active type's budget density. Stop when nothing is affordable.
A coalition is a vector \(z\) with \(0\le z_i\le w_i\) and \(\sum_i z_i>0\), allowing arbitrary real portions of types. For \(t>0\), it is \(t\)-cohesive if \(\sum_i z_i\ge t/\alpha\) and \(s(\bigcap_{i:z_i>0}R_i)\ge t\). Mass-EJR-1 requires, for every such \(t\) and coalition, some \(i\) with \(z_i>0\) to have \(u_i(A)>t-1\).

Is exact computation of this deterministic mass-Generalized-MES allocation possible in time polynomial in \(m,\tau,k,L\), or is it NP-hard? Does its output always satisfy mass-EJR-1?

For a finite list of equally weighted agents, Generalized MES is polynomial-time computable and satisfies EJR-1; the journal version additionally establishes strong EJR-1. [Verified finite-society result](https://link.springer.com/article/10.1007/s00355-024-01511-8).
No result settling the exact mass problem defined here was identified in the literature search.

Modeling choices made when packaging the task

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

1. Result

Exact computation is possible in time polynomial in \(m,\tau,k,L\), and every output satisfies mass-EJR-1.

The finite-society analogue is established in [Theorem 3.13 of the cited paper](https://link.springer.com/article/10.1007/s00355-024-01511-8). The proof below works directly with the encoded masses: it bounds both the number of iterations and the bit lengths of intermediate rational numbers.

Throughout, cake sets are identified up to interval endpoints.

2. Exact prices and cake prefixes

At any intermediate stage, let \(b_i\) denote the remaining budget density of type \(i\).

Cake cells

Consider a remaining cell interval of length \(d>0\). Let \(S\) be its active approving types, and put \(W=\sum_{i\in S}w_i\).

If \(S\) is empty, no positive prefix is affordable. Otherwise, affordability implies

\(\displaystyle q=\sum_{i\in S}w_i\min\{b_i,q\rho\}\le q\rho W.\)

Since \(q>0\), necessarily \(\rho\ge 1/W\).

Conversely, at \(\rho=1/W\), every prefix satisfying

\(\displaystyle 0<q\le \min\left\{d,\;W\min_{i\in S}b_i\right\}\)

is affordable: each participating type pays density \(q/W\), and the weighted payments sum to \(q\).

Moreover, these are exactly the affordable prefixes at this price. Indeed, each summand in the preceding inequality is bounded above by \(w_iq/W\). Equality of the sums, with every \(w_i>0\), requires \(b_i\ge q/W\) for every \(i\in S\).

Thus the exact cell candidate is

\(\displaystyle \rho_{\mathrm{cell}}=\frac1W,\qquad q_{\mathrm{cell}}=\min\left\{d,\;W\min_{i\in S}b_i\right\}.\)

If this prefix does not finish the cell, at least one active approving type becomes exhausted.

Indivisible goods

For a remaining good with active approving set \(S\), define

\(\displaystyle F(\rho)=\sum_{i\in S}w_i\min\{b_i,\rho\}.\)

The function \(F\) is continuous and nondecreasing, starts at zero, and becomes constant at \(\sum_{i\in S}w_ib_i\). Hence the good is affordable exactly when

\(\displaystyle \sum_{i\in S}w_ib_i\ge1.\)

When affordable, its least price is the first solution of \(F(\rho)=1\). Sorting the budgets identifies the linear segments of \(F\), so this price is computed exactly using polynomially many rational operations.

More explicitly, at the least price let

\(\displaystyle E=\{i\in S:b_i<\rho\},\qquad U=\{i\in S:b_i\ge\rho\}.\)

The least price is at most the largest approving budget, so \(U\ne\varnothing\). The affordability equation gives

\(\displaystyle \rho=\frac{1-\sum_{i\in E}w_ib_i}{\sum_{i\in U}w_i}.\)

This formula also covers the boundary case in which the total approving budget equals one.

3. Polynomial-time exact computation

Number of iterations and feasibility

Compute the candidates above for every remaining good and cell. Choose the least price using the prescribed order for ties, and perform the specified purchase.

Every purchase causes at least one of the following:

For counting purposes, charge a good purchase to that good, a cell-finishing purchase to that cell, and any other purchase to a newly exhausted type. No object receives two charges. Therefore the number of purchases is at most \(N=m+k+\tau\).

Also, every purchase decreases total remaining budget by exactly its size. Initially the total budget is \(\sum_iw_i\alpha=\alpha\). Consequently, at every stage,

\(\displaystyle s(A)=\alpha-\sum_iw_ib_i\le\alpha.\)

Thus the computed allocation is feasible.

Bit complexity

A polynomial bound on rational operations alone would not establish polynomial time. We next bound their operand lengths.

Choose a common denominator \(Q\) for the input masses, and write

\(\displaystyle w_i=\frac{a_i}{Q},\qquad a_i\in\mathbb Z_{>0},\qquad \sum_i a_i=Q.\)

Taking the product of the input denominators gives \(\log Q=O(L)\). Choose likewise an initial denominator \(D_0\) for \(\alpha\) and all cake endpoints, with \(\log D_0=O(L)\).

Suppose all current budget densities and cake endpoints have common denominator \(D\).

For a good purchase, write \(b_i=p_i/D\) and \(A_U=\sum_{i\in U}a_i\). Its price is

\(\displaystyle \rho=\frac{QD-\sum_{i\in E}a_ip_i}{DA_U}.\)

After deducting the payments, all updated budgets and endpoints have common denominator \(DA_U\). Since \(1\le A_U\le Q\), this adds at most \(\log Q\) denominator bits.

For a cell purchase, write \(A_S=\sum_{i\in S}a_i\), so \(W=A_S/Q\). The purchased length is either the remaining cell length or \(A_Sb_{\min}/Q\). Accordingly, its denominator divides \(DQ\). The density payment is \(qQ/A_S\), so all updated budgets and endpoints have common denominator \(DQA_S\). This adds at most \(2\log Q\) denominator bits.

It follows that after \(j\) purchases a common denominator can be chosen satisfying

\(\displaystyle \log D_j\le\log D_0+2j\log Q.\)

Because \(j\le N\), this is polynomial in the requested parameters. Budget densities remain between zero and \(\alpha\), and endpoints remain between zero and \(c\), so their numerators also have polynomial bit length. Good prices are at most \(\alpha\), and cell prices are at most \(Q\); their encodings are polynomial as well.

Candidate evaluation, sorting, exact comparison, and budget updates therefore use polynomial-time integer arithmetic. Preprocessing the approval cells is polynomial too.

Finally, every purchase from a cell takes a prefix of its remaining suffix. Thus the final selected cake within each original cell is itself a prefix, and the output has at most \(k\) rational cake intervals.

This proves polynomial-time exact computation of the prescribed deterministic allocation.

4. Mass-EJR-1

Let \(A\) be the final allocation. Fix any \(t>0\) and any \(t\)-cohesive coalition \(z\). Define its support, mass, and common resource by

\(\displaystyle B=\{i:z_i>0\},\qquad Z=\sum_{i\in B}z_i,\qquad T=\bigcap_{i\in B}R_i.\)

The hypotheses give

\(\displaystyle Z\ge\frac t\alpha,\qquad s(T)\ge t,\qquad \sum_{i\in B}w_i\ge Z.\)

Suppose, for contradiction, that

\(\displaystyle u_i(A)\le t-1\quad\text{for every }i\in B.\)

Nonnegative utilities make this impossible when \(t<1\), so assume \(t\ge1\). Set \(h=1/Z\).

A common resource remains throughout the run

Since \(T\subseteq R_i\) for every \(i\in B\),

\(\displaystyle s(T\cap A)\le u_i(A)\le t-1.\)

Therefore

\(\displaystyle s(T\setminus A)\ge t-(t-1)=1.\)

Consequently, the final unallocated common resource contains either an indivisible good or a positive-length cake interval. Fix such a resource. It remains available at every earlier stage, because the allocation only grows.

In the cake case, some approval cell has a positive-length final remainder and is approved by every type in \(B\).

Budget bound at prices at most the threshold

Suppose all purchases made so far have prices at most \(h\), and let \(A'\) be the current allocation.

For a good purchase approved by type \(i\), its density payment is at most \(h\), while its utility increment is one. For an approved cake prefix of length \(q\), its payment is at most \(qh\), while its utility increment is \(q\). Summing these bounds gives

\(\displaystyle \alpha-b_i\le h\,u_i(A').\)

Since \(A'\subseteq A\), for every \(i\in B\),

\(\displaystyle b_i\ge\alpha-hu_i(A')\ge\alpha-h(t-1)\ge h.\)

The last inequality follows from \(\alpha Z\ge t\). In particular, every type in \(B\) remains active.

A candidate always has price at most the threshold

If the persistent common resource is a good \(g\), then its affordability function satisfies

\(\displaystyle F_g(h)\ge\sum_{i\in B}w_i\min\{b_i,h\}=h\sum_{i\in B}w_i\ge hZ=1.\)

Continuity, together with \(F_g(0)=0\), gives an affordable price at most \(h\).

If the persistent resource is cake, its remaining cell has active approving mass \(W\ge\sum_{i\in B}w_i\ge Z\). Section 2 therefore gives a positive affordable prefix at price

\(\displaystyle \rho_{\mathrm{cell}}=\frac1W\le\frac1Z=h.\)

Contradiction

Initially, \(\alpha\ge t/Z\ge h\), so all types in \(B\) have budget density at least \(h\). The persistent common resource consequently offers a candidate at price at most \(h\).

Inductively, whenever all preceding prices were at most \(h\), the budget bound above keeps every type in \(B\) active with budget at least \(h\). The persistent resource again offers a candidate at price at most \(h\), so the rule’s next selected price is at most \(h\).

Thus every purchase has price at most \(h\). At termination, the same budget bound and persistent resource still provide an affordable candidate. This contradicts the stopping rule.

Hence some \(i\in B\) satisfies \(u_i(A)>t-1\), proving mass-EJR-1. The proof allows arbitrary real coalition portions; it does not require rational \(z_i\).

5. Additional proven strengthening

The same rule also satisfies the mass analogue of strong EJR-1: if positive-length commonly approved cake remains unallocated, then some participating type has utility at least \(t\).

To prove this, suppose such cake remains and every \(i\in B\) has \(u_i(A)<t\). Since \(B\) is finite, let \(U=\max_{i\in B}u_i(A)<t\). Again set \(h=1/Z\).

After any sequence of purchases at prices at most \(h\),

\(\displaystyle b_i\ge\alpha-hU\ge\frac{t-U}{Z}>0\quad\text{for every }i\in B.\)

Thus the persistent common cake always has active approving mass at least \(Z\), and offers a positive prefix at price at most \(h\). Induction forces every selected price to be at most \(h\), while the displayed bound keeps all types in \(B\) active at termination. The common cake would still be affordable, a contradiction.

Together with Section 4, this proves the strengthening. Both questions in the task are therefore settled.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Assessment: proved with a minor input-encoding clarification. The price calculations, termination bound, rational bit-complexity argument, and mass-EJR-1 proof are sound. No false central step or gap requiring new mathematics was found.

The only clarification concerns the representation of the outer cake endpoint \(c\). The task does not explicitly say that \(c\) is rational, while the complexity argument implicitly treats every cake endpoint as a rational input.

1. Scope and cited result

The output addresses both assigned questions: exact polynomial-time computation of the specified deterministic allocation and its mass-EJR-1 guarantee.

The reference to the finite-society result is accurate: [Theorem 3.13 of the cited paper](https://link.springer.com/article/10.1007/s00355-024-01511-8) states that Generalized MES satisfies strong EJR-1 and can be implemented in polynomial time. The prover does not apply that theorem to the mass setting; its subsequent arguments are independent. Consequently, no unverified transfer from equally weighted agents to encoded masses occurs.

2. Exact cake candidates

Every step in the cake-price calculation is valid.

The empty approving set is correctly excluded. There is no issue concerning an unattained infimum as prefix lengths approach zero.

3. Exact good candidates

The good-price argument is correct.

Sorting the budget breakpoints and inspecting the resulting linear segments requires only polynomially many rational operations. This is an adequately specified elementary computation.

4. Termination, feasibility, and deterministic output

The charging argument establishes at most \(m+k+\tau\) purchases.

A good can be removed once, an original cell can be finished once, and a type can become exhausted once because budgets never increase. Every unfinished cell purchase exhausts a previously active type. Hence the proposed charges cannot repeat.

Every purchase decreases the weighted total budget by exactly its size, by its affordability equation. Budgets remain nonnegative because deductions are capped by the remaining budget. The identity
\(s(A)=\alpha-\sum_iw_ib_i\)
and feasibility follow.

The candidate computations implement the specified minimum-price choice and largest-prefix rule. Exact rational comparisons permit the prescribed tie-breaking.

Repeated purchases from a cell extend its selected prefix. Thus the asserted output bound of at most \(k\) cake intervals is correct, including the cake-free case \(k=0\).

5. Bit complexity

The denominator calculations are correct under the intended rational input encoding.

Minor issue — Section 3, “Bit complexity,” initial denominator \(D_0\). The proof implicitly assumes that \(c\), as an outer cake endpoint, has a rational encoding included in \(L\). The task explicitly requires rational approval endpoints and capacity but only writes \(c\ge0\).

Minimum clarification: explicitly state the intended rational encoding convention for \(c\), including its contribution to \(L\). This is an input-description clarification, not a substantive mathematical gap.

6. Mass-EJR-1

The coalition argument is valid for arbitrary real portions \(z_i\).

This establishes the strict conclusion \(u_i(A)>t-1\), including the boundary case \(t=1\). No rationality assumption on coalition portions is used.

7. Additional strengthening

Section 5 is also sound. Finiteness of \(B\) justifies a maximum \(U<t\). Its budget bound remains strictly positive, which suffices for a persistent common cake cell to offer a positive prefix. The induction and terminal contradiction are valid.

Together with Section 4, this establishes the stated strong analogue under the convention that cake sets are identified up to endpoints.

There are no blocking issues. The argument resolves both target questions under the intended rational input encoding.

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