← back to the atlas

d4-conf-sagt-2021-0020 (d4-conf-sagt-2021-0020)

Answer: Polynomial-time solvable in \(\tau\) and \(L\); every welfare-maximizing feasible allocation is stable.

The anchor (named result in the paper)

Theorem 3 — class: hardness

The continuous mirror question, as graded

Given finite types \(T\), rational masses \(\mu_t>0\) summing to \(1\), and symmetric binary compatibilities \(a_{ts}=a_{st}\), choose \(y_S\geq 0\) for every multiset \(S\) of three types, with \(\sum_S m_t(S)y_S=\mu_t\) for each \(t\). Define \(u_t(S)=\sum_s (m_s(S)-\mathbf{1}[s=t])a_{ts}\) and \(D_t(S;y)=\sum_{R\ni t}m_t(R)y_R\mathbf{1}[u_t(S)>u_t(R)]\). Require that no \(S\) has \(D_t(S;y)>0\) for every distinct type \(t\) in \(S\). Find a stable \(y\) maximizing \(W(y)=\sum_S y_S\sum_t m_t(S)u_t(S)\), or report that no stable \(y\) exists.

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

A society is given by its support: a nonempty list \(T\) of \(\tau\) types with positive binary rational masses \(\mu_t\) summing to \(1\); \(\tau\) counts supported types, not possible types. Input also includes \(a\in\{0,1\}^{T\times T}\) with \(a_{ts}=a_{st}\); \(a_{tt}\) values a distinct partner of the same type, not oneself.
Let \(\mathcal S\) contain all unordered multisets of three types, allowing repetitions, and let \(m_t(S)\) denote multiplicity. An allocation consists of real \(y_S\geq0\) satisfying \(\sum_{S\in\mathcal S}m_t(S)y_S=\mu_t\) for every \(t\); all mass is assigned to triples.
For \(t\) occurring in \(S\), define \(u_t(S)=\sum_{s\in T}(m_s(S)-\mathbf1[s=t])a_{ts}\) and \(D_t(S;y)=\sum_{R\in\mathcal S:m_t(R)>0}m_t(R)y_R\mathbf1[u_t(S)>u_t(R)]\), where \(\mathbf1\) is the indicator.
An allocation is stable if no \(S\in\mathcal S\) satisfies \(D_t(S;y)>0\) for every distinct type occurring in \(S\). Thus blocking uses strictly improving positive submasses, including repeated types; utility ties do not block.
The computational problem is to find a stable allocation maximizing \(W(y)=\sum_{S\in\mathcal S}y_S\sum_{t:m_t(S)>0}m_t(S)u_t(S)\), or report that no stable allocation exists. Let \(L\) be the total input bit length; the room size is fixed at \(3\), and there is no separate candidate parameter \(m\).

Is this exact continuous welfare optimization problem solvable in polynomial time in \(\tau\) and \(L\), or is it \(\mathrm{NP}\)-hard?

