← back to the atlas

d4-journals-mss-2022-0037 (d4-journals-mss-2022-0037)

Answer: No polynomial total-time algorithm exists for the requested explicit output: some instances require at least \(2^{m/7}=2^{\tau/6}\) polyhedra.

The anchor (named result in the paper)

Theorem 2 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateFor a market (F, W, P), the algorithm computes the full set of stable matchings S(P). The following example illustrates the algorithm. Example 1 (Continued) We apply the algorithm to the market of Example 1.

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

The continuous mirror question, as graded

Given finite sets of worker types \(A\) and employer types \(B\), rational masses \(\mu_a,\nu_b\), and strict rankings of acceptable opposite-side types, compute an exact finite union of rational polyhedra describing all stable mass matrices \(x\). Each matrix must satisfy \(x_{ab}\ge 0\), \(\sum_b x_{ab}\le\mu_a\), and \(\sum_a x_{ab}\le\nu_b\); for every mutually acceptable pair, stability requires \(r_{ab}(x)s_{ab}(x)=0\), where \(r_{ab}(x)\) and \(s_{ab}(x)\) are the masses on each side unmatched or matched to a less-preferred type.

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

Let \(A\) and \(B\) be disjoint finite sets of worker and employer types. A society is given by its support: its \(\tau=|A|+|B|\) types with positive masses \(\mu_a,\nu_b\), each encoded as a binary rational; \(\tau\) counts supported types, not possible types. Masses need not sum to one, and the two sides may have different total masses. Each type strictly ranks its acceptable opposite-side types above being unmatched.
Let \(E\subseteq A\times B\) be the mutually acceptable pairs, \(m=|E|\), and \(L\) the total input bit length. Write \(E_a=\{b:(a,b)\in E\}\) and \(E_b=\{a:(a,b)\in E\}\).
A feasible mass matrix \(x\in\mathbb R^{A\times B}\) satisfies \(x_{ab}\geq0\), \(x_{ab}=0\) outside \(E\), \(\sum_bx_{ab}\leq\mu_a\), and \(\sum_ax_{ab}\leq\nu_b\). Mass is divisible, with no additional pair capacities.
For \((a,b)\in E\), define \(r_{ab}(x)=\mu_a-\sum_cx_{ac}+\sum_{c\in E_a:\,b\succ_a c}x_{ac}\) and \(s_{ab}(x)=\nu_b-\sum_dx_{db}+\sum_{d\in E_b:\,a\succ_b d}x_{db}\). A feasible matrix is stable exactly when \(r_{ab}(x)s_{ab}(x)=0\) for every \((a,b)\in E\).
The computational problem is to produce an explicit finite union of rational polyhedra in the matrix coordinates whose union is exactly the set of stable matrices; each polyhedron is specified by rational linear inequalities.

Can this exact union be computed in time polynomial in \(m,\tau,L\), or is this computation NP-hard?

