← back to the atlas

d4-conf-sagt-2016-0021 (d4-conf-sagt-2016-0021)

Answer: Polynomial-time solvable: every valid instance admits a stable mass assignment, including unequal \(\mu_t\), ties, and diagonal pairs.

The anchor (named result in the paper)

Theorem 12 — class: hardness

The continuous mirror question, as graded

Given a finite support \(T\), rational masses \(\mu_t\geq 0\) summing to \(1\), and symmetric compatibility with each type ranking at most three compatible partner types, decide whether there is a stable mass assignment \(q\). Require \(q_{tu}=q_{ut}\geq 0\), \(\sum_{u:\{t,u\}\text{ compatible}}q_{tu}\leq\mu_t\), and, for every compatible pair, \(B_t(u)=0\) or \(B_u(t)=0\), where \(B_t(u)=\mu_t-\sum_{v\succeq_t u}q_{tv}\). Here \(q_{tt}\) counts the mass of type-\(t\) agents used in within-type pairs, and \(B_t(u)\) is the mass unmatched or assigned below \(u\).

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\), where \(\sum_{t\in T}\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types; \(L\) is the total input bit length.
Compatibility is symmetric and may include within-type pairing. Let \(m\) count compatible unordered type pairs, including diagonal pairs. Each type weakly orders its compatible partner types, allowing ties, and lists at most three types, counting itself once if compatible. Every compatible partner is strictly preferred to being unmatched.
A mass assignment has real entries \(q_{tu}=q_{ut}\geq0\), zero on incompatible pairs, with \(\sum_{u:\{t,u\}\text{ compatible}}q_{tu}\leq\mu_t\). For distinct types, \(q_{tu}\) is the mass from each endpoint paired together; \(q_{tt}\) is the total mass of type \(t\) used in pairs of distinct agents of that type and is counted once in its capacity constraint.
Write \(v\succeq_t u\) when \(t\) weakly prefers \(v\) to \(u\), and define \(B_t(u)=\mu_t-\sum_{v:\{t,v\}\text{ compatible},\ v\succeq_t u}q_{tv}\). An assignment is stable when every compatible pair satisfies \(B_t(u)=0\) or \(B_u(t)=0\), including diagonal pairs.

Is deciding whether a stable mass assignment exists solvable in time polynomial in \(m,\tau,L\), or is it NP-hard?

For finite agents, stable roommates existence with ties and lists of length at most three is NP-complete. [Cseh–Irving–Manlove](https://arxiv.org/abs/1605.04609v3)
For unit-capacity vertices without diagonal pairs, ordinally stable fractional roommate matchings always exist, even with ties, and can be found in polynomial time. [Chen–Roy–Sorge](https://www.ijcai.org/proceedings/2021/0013.pdf)
Existence of fractional stable allocations is also known for general capacitated NTU-games, a different formulation from the support-based decision problem above. [Biró–Fleiner](https://real.mtak.hu/26264/7/BF16do_last.pdf)

Modeling choices made when packaging the task

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

Result

Deciding existence is polynomial-time solvable. In fact, every valid instance admits a stable mass assignment, including instances with unequal masses, ties, and diagonal pairs.

We prove this by applying Scarf’s lemma directly to the capacity constraints.

1. The version of Scarf’s lemma used

Let \(A,C\) be matrices with \(n\) rows and \(n+p\) columns, and let \(b\) have strictly positive coordinates. Suppose:

\[ C_{i,i}<C_{i,k}<C_{i,j}. \]

Then there exists \(x\geq 0\) with \(Ax=b\) such that, for every column \(k\), some row \(i\) satisfies
\[ C_{i,k}\leq C_{i,j} \qquad\text{for every }j\text{ with }x_j>0. \]

This is the domination formulation of Scarf’s lemma stated as Theorem 5 in [Biró–Fleiner](https://real.mtak.hu/26264/7/BF16do_last.pdf). Its hypotheses do not require distinct values among the entries \(C_{i,k}\) with \(k>n\), so ties are permitted.

2. Encoding the given instance

Let \(E\) be the set of compatible unordered pairs. If \(m=0\), the zero assignment is feasible and stability is vacuous. Hence assume \(m>0\).

Introduce one variable \(q_e\) for each \(e\in E\), and one slack variable \(s_t\) for each \(t\in T\). For incidence purposes, a diagonal pair \(\{t,t\}\) has just the endpoint \(t\). The capacity equations are therefore
\[ s_t+\sum_{\substack{e\in E\\t\in e}}q_e=\mu_t \qquad(t\in T). \]

Write these equations as \(Ax=\mu\), with the slack variables first. Thus \(A\) has \(\tau\) rows and \(\tau+m\) columns, its first \(\tau\) columns form the identity matrix, and each remaining column is the incidence vector of its compatible pair. A diagonal column has one entry equal to one, exactly as required by the problem.

For every compatible partner \(u\) of \(t\), define
\[ r_t(u)=1+\text{the number of preference classes strictly below }u. \]
Since each list contains at most three types,
\[ 1\leq r_t(u)\leq 3, \qquad v\succeq_t u\ \Longleftrightarrow\ r_t(v)\geq r_t(u). \]

Define \(C\) as follows. On a slack column \(s_u\), set
\[ C_{t,s_u}= \begin{cases} 0,&u=t,\\ 5,&u\neq t. \end{cases} \]
On a pair column \(e\), set
\[ C_{t,e}= \begin{cases} r_t(u),&e=\{t,u\}\text{ is incident with }t,\\ 4,&t\notin e. \end{cases} \]
For a diagonal pair, the first case uses \(u=t\).

We now check all hypotheses of the lemma:

Scarf’s lemma therefore supplies a nonnegative solution \(x=(s,q)\) satisfying both the capacity equations and domination.

3. Domination implies precisely the required stability

Fix any compatible pair \(e\). Choose a row \(t\) that dominates its column:
\[ C_{t,e}\leq C_{t,j} \qquad\text{whenever }x_j>0. \]

First, \(t\) must be an endpoint of \(e\). Otherwise \(C_{t,e}=4\). Since
\[ s_t+\sum_{h\ni t}q_h=\mu_t>0, \]
either \(s_t>0\), whose column has entry zero in row \(t\), or some incident \(q_h>0\), whose column has entry at most three. Either alternative contradicts domination.

Write \(e=\{t,u\}\), allowing \(u=t\). Its entry in row \(t\) is \(r_t(u)\geq 1\). Thus domination also implies \(s_t=0\): a positive \(s_t\) would require \(r_t(u)\leq 0\).

Moreover, every positive incident assignment \(q_{tv}\) satisfies
\[ r_t(u)\leq r_t(v), \]
so \(v\succeq_t u\). All mass used at \(t\) is consequently assigned to partners weakly preferred to \(u\). Together with \(s_t=0\), this gives
\[ \sum_{v:\,v\succeq_t u}q_{tv} = \sum_{v:\,\{t,v\}\text{ compatible}}q_{tv} = \mu_t. \]
Hence \(B_t(u)=0\).

Every compatible pair therefore has an endpoint satisfying the required equality. For a diagonal pair, that endpoint is necessarily \(t\), giving \(B_t(t)=0\). The resulting assignment is stable.

4. Decision complexity

Every promised input is a YES-instance. The decision algorithm therefore returns YES; reading the input takes time polynomial in \(m,\tau,L\). If input validity is also checked, exact rational arithmetic and the compatibility and preference checks take polynomial time.

This conclusion concerns the requested existence decision. It uses no polynomial running-time claim for constructing a witness with Scarf’s algorithm.

⟨structured verdict parsed — rendered above⟩

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

Verdict

The proof is correct and resolves the existence decision problem. Every valid instance admits a stable mass assignment, so the promised decision problem is polynomial-time solvable. No major or minor mathematical issues were found.

Step-by-step verification

1. The cited theorem is stated correctly

I checked Theorem 5 in [Biró–Fleiner](https://real.mtak.hu/26264/7/BF16do_last.pdf). Its matrix hypotheses and domination conclusion match the prover’s statement. In particular:

Thus unequal masses and tied preference ranks are permitted. The theorem requires positive matrix dimensions; the proof handles \(m=0\) separately, and the nonempty support guarantees \(\tau>0\).

2. The capacity encoding matches the task

For an off-diagonal pair, its single variable occurs once in each endpoint’s capacity equation. This enforces the required equality of the masses assigned from the two endpoints.

For a diagonal pair, its variable occurs once in its type’s equation. This matches the task’s explicit convention that \(q_{tt}\) counts total mass used and enters the capacity constraint once.

Adding nonnegative slack variables therefore represents precisely the stated capacity inequalities. Variables for incompatible pairs are omitted and can be understood as zero.

The feasible set is nonempty by the stated slack-only solution. It is bounded because every variable appears with coefficient one in at least one equation whose other terms are nonnegative. These checks are valid even when some types have no compatible partners.

3. The preference encoding and theorem hypotheses hold

The rank definition assigns the same value to tied partners and larger values to strictly preferred partners. Since a list contains at most three types, all incident ranks lie between \(1\) and \(3\), inclusive.

The entries in any pair column are consequently between \(1\) and \(4\). They are strictly larger than the own-slack entry \(0\) and strictly smaller than every other-slack entry \(5\), as the theorem requires.

When \(\tau=1\), there are no other-slack comparisons to check. This causes no problem: those quantified comparisons are vacuous, and the constructed own-slack and pair entries still have the required ordering.

All hypotheses needed for the application of Scarf’s lemma are satisfied.

4. The domination-to-stability argument is valid

Fix a compatible pair column and a row dominating it.

The row must correspond to an endpoint. If it did not, the pair-column entry would be \(4\). The strictly positive capacity at that row guarantees a positive own-slack variable or a positive incident pair variable. Its row entry would respectively be \(0\) or at most \(3\), contradicting domination.

The dominating endpoint has zero slack. Its pair-column entry is at least \(1\), so a positive own-slack variable, with entry \(0\), would again contradict domination.

Every positive incident assignment goes to a weakly preferred partner. Domination compares the fixed pair’s rank against every positive incident variable’s rank. The rank equivalence stated in the proof therefore gives exactly the required weak preference comparison, including ties.

The capacity equation now shows that all mass at this endpoint is assigned to partners weakly preferred to the fixed partner. Hence the relevant sum equals its mass and \(B_t(u)=0\).

This proves the required disjunction for every off-diagonal pair. For a diagonal pair, the endpoint argument forces the dominating row to be its sole endpoint, so it proves \(B_t(t)=0\) as required.

Only this implication is needed for the existence claim; no converse characterization of domination is required.

5. The decision-complexity conclusion follows

The \(m=0\) case has the stated stable zero assignment. The theorem application handles every case with \(m>0\). Thus every promised input is a YES-instance.

Returning YES settles the requested decision problem. Reading or validating the explicitly represented rational input takes polynomial time in its bit length. The proof correctly distinguishes this decision conclusion from computing a witness: it makes no unsupported claim that Scarf’s algorithm runs in polynomial time.

Repair feedback

No mathematical repair or additional clarification 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.