For finite agents with symmetric binary valuations, maximizing welfare among stable matchings into triples is \(\mathrm{NP}\)-hard; a stable matching always exists and can be found in \(O(n^3)\) time, where \(n\) is the number of agents. [Source](https://eprints.gla.ac.uk/245422/2/245422.pdf)
No result settling this exact continuous optimization problem 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

The exact continuous optimization problem is polynomial-time solvable in \(\tau\) and \(L\).

In fact, every welfare-maximizing feasible allocation is stable. Thus one can discard the stability constraints and solve a single linear program. The proof depends essentially on allowing fractional allocations and repeated-type triples.

2. Edge counts and a local construction

For a triple multiset \(R=\{r_1,r_2,r_3\}\), define its valued-edge count by
\(e(R)=a_{r_1r_2}+a_{r_1r_3}+a_{r_2r_3}\).
The three positions represent distinct individuals, even when their types coincide. Symmetry gives
\(\sum_{t:m_t(R)>0}m_t(R)u_t(R)=2e(R)\).
Consequently, \(W(y)=2F(y)\), where
\(F(y)=\sum_R e(R)y_R\).

We first construct an auxiliary nonnegative triple vector \(z(P)\) for any pair multiset \(P=\{p,q\}\). It consumes exactly the type masses specified by \(P\), namely one unit of each endpoint if they differ and two units of their common type otherwise.

If \(p\ne q\), set
\(z(P)_{\{p,p,q\}}=z(P)_{\{p,q,q\}}=\frac13\),
with all other coordinates zero. Indeed, each endpoint’s consumed mass is \(\frac23+\frac13=1\). Its valued-edge total is
\(g(P):=\sum_R e(R)z(P)_R=\frac{4a_{pq}+a_{pp}+a_{qq}}3\).

If \(p=q\), set
\(z(P)_{\{p,p,p\}}=\frac23\).
This consumes two units of type \(p\), and \(g(P)=2a_{pp}\).

Writing \(b(P)=a_{pq}\), both cases give
\(g(P)\ge b(P)\).
Moreover, if \(b(P)=1\), then
\(g(P)-b(P)\ge\frac13\).

Thus two retained partners can be reassigned without losing their valued edge, and with a strict gain when that edge is valued.

3. Welfare maximizers contain no one-edge triples

Let \(y\) maximize welfare over all feasible allocations. Suppose \(y_R>0\) for a triple \(R\) with \(e(R)=1\).

Choose the endpoints of its unique valued edge as a pair multiset \(P\), and denote the remaining type by \(r\). For any \(0<\delta\le y_R\), remove \(\delta\) units of \(R\), add the triple vector \(\delta z(P)\), and add \(\frac{\delta}{3}\) units of \(\{r,r,r\}\).

This preserves every type’s mass: \(\delta z(P)\) consumes precisely the two endpoint masses, and the pure triple consumes precisely the remaining mass. All coordinates remain nonnegative.

Since \(b(P)=1\), the change in \(F\) is
\(\delta\bigl(g(P)+a_{rr}-1\bigr)\ge\frac{\delta}{3}>0\).
This contradicts welfare optimality.

Therefore
\(y_R>0\ \Longrightarrow\ e(R)\ne1\).

4. Every welfare maximizer is stable

Fix a welfare-maximizing feasible allocation \(y\). Suppose, for contradiction, that a triple multiset \(S=\{t_1,t_2,t_3\}\) blocks it.

For every distinct type \(t\) in \(S\), the condition \(D_t(S;y)>0\) implies that some triple \(R\) satisfies
\(y_R>0\), \(m_t(R)>0\), and \(u_t(R)<u_t(S)\).
This follows directly because the defining sum for \(D_t\) has finitely many nonnegative terms.

For each position \(i\), choose such a source triple \(R_i\) for type \(t_i\), and distinguish one occurrence of \(t_i\) in \(R_i\). Sources may coincide, including when \(S\) repeats a type. Let
\(k_i=u_{t_i}(R_i)\),
and let \(P_i\) be the pair remaining after deleting the distinguished occurrence. Put \(b_i=b(P_i)\). Counting edges incident to the distinguished position gives
\(e(R_i)=k_i+b_i\).

Choose \(\delta>0\) sufficiently small that all three source copies can be removed simultaneously. Explicitly, if a triple \(R\) occurs \(c_R\) times among the sources, take
\(\delta\le\min_{R:c_R>0} y_R/c_R\).

Now remove \(\delta\) units of each source copy, add \(\delta\) units of \(S\), and add \(\delta z(P_i)\) for each \(i\). This produces a nonnegative allocation \(y'\).

It is feasible because the removed distinguished occurrences have exactly the multiset of types \(S\), while each \(z(P_i)\) restores the corresponding remaining pair. Its change in valued-edge total is
\(F(y')-F(y)=\delta\left(e(S)-\sum_{i=1}^3k_i+\sum_{i=1}^3\bigl(g(P_i)-b_i\bigr)\right)\).

We show that this quantity is strictly positive.

The three positions of \(S\), with edges given by their binary valuations, form a simple graph on three positions. A blocking triple cannot have an isolated position: that position would have utility zero, which cannot strictly exceed its nonnegative current utility. Hence only the following two cases are possible.

\(F(y')-F(y)\ge\delta(2-1)>0\).

\(F(y')-F(y)\ge\delta\left(3-\sum_i k_i\right)>0\).
Otherwise all \(k_i=1\). Since \(y_{R_i}>0\), Section 3 excludes \(e(R_i)=1\). The identity \(e(R_i)=1+b_i\), together with \(b_i\in\{0,1\}\), therefore forces every \(b_i=1\). Consequently,
\(F(y')-F(y)\ge\delta\sum_{i=1}^3\frac13=\delta>0\).

Both cases contradict welfare optimality. Thus \(y\) is stable.

This argument includes all repeated-type cases: it operates on distinguished positions, allows coinciding source triples, and preserves type multiplicities exactly.

5. Exact polynomial-time algorithm

Enumerate the \(\binom{\tau+2}{3}\) triple multisets and solve the rational linear program with objective
\(\max_y\sum_{S\in\mathcal S}2e(S)y_S\),
subject to
\(\sum_{S\in\mathcal S}m_t(S)y_S=\mu_t\) for every \(t\in T\), and \(y_S\ge0\) for every \(S\).

The required hypotheses for rational linear programming are satisfied:

The standard polynomial-time theorem for rational linear programming therefore provides an exact rational optimum in polynomial time. By Section 4, every returned optimum is stable. Since it maximizes welfare over all feasible allocations, it also maximizes welfare among stable allocations. A stable allocation always exists, so the “no stable allocation” outcome is never needed.

The [finite-agent hardness result](https://eprints.gla.ac.uk/245422/2/245422.pdf) does not transfer to this model. Here the fractional replacement of a pair by repeated-type triples is feasible and is precisely what makes the improvement argument work.

⟨structured verdict parsed — rendered above⟩

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

Verification report

The proof is correct and resolves the assigned continuous optimization problem. The local replacements preserve type masses, strictly improve welfare in every alleged blocking case, and remain valid with repeated types and coinciding sources. The resulting rational linear program has polynomial encoding length and yields an exact optimal stable allocation.

No major or minor mathematical issues were found.

1. Welfare and valued-edge counts

The definition of \(e(R)\) correctly counts the three unordered pairs of distinct positions. Repeated types do not create self-interactions: the positions still represent distinct individuals, as required by the task.

The identity \(\sum_{t:m_t(R)>0}m_t(R)u_t(R)=2e(R)\) is valid. Symmetry ensures that each valued edge contributes once to each endpoint’s utility, including edges between individuals of the same type. Therefore \(W(y)=2F(y)\), and maximizing either objective is equivalent.

2. Auxiliary replacement of a pair

For \(p\ne q\), the two specified triples consume exactly one unit of each endpoint type. Their edge counts are \(a_{pp}+2a_{pq}\) and \(2a_{pq}+a_{qq}\), so the stated formula \(g(P)=(4a_{pq}+a_{pp}+a_{qq})/3\) is correct.

For \(p=q\), assigning \(2/3\) units to the pure triple consumes two units of type \(p\). Its edge contribution is \(g(P)=2a_{pp}\), also correctly calculated.

Both claimed inequalities hold:

The construction is an auxiliary mass vector, so it need not itself satisfy the original society’s mass constraints. Its subsequent use as a replacement is legitimate.

3. Exclusion of positive one-edge triples

The replacement of \(\delta\) units of \(R\) preserves all type masses. This remains true when the remaining type \(r\) coincides with an endpoint type: the argument accounts for multiplicities, and contributions to coinciding coordinates are added.

Choosing \(0<\delta\le y_R\) guarantees nonnegativity after removal. All added quantities are nonnegative.

The pure triple contributes \((\delta/3)e(\{r,r,r\})=\delta a_{rr}\). Thus the stated objective change \(\delta(g(P)+a_{rr}-1)\) is correct and is at least \(\delta/3>0\).

Consequently, the conclusion that a welfare maximizer cannot assign positive mass to a triple with exactly one valued edge is established.

4. Extraction and simultaneous removal of sources

For each blocking type, the defining sum for \(D_t(S;y)\) is finite and nonnegative. A positive sum therefore supplies a source triple with positive allocation and strictly smaller utility. This implication is justified.

Selecting a source separately for each position of \(S\) is valid even when types repeat. The same source may be selected multiple times because sufficiently small fractions can be removed separately.

The stated condition \(\delta\le\min_{R:c_R>0}y_R/c_R\) handles all coinciding sources. Every numerator in this minimum is positive, so a positive \(\delta\) exists, and aggregate removal from each source does not exceed its allocated mass.

The identity \(e(R_i)=k_i+b_i\) correctly partitions source edges into those incident to the distinguished occurrence and the edge between the remaining two positions.

5. Feasibility and objective change

The removed distinguished occurrences have precisely the type multiplicities of \(S\). Adding \(\delta\) units of \(S\) restores their masses, while each \(\delta z(P_i)\) restores the remaining pair’s masses.

This reasoning covers repeated types, overlapping source triples, and overlapping added coordinates. Together with the removal bound, it establishes feasibility and nonnegativity of \(y'\).

The displayed expression
\(F(y')-F(y)=\delta(e(S)-\sum_{i=1}^3k_i+\sum_{i=1}^3(g(P_i)-b_i))\)
correctly accounts for every removal and addition.

6. Exhaustion of blocking cases

An isolated position in \(S\) has utility zero. Since all source utilities are nonnegative, that position cannot strictly improve. Thus a blocking triple has no isolated position.

A simple graph on three positions without an isolated position has either two or three edges. Repeated types do not invalidate this classification: edges are between distinct positions, and equal-type positions have the same utility prescribed by the task.

Two edges. The target utilities are \(2,1,1\). Strict improvement and integral source utilities imply corresponding bounds \(1,0,0\). Hence \(\sum_i k_i\le1\). Since every replacement surplus is nonnegative, the stated gain of at least \(\delta(2-1)>0\) follows.

Three edges. Every target utility equals \(2\), so each \(k_i\le1\). If their sum is below \(3\), the objective change is strictly positive as stated.

Otherwise, all three source utilities equal \(1\). Section 3 applies because every selected source has positive allocation. Combining its exclusion of one-edge triples with \(e(R_i)=1+b_i\) forces \(b_i=1\). Each pair replacement then contributes surplus at least \(1/3\), giving the claimed total gain of at least \(\delta>0\).

The cases are exhaustive. Every alleged block contradicts optimality, establishing that every feasible welfare maximizer is stable.

7. Exact polynomial-time optimization

The number of triple multisets is correctly given by \(\binom{\tau+2}{3}\). Enumerating them and computing their multiplicities and objective coefficients takes polynomial time.

The pure-triple allocation proves feasibility. Summing the mass equations gives \(3\sum_S y_S=1\); together with nonnegativity, this bounds every coordinate. The feasible set is closed, so a maximum exists.

The coefficient ranges and constraint count are correct. Including nonnegativity constraints still leaves polynomially many constraints. The rational masses retain their input encoding, and the full explicit LP has polynomial binary encoding length in \(\tau\) and \(L\).

The rational linear-programming theorem is used in its applicable form: a rational LP with polynomial encoding length can be solved exactly in polynomial time, returning a rational optimal solution when feasible and bounded. Both hypotheses are verified here.

Every returned optimum is stable by the established argument. Because it maximizes welfare over the entire feasible set, it also maximizes welfare over stable allocations. Feasibility and existence of an optimum additionally establish that a stable allocation always exists.

The finite-agent hardness result is not used as a premise. The proof supplies its own continuous-model classification.

Required clarification

None. The argument establishes the claimed polynomial-time solution under the task’s stated definitions.

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