For discrete many-to-many markets with substitutable preferences satisfying the law of aggregate demand, a finite cycle algorithm enumerates every stable matching ([Bonifacio et al.](https://arxiv.org/abs/2110.11846)).
For continuous stable allocation with strict preferences and real quotas and pair capacities, strongly polynomial algorithms find one stable allocation ([Baïou–Balinski](https://pubsonline.informs.org/doi/10.1287/moor.27.3.485.310)); a polynomially constructible rotation representation describes all stable allocations, using a different output representation ([Dean–Munshi](https://people.computing.clemson.edu/~bcdean/stable_alloc.pdf)).

Modeling choices made when packaging the task

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

Conclusion

The requested explicit union cannot always be computed in time polynomial in \(m,\tau,L\). There are instances with \(m=7k\), \(\tau=6k\), and polynomial input length for which every exact union requires at least \(2^k\) polyhedra.

This is an unconditional output-size obstruction. It does not depend on any assumption about \(\mathrm P\) versus \(\mathrm{NP}\). Thus “polynomial-time or NP-hard” is not an exhaustive dichotomy for this explicit-output problem; the result below establishes impossibility of polynomial total running time without claiming reduction-based NP-hardness.

1. An exact finite union always exists

Let \(F\) denote the feasible polyhedron specified in the question. For every \(x\in F\), both \(r_{ab}(x)\) and \(s_{ab}(x)\) are nonnegative: each is unmatched mass plus mass assigned to less-preferred partners.

Consequently, stability is equivalent to requiring, for every \((a,b)\in E\), the disjunction
\(r_{ab}(x)=0\) or \(s_{ab}(x)=0\).

For each function \(\sigma:E\to\{A,B\}\), define the rational polyhedron

\(P_\sigma=\{x\in F:r_{ab}(x)=0\text{ when }\sigma(a,b)=A,\ s_{ab}(x)=0\text{ when }\sigma(a,b)=B\}\).

Every equality can be written as two rational linear inequalities. The stable set is exactly \(\bigcup_\sigma P_\sigma\): every member of this union satisfies all stability products, and every stable matrix supplies at least one valid choice for each pair.

This gives a direct construction using at most \(2^m\) polyhedra. We next show that exponentially many polyhedra can be necessary under any construction.

2. A six-type example

Take workers \(a_1,a_2,a_3\) and employers \(b_1,b_2,b_3\), all with mass \(1\). Their complete acceptable lists, from best to worst, are:

| Worker | Preference list | Employer | Preference list |
|---|---|---|---|
| \(a_1\) | \(b_1\succ b_2\) | \(b_1\) | \(a_3\succ a_2\succ a_1\) |
| \(a_2\) | \(b_2\succ b_1\succ b_3\) | \(b_2\) | \(a_1\succ a_2\) |
| \(a_3\) | \(b_3\succ b_1\) | \(b_3\) | \(a_2\succ a_3\) |

These lists specify seven mutually acceptable pairs.

Every stable matrix fills every type’s mass

Each worker’s worst acceptable employer ranks that worker first: these pairs are \((a_1,b_2)\), \((a_2,b_3)\), and \((a_3,b_1)\).

Suppose a worker \(a\) has positive unmatched mass, and let \(b\) be that worker’s worst acceptable employer. Then

\(r_{ab}(x)=1-\sum_c x_{ac}>0\).

Because \(b\) ranks \(a\) first,

\(s_{ab}(x)=1-x_{ab}>0\),

where the strict inequality follows from \(x_{ab}\leq\sum_c x_{ac}<1\). This contradicts stability.

Therefore every worker has row sum \(1\). The total assigned mass is consequently \(3\). Each of the three employer columns has sum at most \(1\), so every column must also have sum \(1\).

Parameterizing every stable candidate

Write \(\alpha=x_{a_1b_1}\) and \(\beta=x_{a_3b_1}\). The row and column equations force the matrix, with workers indexing rows, to be

\(x(\alpha,\beta)=\begin{pmatrix} \alpha&1-\alpha&0\\ 1-\alpha-\beta&\alpha&\beta\\ \beta&0&1-\beta \end{pmatrix}\).

Nonnegativity is equivalent to \(\alpha\geq0\), \(\beta\geq0\), and \(\alpha+\beta\leq1\).

For the pair \((a_2,b_1)\), the only worse employer for \(a_2\) is \(b_3\), and the only worse worker for \(b_1\) is \(a_1\). Since both sides are fully assigned,

\(r_{a_2b_1}(x)=\beta,\qquad s_{a_2b_1}(x)=\alpha\).

Its stability condition is therefore \(\alpha\beta=0\).

All six other pairs automatically satisfy stability:

Thus the stable set is exactly two rational line segments:

\(S=\{x(\alpha,0):0\leq\alpha\leq1\}\ \cup\ \{x(0,\beta):0\leq\beta\leq1\}\).

In matrix coordinates, these segments can be specified by nonnegativity, zero entries outside the acceptable pairs, all row and column sums equal to \(1\), and respectively \(x_{a_3b_1}=0\) or \(x_{a_1b_1}=0\).

Two stable points cannot share one convex piece

Let \(U=x(1,0)\) and \(V=x(0,1)\). Both are stable. Their midpoint is \(x(\tfrac12,\tfrac12)\), at which

\(r_{a_2b_1}(x)s_{a_2b_1}(x)=\tfrac14>0\).

Hence no convex subset of the stable set can contain both \(U\) and \(V\).

3. Exponentially many polyhedra are necessary

Take \(k\) disjoint copies of this example, with no acceptable pairs between copies. All \(6k\) types have positive unit masses, so

\(\tau=6k,\qquad m=7k\).

The stable set is the Cartesian product \(S^k\), with all coordinates between copies fixed to zero. Indeed, feasibility and every stability condition involve only one copy.

For each word \(\varepsilon\in\{U,V\}^k\), let \(X^\varepsilon\) use the indicated endpoint in each copy. These are \(2^k\) distinct stable matrices.

If \(\varepsilon\neq\delta\), the words differ in some copy. In that copy, the midpoint of \(X^\varepsilon\) and \(X^\delta\) restricts to \(x(\tfrac12,\tfrac12)\), which is unstable. Therefore their global midpoint is unstable.

Now consider any exact representation

\(S^k=P_1\cup\cdots\cup P_N\),

where each \(P_i\) is a rational polyhedron in the matrix coordinates. Exactness implies \(P_i\subseteq S^k\) for every \(i\). Since each polyhedron is convex, none can contain two distinct matrices \(X^\varepsilon\): otherwise it would contain their unstable midpoint.

Covering all \(2^k\) matrices consequently requires

\(N\geq2^k=2^{m/7}=2^{\tau/6}\).

This lower bound is sharp for these instances: choosing one of the two local segments in every copy gives an exact union of \(2^k\) rational polyhedra.

4. Computational consequence

The constructed instances have constant-size preference lists and unit masses. With binary type identifiers, their input length is \(L=O(k\log(k+1))\). Even a dense encoding has polynomial length in \(k\).

Every permitted output nevertheless contains at least \(2^k\) explicitly listed polyhedra. Merely writing that output requires exponential time. Therefore a running time polynomial in \(m,\tau,L\) is impossible.

This does not conflict with finding one stable allocation efficiently or representing all allocations compactly. In particular, [Dean–Munshi’s rotation representation](https://people.computing.clemson.edu/~bcdean/stable_alloc.pdf), described in Lemma 12, uses rotation variables with precedence conditions. It is a different output representation from an explicit list of polyhedra in the original matrix coordinates.

⟨structured verdict parsed — rendered above⟩

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

The argument is correct and resolves the polynomial total-time question for the required explicit output. It proves an unconditional exponential lower bound on the number of polyhedra. It does not establish reduction-based NP-hardness, and explicitly disclaims that claim. No mathematical gaps or false steps were found.

On the feasible polyhedron \(F\), unmatched masses and all matrix entries are nonnegative. Thus every \(r_{ab}(x)\) and \(s_{ab}(x)\) is nonnegative. The condition \(r_{ab}(x)s_{ab}(x)=0\) is exactly the stated disjunction.

Each choice function \(\sigma\) imposes rational affine equalities alongside the rational inequalities defining \(F\), so \(P_\sigma\) is a rational polyhedron in the required matrix coordinates. Both inclusions in the asserted union follow directly: every chosen piece satisfies every product condition, and every stable matrix admits a choice of a zero factor for each pair.

Empty pieces and pairs for which both factors vanish cause no difficulty. If \(E\) is empty, the single empty choice function gives \(F\), as required.

The preference lists agree on mutual acceptability and specify exactly seven pairs. There are six supported types, all with positive binary-rational unit masses. Every acceptable partner is ranked strictly, and no additional pair capacities are introduced.

For each worker, its worst acceptable employer ranks that worker first, exactly as asserted.

If worker \(a\) has positive unmatched mass, its worst acceptable employer \(b\) has no partners below it on \(a\)'s list. Therefore
\(r_{ab}(x)=1-\sum_c x_{ac}>0\).

Since \(b\) ranks \(a\) first, the unmatched mass and all assignments to other workers combine to give
\(s_{ab}(x)=1-x_{ab}>0\).
The strict inequality follows from the displayed row bound. This contradicts stability.

Consequently all three worker rows sum to one. Their total assigned mass is three, and three employer columns bounded above by one must each sum to one. This argument uses only the gadget’s equal unit masses; it does not impose any unstated restriction on general inputs.

The row and column equations force every feasible fully assigned matrix into the displayed form \(x(\alpha,\beta)\). Its nonnegativity conditions are exactly
\(\alpha\geq0\), \(\beta\geq0\), and \(\alpha+\beta\leq1\). These also ensure nonnegativity of \(1-\alpha\) and \(1-\beta\).

At \((a_2,b_1)\), the only lower-ranked employer is \(b_3\), and the only lower-ranked worker is \(a_1\). Hence the two residuals are \(\beta\) and \(\alpha\), respectively.

The other six acceptable pairs are exhaustively listed. For the three worker-worst pairs, full row assignment makes \(r_{ab}(x)=0\). For the three employer-worst pairs, full column assignment makes \(s_{ab}(x)=0\).

Thus the stable set is exactly the two stated segments, including their endpoints and common intersection. The proposed rational inequality descriptions correctly specify those segments.

Both \(U=x(1,0)\) and \(V=x(0,1)\) are stable. Their midpoint has \(\alpha=\beta=\tfrac12\), so its stability product at \((a_2,b_1)\) equals \(\tfrac14>0\). A convex subset of the stable set therefore cannot contain both endpoints.

In the disjoint-copy construction, all cross-copy coordinates are forced to zero. Feasibility and stability separate by copy, so the stable set is the asserted embedded Cartesian product.

Any two distinct selected endpoint matrices differ in some copy; their midpoint is unstable in that copy. Exactness of a union implies that each constituent polyhedron lies entirely inside the stable set. Convexity therefore permits each constituent to contain at most one selected endpoint matrix.

Covering all \(2^k\) selected matrices requires at least \(2^k\) polyhedra. This applies to arbitrary rational polyhedra, regardless of their dimension, overlap, or inequality descriptions. The asserted matching upper bound follows from choosing one local segment per copy.

The constructed inputs have \(m=7k\), \(\tau=6k\), and polynomial bit length. The sparse encoding estimate \(L=O(k\log(k+1))\) is consistent with constant-length lists and binary identifiers; a dense encoding remains polynomial in \(k\).

An explicitly listed union containing at least \(2^k\) polyhedra requires at least that much output-writing time. This exceeds every polynomial in the stated input parameters along this family.

This is a valid resolution of the polynomial total-time possibility. It leaves reduction-based NP-hardness unclassified, precisely as the prover says.

[Dean–Munshi, Lemma 12](https://people.computing.clemson.edu/~bcdean/stable_alloc.pdf) describes a correspondence between stable assignments and rotation vectors subject to bounds and precedence conditions. This supports the stated distinction between that representation and an explicit union in matrix coordinates. The proof under audit does not invoke this theorem to establish its lower bound, so no theorem application or hypothesis verification is missing from the central argument.

No repair or additional clarification is required.

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