← back to the atlas

d4-conf-ecai-2024-0156 (d4-conf-ecai-2024-0156)

Answer: Polynomial-time solvable in \(O(L)\) time. Equality holds if and only if \(|B|=1\); whenever \(|B|>1\), \(\sum_{a,b}z_{ab}\le |B|-1+\max_b\nu_b<|B|\).

The anchor (named result in the paper)

Theorem 6 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateFor any preference profile ≻ 1. isMaxProp(≻) can be checked in O(n). 2. isMaxRou(≻) can be checked in O(n).

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

The continuous mirror question, as graded

Given finite type sets \(A,B\), positive rational masses \(\mu_a,\nu_b\) with \(\sum_{a\in A}\mu_a=\sum_{b\in B}\nu_b=1\), and strict rankings of \(B\)-types by each \(A\)-type and of \(A\)-types by each \(B\)-type, run mass deferred acceptance: each unmatched \(A\)-mass proposes in ranking order, each \(B\)-type retains up to \(\nu_b\) mass according to its ranking, and rejected mass advances. Let \(z_{ab}\) be the total mass of type \(a\) that proposes to type \(b\). Decide whether \(\sum_{a\in A,b\in B} z_{ab}=|B|\), the universal upper bound when each unit of mass proposes to each \(B\)-type at most once.

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

Let \(A,B\) be disjoint, nonempty finite sets of types, with positive rational masses satisfying \(\sum_{a\in A}\mu_a=\sum_{b\in B}\nu_b=1\). Every type has a complete strict ranking of the opposite side, and all opposite-side types are acceptable.
Each society is given by its support: the list of types with positive mass, each mass encoded as a binary rational. Set \(\tau=|A|+|B|\), the total support size, not the number of possible types; let \(m=\max\{|A|,|B|\}\) and let \(L\) be the total binary input length, including the explicitly listed rankings. State running times in \(m,\tau,L\).
Mass is divisible. Initially all \(A\)-mass is unmatched. In each synchronous round, every unmatched parcel proposes to its highest-ranked \(B\)-type to which it has not previously proposed. Each \(b\) pools new proposals with previously retained mass, retains the highest-ranked mass up to capacity \(\nu_b\), and rejects the remainder, including any displaced retained mass. A boundary type may be retained partially; parcels of the same type are interchangeable. Rejected mass advances in the next round. Stop when no mass is unmatched.
Let \(z_{ab}\) be the cumulative mass of type \(a\) that proposes to \(b\), including mass subsequently rejected; each parcel contributes at most once to each \(b\).

Is deciding whether \(\sum_{a\in A,b\in B}z_{ab}=|B|\) solvable in polynomial time in \(m,\tau,L\), or is it NP-hard?

