← back to the atlas

d4-conf-wine-2020-0039 (d4-conf-wine-2020-0039)

Answer: \(\mathsf{P}\): every valid instance admits a stable assignment.

The anchor (named result in the paper)

Theorem 3.8 — class: hardness

The continuous mirror question, as graded

Given a finite type set \(T\), rational masses \(\mu_t>0\) summing to \(1\), and a strict master order over multisets of two types that induces each type’s ranking, decide whether there are \(\lambda_r\ge 0\), one for each multiset \(r\) of three types, such that \(\sum_r \nu_t(r)\lambda_r=\mu_t\) for every \(t\in T\) and no triple multiset \(q\) has \(B_{t,q}(\lambda)>0\) for every type \(t\) occurring in \(q\). Here \(\nu_t(r)\) is the number of copies of \(t\) in \(r\), and \(B_{t,q}(\lambda)\) is the mass of type-\(t\) residents assigned to pairs of co-resident types ranked below \(q\setminus\{t\}\).

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\). Here \(\tau\) is the support size, not the number of possible types. Let \(m=3\) be the fixed room size and \(L\) the total input bit length; state running times in \(m,\tau,L\).
Let \(\mathcal M_k(T)\) denote all multisets of \(k\) types, allowing repetitions. The input explicitly lists a strict total master order \(\succ\) on \(\mathcal M_2(T)\); every type uses this order and accepts every pair, including pairs containing its own type. Residents are nonatomic, and distinct residents may have the same type.
An assignment consists of real room masses \(\lambda_r\geq0\), for \(r\in\mathcal M_3(T)\), satisfying \(\sum_{r\in\mathcal M_3(T)}\nu_t(r)\lambda_r=\mu_t\) for every \(t\in T\), where \(\nu_t(r)\) counts occurrences of \(t\). Thus all resident mass is assigned.
For \(q\in\mathcal M_3(T)\) and \(t\) occurring in \(q\), define \(B_{t,q}(\lambda)=\sum_{r:\nu_t(r)>0,\ q\setminus\{t\}\succ r\setminus\{t\}}\nu_t(r)\lambda_r\), where multiset subtraction removes one occurrence.
The multiset \(q\) blocks precisely when \(B_{t,q}(\lambda)>0\) for every type occurring in \(q\), including when a type occurs repeatedly. An assignment is stable if no multiset blocks.

Is deciding whether such a stable assignment exists in \(\mathsf P\), or is it \(\mathsf{NP}\)-hard?