For two sides of \(n\geq 2\) individual agents with complete strict preferences, recognizing attainment of the maximum \(n^2-n+1\) DA proposals takes \(O(n)\) time with random access to ranking positions ([Gokhale et al.](https://arxiv.org/html/2310.18736v2)).
Real-valued stable allocations can be computed in strongly polynomial time ([Baïou–Balinski](https://pubsonline.informs.org/doi/pdf/10.1287/moor.27.4.662.302)); this concerns final allocations rather than the cumulative-proposal equality above. No result settling that exact equality problem was located.

Modeling choices made when packaging the task

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

Conclusion

The decision problem is polynomial-time solvable. In fact, equality holds if and only if \(|B|=1\).

This follows from a structural bound on cumulative proposals, rather than from computing a stable allocation. Writing \(q=|B|\), every instance satisfies
\(\sum_{a\in A,b\in B}z_{ab}\le q-1+\max_{b\in B}\nu_b\).
For \(q>1\), positivity and normalization imply \(\max_b\nu_b<1\), so the requested equality is impossible.

1. Retained mass and exhaustion of preference lists

Let \(h_b(t)\) denote the mass retained by receiving type \(b\) after round \(t\), with \(h_b(0)=0\). Let \(p_b(t)\) denote the new proposal mass received by \(b\) in round \(t\). The retention rule gives
\(h_b(t)=\min\{\nu_b,h_b(t-1)+p_b(t)\}\).

Consequently, \(h_b(t)\) is nondecreasing. Moreover, whenever \(b\) rejects positive mass, including displaced mass, it retains exactly \(\nu_b\). Once full, it remains full.

An unmatched parcel cannot have exhausted its preference list. Indeed, such a parcel would have been rejected by every receiving type. Each receiving type would therefore be full and remain full. Total retained mass would then be \(\sum_b\nu_b=1\), leaving no unmatched mass, a contradiction.

Thus, whenever unmatched mass remains, all of it has a valid next proposal.

2. Finite termination for rational masses

Choose a positive integer \(D\) such that every \(\mu_a\) and every \(\nu_b\) is an integer multiple of \(1/D\). For example, take the product of their denominators.

We first verify that all aggregate quantities during the process remain integer multiples of \(1/D\). Track retained mass by the pair \((a,b)\), and unmatched mass by its type and next preference-list position. These quantities initially have the asserted property. Pooling uses addition, and retaining a boundary type uses subtraction and a minimum with the remaining capacity; these operations preserve the property. Rejected quantities therefore also have the property.

This aggregation respects parcel histories: all parcels of type \(a\) proposing to a given \(b\) have proposed to exactly the same preference-list prefix. Choosing which same-type parcels to retain cannot change their future proposal destinations.

Define \(C(t)\) to be the total cumulative proposal mass through round \(t\). Since each parcel proposes to each receiving type at most once,
\(C(t)\le\sum_{a\in A}\sum_{b\in B}\mu_a=q\).

In every round that starts with unmatched mass, that mass is positive and is an integer multiple of \(1/D\). By Section 1, it all proposes. Hence \(C(t)-C(t-1)\ge 1/D\).

There can therefore be at most \(qD\) rounds, and the process terminates. This argument establishes termination only; \(D\) can be exponential in the binary input length, so it does not establish polynomial-time simulation.

3. A receiving type gets exactly its capacity in cumulative proposals

Let \(T\) be the terminating round. Immediately before that round, some positive mass is unmatched. Therefore,
\(\sum_b h_b(T-1)<1=\sum_b\nu_b\).
Since \(h_b(T-1)\le\nu_b\) for every \(b\), there is a receiving type \(b_*\) with \(h_{b_*}(T-1)<\nu_{b_*}\).

By monotonicity, \(b_*\) was under capacity after every preceding round. It consequently rejected no mass in those rounds. Its cumulative proposal mass before round \(T\) is exactly its retained mass \(h_{b_*}(T-1)\).

There are also no rejections in round \(T\). To see this explicitly, let \(U\) be the unmatched mass before that round. All of it proposes, so the total mass in the receiving types’ pools is
\(\sum_b h_b(T-1)+U=1\).
Termination means that total retained mass after processing those pools is also \(1\). The nonnegative rejected quantities must therefore sum to zero.

Finally, every receiving type is full after termination: their retained masses sum to \(1\), their capacities sum to \(1\), and no retained mass exceeds its capacity. Thus \(h_{b_*}(T)=\nu_{b_*}\).

Because \(b_*\) never rejected mass, including in the final round, we obtain the identity
\(\sum_{a\in A}z_{ab_*}=\nu_{b_*}\).

4. The strict bound and the nontrivial case

For each receiving type \(b\), the rule against repeated proposals gives
\(\sum_{a\in A}z_{ab}\le\sum_{a\in A}\mu_a=1\).

Combining this with Section 3 yields
\(\sum_{a\in A,b\in B}z_{ab}\le(q-1)+\nu_{b_*}\le q-1+\max_b\nu_b\).

If \(q>1\), every capacity is strictly less than \(1\), because all capacities are positive and sum to \(1\). Hence
\(\sum_{a,b}z_{ab}<q\).

The more interesting attainable bound is therefore below the threshold in the question. For example, it is sharp when \(|A|=|B|=n\ge2\) and all masses equal \(1/n\). Take an individual-agent instance attaining \(n^2-n+1\) proposals, whose existence is established by [Gokhale et al.](https://arxiv.org/html/2310.18736v2). Scaling each agent’s mass and each receiving capacity to \(1/n\) reproduces that execution: every proposal is retained or rejected in its entirety. Its cumulative proposal mass is \((n^2-n+1)/n=n-1+1/n\), exactly the bound above.

If \(q=1\), the unique receiving type has capacity \(1\). All mass proposes to it in the first round and is retained, giving \(\sum_{a,b}z_{ab}=1=q\).

5. Decision algorithm and running time

Count the receiving types in the explicitly supplied support. Return YES exactly when \(|B|=1\).

Scanning the input takes \(O(L)\) time. Expressed using all requested parameters, this is \(O(L+\tau+m)=O(L)\), since the explicit input length dominates the support sizes. If the support cardinality is already available as metadata, the decision itself takes \(O(1)\) time.

⟨structured verdict parsed — rendered above⟩

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

The prover’s conclusion is correct: the equality holds exactly when \(|B|=1\), and the decision problem is solvable in \(O(L)\) time. The argument establishes finite termination before using the final round, and its bound concerns cumulative proposals directly. No major or minor mathematical issues were found.

The recurrence
\[ h_b(t)=\min\{\nu_b,h_b(t-1)+p_b(t)\} \]
correctly describes total retained mass. All proposed types are acceptable, so the receiving type fills its capacity whenever its pool contains enough mass; preferences determine which mass it retains.

Since \(h_b(t-1)\leq\nu_b\) and \(p_b(t)\geq0\), the recurrence implies \(h_b(t)\geq h_b(t-1)\). Positive rejection occurs only when the pool exceeds capacity, so a receiving type that rejects positive mass is full afterward and remains full.

The contradiction is valid for positive unmatched mass that has exhausted its list. Such mass has been rejected by every receiving type. Each receiving type must consequently have become full and stayed full. Their combined retained mass would then equal \(\sum_b\nu_b=1\), contradicting the existence of positive unmatched mass.

This uses the task’s complete lists, universal acceptability, and equal total mass on the two sides. Thus every positive unmatched quantity has a valid next destination.

A common denominator \(D\) exists because there are finitely many rational masses and capacities. The stated aggregate quantities initially belong to \((1/D)\mathbb{Z}_{\geq0}\). Pooling, assigning remaining capacity to a boundary type, and computing rejections preserve that property.

The proposed aggregation also preserves the histories relevant to future proposals. For a fixed type \(a\), every parcel reaching a given receiving type has traversed the same prefix of \(a\)’s strict preference list. Previously retained parcels of that type at that receiving type have the same prefix. Interchanging those parcels therefore does not change the next destination of rejected mass.

The bound \(C(t)\leq q\) is correct: each parcel contributes its mass at most once to each of the \(q\) receiving types, and total proposer mass is \(1\). Every active round adds at least \(1/D\), because its positive unmatched mass lies on the grid and all of it proposes. Hence there are at most \(qD\) active rounds.

The prover correctly distinguishes this finite-termination argument from a polynomial-time simulation: the numerical value of \(D\) need not be polynomial in \(L\).

Initially all mass is unmatched, so the terminating round \(T\) exists and satisfies \(T\geq1\). Immediately before it, positive unmatched mass remains. Conservation of mass therefore gives
\[ \sum_b h_b(T-1)<1. \]
Since capacities sum to \(1\), at least one \(b_*\) is under capacity.

Monotonicity implies that \(b_*\) was under capacity after every earlier round. It could not have rejected positive mass in any such round, because positive rejection would have made it permanently full. Its cumulative proposal mass before round \(T\) consequently equals its retained mass.

This step is justified by the explicit mass accounting. Previously retained mass and the unmatched mass proposing in round \(T\) together have total mass \(1\). At termination, retained mass also totals \(1\). Since rejected quantities are nonnegative, their total is zero.

Every receiving type is full at termination: individual retained masses are bounded by their capacities, and both totals equal \(1\). Thus \(b_*\), which never rejected positive mass, satisfies
\[ \sum_a z_{ab_*}=\nu_{b_*}. \]

For every \(b\), the prohibition on repeated proposals gives \(\sum_a z_{ab}\leq1\). Combining these bounds with the identity for \(b_*\) yields
\[ \sum_{a,b}z_{ab}\leq q-1+\nu_{b_*} \leq q-1+\max_b\nu_b. \]
When \(q>1\), positivity of every capacity and normalization imply \(\max_b\nu_b<1\), so the requested equality is impossible.

When \(q=1\), the unique capacity is \(1\). All proposer mass is accepted in the first round, giving cumulative proposal mass \(1\). This covers arbitrary nonempty \(A\), including \(|A|=1\).

The cited existence statement is supported by [Gokhale et al., Fact 2](https://arxiv.org/html/2310.18736v2): complete strict individual preferences can attain \(n^2-n+1\) proposals. The hypotheses match the prover’s example.

With every mass and capacity equal to \(1/n\), each receiving type retains one entire proposer type whenever its pool is nonempty. Scaling therefore preserves the synchronous individual execution, and the stated cumulative mass \((n^2-n+1)/n=n-1+1/n\) is correct. This example is supplementary; the decision result does not depend on it.

Returning YES exactly when the explicitly listed receiving support has cardinality \(1\) follows from the proved characterization. Scanning the input takes \(O(L)\) time, and \(O(L+\tau+m)=O(L)\) is valid because the explicit input length dominates the support sizes. No simulation or rational arithmetic is required.

No additional clarification is needed to make the mathematical argument verifiable.

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