For finite agents with complete strict preferences induced by a common master order of pairs of distinct agents, stable triple-matching existence is \(\mathsf{NP}\)-complete. [Bredereck, Heeger, Knop, and Niedermeier](https://arxiv.org/pdf/2009.14191)
No result settling this exact nonatomic mass model was located in the literature search.

Modeling choices made when packaging the task

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

Resolution

The decision problem is in \(\mathsf P\): every valid input admits a stable assignment. This follows from Scarf’s lemma applied to the matrix of type multiplicities. The homogeneous rooms force the resulting fractional allocation to assign every type’s full mass.

1. The existence theorem used

We use the following matrix form of Scarf’s lemma, stated as Lemma 1 in [Biró, Csáji, and Schlotter, *Stable Hypergraph Matching in Unimodular Hypergraphs*](https://drops.dagstuhl.de/storage/00lipics/lipics-vol334-icalp2025/html/LIPIcs.ICALP.2025.31/LIPIcs.ICALP.2025.31.html).

Let \(A\) be a finite nonnegative matrix with no zero column, and let \(b\) be a positive vector. For each row \(i\), suppose there is a strict order \(\succ_i\) on the columns \(j\) satisfying \(A_{ij}>0\). Then there exists an extreme point \(x\) of

\(\displaystyle P=\{x:x\geq 0,\ Ax\leq b\}\)

such that every column \(j\) is dominated in some row \(i\), meaning:

Here \(\succeq_i\) allows equality. Crucially, the matrix entries need not be binary.

2. Applying the theorem to room masses

Index the rows by \(T\) and the columns by \(\mathcal M_3(T)\). Define

\(\displaystyle A_{t,r}=\nu_t(r),\qquad b_t=\mu_t.\)

For each type \(t\), order the columns containing \(t\) by

\(\displaystyle r\succ_t s\quad\Longleftrightarrow\quad r\setminus\{t\}\succ s\setminus\{t\}.\)

We check the hypotheses explicitly.

Scarf’s lemma therefore supplies a nonnegative vector \(\lambda\) satisfying \(A\lambda\leq\mu\) and dominating every room column.

Full assignment of every type

Fix \(t\in T\), and consider the homogeneous room \(h_t=\{t,t,t\}\).

Its column has exactly one nonzero entry, namely \(A_{t,h_t}=3\). Consequently, the only row in which this column can be dominated is row \(t\). The saturation condition in Scarf’s lemma gives

\(\displaystyle (A\lambda)_t=\mu_t.\)

Since this holds for every type,

\(\displaystyle \sum_{r\in\mathcal M_3(T)}\nu_t(r)\lambda_r=\mu_t\qquad\text{for every }t\in T.\)

Thus \(\lambda\) is an assignment in the exact sense required by the question.

3. Verifying the exact blocking condition

Fix any proposed room \(q\in\mathcal M_3(T)\). Because its column is dominated, there is some type \(t\) occurring in \(q\) such that every room \(r\) satisfying \(\nu_t(r)\lambda_r>0\) obeys

\(\displaystyle r\succeq_t q.\)

By the definition of the row order, this means that \(r\setminus\{t\}\) is equal to, or preferred to, \(q\setminus\{t\}\) in the master order. In particular, no such positive-mass room satisfies

\(\displaystyle q\setminus\{t\}\succ r\setminus\{t\}.\)

Every summand in the defining expression for \(B_{t,q}(\lambda)\) is therefore zero, so

\(\displaystyle B_{t,q}(\lambda)=0.\)

The proposed room \(q\) can block only if this quantity is positive for every type occurring in \(q\). The type \(t\) just identified prevents that. Since \(q\) was arbitrary, the assignment is stable.

This argument covers repeated types directly: the matrix uses their actual multiplicities, and blocking is excluded by precisely the condition specified in the task.

4. Complexity and the finite-agent distinction

On inputs satisfying the stated promises, the decision algorithm simply returns YES. Its running time is \(O(1)\), or \(O(L)\) if the input is read first. These bounds are independent of \(\tau\), with room size fixed at \(m=3\). No enumeration of the \(\binom{\tau+m-1}{m}\) possible rooms is needed for decision.

The proof also guarantees a rational stable assignment supported on at most \(\tau\) room multisets. To see this, take the extreme point supplied by Scarf’s lemma. If its positive-support columns were linearly dependent, a nonzero vector supported on those columns and lying in the kernel of \(A\) would permit sufficiently small perturbations in both directions while preserving feasibility, contradicting extremality. Hence those columns are independent, so there are at most \(\tau\). Their coordinates solve an invertible rational subsystem of \(A\lambda=\mu\), and are therefore rational.

The finite-agent hardness result does not contradict this conclusion: Scarf’s lemma supplies fractional room masses, whereas a finite matching requires indivisible groups of agents. The proof above establishes existence in the given nonatomic model; it does not assert a polynomial-time algorithm for constructing the assignment.

⟨structured verdict parsed — rendered above⟩

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

The prover’s argument is correct and resolves the decision problem: every valid input admits a stable assignment. I found no major or minor mathematical issues.

1. The cited existence theorem

The stated matrix form of Scarf’s lemma matches Lemma 1 of the [cited paper](https://drops.dagstuhl.de/storage/00lipics/lipics-vol334-icalp2025/html/LIPIcs.ICALP.2025.31/LIPIcs.ICALP.2025.31.html). In particular, that lemma permits arbitrary nonnegative matrix entries, requires every column to have a nonzero entry, and provides an extreme point dominating every column in some row. Its definition of domination includes both row saturation and weak preference over the dominated column for every positively used incident column.

The source permits nonnegative capacities; the prover states the theorem under the stronger assumption of positive capacities. This restriction is valid and matches the task.

Thus the application does not improperly extend a theorem for binary incidence matrices to multiplicity matrices. No integrality or total unimodularity hypothesis is required.

Assessment: Correct theorem statement and verified citation.

2. Matrix construction and hypotheses

The construction \(A_{t,r}=\nu_t(r)\), \(b_t=\mu_t\) faithfully represents the task’s resource constraints.

Every listed hypothesis is satisfied:

Consequently, the strict total master order induces a strict total order on the columns incident to each row. Repeated occurrences of \(t\) cause no ambiguity: multiset subtraction removes one occurrence, regardless of which indistinguishable occurrence is selected.

Scarf’s lemma therefore applies exactly as written.

Assessment: Correct, with all necessary hypotheses checked.

3. Full assignment

For each type \(t\), the homogeneous room \(h_t=\{t,t,t\}\) is among the permitted columns. Its only positive entry is in row \(t\).

Scarf’s domination condition requires a positive entry in the dominating row. Therefore \(h_t\) must be dominated in row \(t\), and domination forces \((A\lambda)_t=\mu_t\).

The quantifier is correct: applying this reasoning separately to every type establishes every required equality for the same vector \(\lambda\) supplied by the theorem. There is no assumption that the homogeneous rooms themselves receive positive mass.

This step legitimately strengthens the theorem’s capacity inequalities to the exact assignment equalities required by the task.

Assessment: Correct and sufficient.

4. Exact blocking condition

For an arbitrary room \(q\), column domination supplies a type \(t\) occurring in \(q\) such that every room \(r\) with \(\nu_t(r)\lambda_r>0\) satisfies \(r\succeq_t q\).

By the definition of the induced row order, such a room cannot satisfy \(q\setminus\{t\}\succ r\setminus\{t\}\). Hence every term included in the defining sum for \(B_{t,q}(\lambda)\) has zero mass contribution, and \(B_{t,q}(\lambda)=0\).

This is precisely enough to exclude blocking: the task requires strict positivity for every type occurring in \(q\), and the identified type fails that requirement.

The reasoning also handles:

There is no substitution of an integral matching notion for the task’s specified nonatomic blocking condition.

Assessment: Correct, including repetitions and strictness.

5. Complexity claim

Universal existence makes the decision algorithm “return YES” correct on all inputs satisfying the promises.

The stated bounds are appropriate: \(O(1)\) without reading the promised input, or \(O(L)\) if it is read first, with \(m=3\) fixed and no additional dependence on \(\tau\). The latter is a reading bound, not a claim about validating malformed inputs.

The proof does not need an efficient construction of the Scarf point to establish polynomial-time decidability. The output explicitly distinguishes existence decision from construction.

Assessment: Correct resolution of the assigned complexity question.

6. Rationality and support bound

The additional claim about a rational stable assignment supported on at most \(\tau\) rooms is also justified.

If the positive-support columns were dependent, a nonzero kernel vector supported on them would preserve \(A\lambda\) under perturbation. Because the support is finite and all its coordinates are positive, sufficiently small perturbations in both directions preserve nonnegativity. This contradicts extremality.

Thus the support columns are independent and their number is at most \(\tau\). Their full column rank guarantees an invertible square subsystem using the support columns and a corresponding selection of rows. Since its coefficients and right-hand side are rational, the supported coordinates are rational.

This is a valid ancillary result; it is not needed for the decision algorithm.

Assessment: Correct.

7. Final adjudication and feedback

The finite-agent distinction is consistent with the proof: fractional room masses need not correspond to indivisible finite matchings. The output makes no unsupported construction-time claim.

Every nontrivial step survives verification. No 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.