Answer: Polynomial-time solvable in \(m,\tau,L\).
Theorem 3, item 4 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateIt is NP-complete to decide if for a given matching game, initial matching M0 and stable matching M ∗, there is a sequence of improvement steps leading form M0 to M ∗. This holds even for bipartite games with strict correlated preferences in the case of 1. socially stable matching and locally stable matching, 2. considerate matching, and 3. friendship matching for symmetric α-values in [0, 1]. In addition, it holds for ordinary bipartite stable matching in the case of 4. correlated preferences with ties, 5. strict preferences.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given finite type sets \(A,B\), rational masses \(\mu_a,\nu_b\) summing to \(1\) on each side, allowed pairs \(E\subseteq A\times B\), positive rational shared benefits \(w_{ab}\), and rational initial and target mass matchings \(x^0,x^\star\), decide whether a finite sequence of legal blocking steps takes \(x^0\) exactly to \(x^\star\). A mass matching satisfies \(\sum_b x_{ab}\leq\mu_a\) and \(\sum_a x_{ab}\leq\nu_b\). A step selects an allowed pair \((a,b)\) with positive mass on both sides of agents who are unmatched or strictly prefer that pair to their current partner, then matches the same positive rational mass \(\delta\) from those pools, dissolving their prior matches. The target must be stable, meaning no allowed pair has positive willing mass on both sides.
Let \(A,B\) be disjoint finite type supports with positive binary-rational masses \(\mu_a,\nu_b\), summing to \(1\) on each side. A society is given by its support: the list of types with positive mass and their binary-rational masses. Set \(\tau=|A|+|B|\), the support size, not the number of possible types; let \(m=|E|\) and \(L\) be the total input bit length.
Allowed pairs are \(E\subseteq A\times B\), with shared benefits \(w_{ab}\in\mathbb{Q}_{>0}\). Types rank partners by these benefits; equal benefits are ties, with no tie-breaking, and unmatched agents receive \(0\).
A mass matching is \(x\in\mathbb{Q}_{\geq0}^{E}\) satisfying \(\sum_b x_{ab}\leq\mu_a\) and \(\sum_a x_{ab}\leq\nu_b\); entries outside \(E\) are zero. Write \(u_a=\mu_a-\sum_b x_{ab}\) and \(v_b=\nu_b-\sum_a x_{ab}\).
For \((a,b)\in E\), its willing pools consist of unmatched mass and mass currently assigned to strictly worse partners: their sizes are \(P_{ab}=u_a+\sum_{c:w_{ac}<w_{ab}}x_{ac}\) and \(Q_{ab}=v_b+\sum_{d:w_{db}<w_{ab}}x_{db}\), summing only over allowed pairs.
A legal step selects \((a,b)\in E\) and rational portions totaling the same \(\delta\in\mathbb{Q}_{>0}\) from each willing pool. It dissolves exactly the selected portions of their previous matches, leaves their former partners unmatched, and increases \(x_{ab}\) by \(\delta\). Portions may be split arbitrarily; an already positive entry may be increased.
The input contains feasible \(x^0,x^\star\), with \(x^\star\) stable: for every \((a,b)\in E\), \(P_{ab}=0\) or \(Q_{ab}=0\).
Is deciding whether a finite sequence of legal steps takes \(x^0\) exactly to \(x^\star\) solvable in time polynomial in \(m,\tau,L\), or is it NP-hard? The sequence may have length zero.
Discrete prescribed-stable-matching reachability is NP-complete for ordinary bipartite matching with shared positive benefits and ties. [Hoefer–Wagner](https://pure.mpg.de/rest/items/item_2073063/component/file_2073062/content)
For divisible stable allocations with strict preferences, a polynomial-time better-response construction reaches some stable allocation; this concerns an unspecified endpoint. [Cseh–Skutella](https://real.mtak.hu/83554/1/MTDP1820.pdf)
No result settling the exact mass reachability problem above was identified in the literature search.
The problem is solvable in time polynomial in \(m,\tau,L\). In fact, the same conclusion holds for any prescribed feasible rational target, without assuming that it is stable.
The proof gives an exact reduction to reachability in rational continuous Petri nets.
A rational continuous Petri net has a finite place set \(\mathcal P\), a finite transition set \(T\), and nonnegative integer matrices \(\mathrm{Pre},\mathrm{Post}\). A marking is a vector \(h\in\mathbb Q_{\geq0}^{\mathcal P}\). Firing transition \(t\) by a positive rational amount \(\lambda\) is permitted when
\(\displaystyle h(p)\geq\lambda\,\mathrm{Pre}(p,t)\quad\text{for every }p\in\mathcal P,\)
and produces
\(\displaystyle h'=h+\lambda\bigl(\mathrm{Post}(\cdot,t)-\mathrm{Pre}(\cdot,t)\bigr).\)
We use the following known theorem:
Continuous reachability theorem. Given such a net and two rational markings encoded in binary, deciding whether a finite sequence of rational firings takes the first marking exactly to the second is polynomial-time solvable.
This is the rational reachability result of Fraca–Haddad, stated explicitly in Proposition 2.4 of [Blondin–Finkel–Haase–Haddad, *The Logical View on Continuous Petri Nets*](https://michaelblondin.com/papers/BFHH17.pdf). That paper uses binary encodings of integers and rationals and defines reachability through finite rational firing sequences.
We now verify that the matching dynamics have precisely this form.
Create distinct places:
Thus \(|\mathcal P|=m+\tau\).
For a feasible mass matching \(x\), define its marking \(h(x)\) by
\(\displaystyle h(x)(M_{ab})=x_{ab},\qquad h(x)(U_a)=u_a,\qquad h(x)(V_b)=v_b.\)
These markings satisfy the type-mass identities
\(\displaystyle h(U_a)+\sum_{b:(a,b)\in E}h(M_{ab})=\mu_a,\)
\(\displaystyle h(V_b)+\sum_{a:(a,b)\in E}h(M_{ab})=\nu_b.\)
Conversely, any nonnegative rational marking satisfying these identities determines a feasible mass matching by setting \(x_{ab}=h(M_{ab})\). The unmatched coordinates are then forced by the identities.
Consequently, this encoding is a bijection between feasible mass matchings and nonnegative rational markings satisfying the type-mass identities.
Fix an allowed pair \(e=(a,b)\). Define its possible source places on the two sides:
\(\displaystyle S_e^A=\{U_a\}\cup\{M_{ac}:(a,c)\in E,\ w_{ac}<w_{ab}\},\)
\(\displaystyle S_e^B=\{V_b\}\cup\{M_{db}:(d,b)\in E,\ w_{db}<w_{ab}\}.\)
Their total markings are exactly \(P_{ab}\) and \(Q_{ab}\).
For each \(s\in S_e^A\) and \(r\in S_e^B\), introduce a transition \(t_{e,s,r}\). Its inputs are one unit from \(s\) and one unit from \(r\). Its outputs are:
All unspecified matrix entries are zero.
The two input places are distinct. Indeed, unmatched places have distinct labels, and equality \(M_{ac}=M_{db}\) would imply \(d=a\) and \(c=b\), contradicting the strict benefit inequalities defining the source sets. Also, \(c\neq b\) and \(d\neq a\). Thus all arc coefficients belong to \(\{0,1\}\).
Firing this transition by amount \(\lambda\) takes precisely \(\lambda\) mass from one willing source on each side, dissolves any selected previous matches, leaves their former partners unmatched, and adds \(\lambda\) to \(x_{ab}\).
Every transition preserves the type-mass identities. For type \(a\), it removes \(\lambda\) either from \(U_a\) or from an incident matching place and adds \(\lambda\) to \(M_{ab}\). The same reasoning applies to \(b\). If a former partner \(c\) exists, its loss of \(\lambda\) at \(M_{ac}\) is offset by a gain of \(\lambda\) at \(V_c\); the analogous statement holds for \(d\). Every other type is unchanged.
It follows that all markings reachable from \(h(x^0)\) encode feasible mass matchings. Every positive rational firing is a legal matching step. In particular, the construction permits increasing an already positive entry, and equal-benefit partners never appear among its sources.
We must also show that a legal step using several source places can be simulated.
Consider a legal step forming \(e=(a,b)\) with total amount \(\delta\in\mathbb Q_{>0}\). Let \(\alpha_s\) be the amount selected from each \(s\in S_e^A\), and let \(\beta_r\) be the amount selected from each \(r\in S_e^B\). Legality gives
\(\displaystyle \sum_s\alpha_s=\sum_r\beta_r=\delta,\qquad 0\leq\alpha_s\leq h(s),\qquad 0\leq\beta_r\leq h(r).\)
Define rational amounts
\(\displaystyle \lambda_{s,r}=\frac{\alpha_s\beta_r}{\delta}.\)
Their row and column sums are
\(\displaystyle \sum_r\lambda_{s,r}=\alpha_s,\qquad \sum_s\lambda_{s,r}=\beta_r.\)
Fire each transition \(t_{e,s,r}\) for which \(\lambda_{s,r}>0\), by that amount, in any order.
To verify enabling, observe that none of these transitions produces mass at any source place in \(S_e^A\cup S_e^B\). Their matching output is \(M_{ab}\), which is excluded from both source sets. Any unmatched output is \(V_c\) with \(c\neq b\), or \(U_d\) with \(d\neq a\).
For any fixed source place, its total consumption over the whole sequence is therefore its selected amount, which is at most its initial marking. Immediately before any particular firing, its remaining marking is at least the sum of its remaining scheduled consumptions, hence at least the amount required by that firing. Every firing is enabled.
The sequence consumes exactly \(\alpha_s\) and \(\beta_r\) from the respective sources. It creates
\(\displaystyle \sum_{s,r}\lambda_{s,r}=\delta\)
at \(M_{ab}\), and releases exactly the selected portions to their former partners’ unmatched places. Its final marking is therefore precisely the marking produced by the original legal step.
This decomposition is finite and rational.
Combining both directions proves the exact equivalence:
\(\displaystyle x^\star\text{ is reachable from }x^0\text{ by finitely many legal steps} \iff h(x^\star)\text{ is reachable from }h(x^0)\text{ by finitely many rational firings}. \)
The empty sequence is allowed on both sides.
For each \(e=(a,b)\),
\(\displaystyle |S_e^A|\leq |B|+1,\qquad |S_e^B|\leq |A|+1.\)
Hence the number of transitions is at most
\(\displaystyle |T|=\sum_{e\in E}|S_e^A||S_e^B| \leq m(|B|+1)(|A|+1) =O(m\tau^2). \)
Each transition has two input arcs and at most three output arcs, all with coefficient one. The net therefore has polynomial encoding length.
Its construction requires only comparisons of input rational benefits and enumeration of source pairs. The markings \(h(x^0)\) and \(h(x^\star)\) require rational sums and differences of input quantities. These computations have polynomial bit complexity: denominators can be combined using products whose bit lengths are bounded by the sum of the operand bit lengths.
The algorithm is therefore:
All hypotheses of the cited theorem hold: the net is finite, its incidence matrices contain nonnegative integers, and both markings are nonnegative binary-encoded rational vectors. Section 4 proves that its answer is exactly the answer to the specified finite-sequence matching problem.
The construction uses only the listed support types. It never expands a mass into individual agents. Target stability is unnecessary for the reduction.
⟨structured verdict parsed — rendered above⟩
The prover’s output resolves the task correctly. The reduction preserves exact reachability by finite rational sequences, and the cited polynomial-time theorem applies to the constructed net. No major or minor mathematical issues were found.
The stronger claim—allowing any prescribed feasible rational target—is also established.
The external reference supports the theorem as stated:
These statements were checked in [Blondin–Finkel–Haase–Haddad, *The Logical View on Continuous Petri Nets*](https://michaelblondin.com/papers/BFHH17.pdf).
The reference permits zero firing amounts in its sequence notation. This does not change the application: such firings leave the marking unchanged and can be deleted. Thus its reachability relation agrees with finite sequences of positive rational firings, including the empty sequence.
Assessment: The theorem is stated precisely enough, its citation is accurate, and its semantics match the required reachability question.
For every feasible allocation, the matching coordinates and the unmatched coordinates are nonnegative rational numbers satisfying the stated type-mass identities.
Conversely, those identities force each unmatched coordinate to equal its type’s mass minus the sum of its incident matching coordinates. Nonnegativity therefore gives exactly the allocation’s capacity constraints.
The distinct place labels avoid identifying unmatched coordinates with matching coordinates or with unmatched coordinates on the opposite side.
Assessment: The claimed bijection is correct.
For a selected pair \(e=(a,b)\), the source sets contain exactly unmatched mass and matches with strictly smaller benefits. Their total markings are therefore precisely the willing-pool sizes.
The two selected source places cannot coincide. If matching places \(M_{ac}\) and \(M_{db}\) coincided, then \(c=b\) and \(d=a\), whereas membership in either matching-source set requires a strict inequality against \(w_{ab}\). This would require \(w_{ab}<w_{ab}\).
The outputs also have the intended interpretation:
The restrictions \(c\neq b\) and \(d\neq a\) exclude collisions with the selected endpoints. The output places are mutually distinct, so the claimed coefficients in \(\{0,1\}\) are correct.
An enabled firing of positive rational amount consumes available willing mass on both sides and performs exactly these updates.
Assessment: Every positive firing is a legal matching step, including firings that increase an already positive matching entry.
The preservation argument accounts for every affected type:
Because \(A\) and \(B\) are disjoint and the former partners differ from the selected endpoints, these cases do not overlap incorrectly.
Nonnegative markings satisfying the type-mass identities therefore remain within the image of feasible allocations.
Assessment: No additional feasibility constraints are missing from the net.
The selected amounts \(\alpha_s\) and \(\beta_r\) are rational, nonnegative, and each family sums to the positive rational number \(\delta\). Consequently,
\[
\lambda_{s,r}=\frac{\alpha_s\beta_r}{\delta}
\]
is well-defined and rational. Its row and column sums are exactly the selected amounts, as claimed.
The enabling argument is valid. For this fixed pair, no transition produces mass at any source place: \(M_{ab}\) is excluded by strict comparison, and the unmatched outputs belong to former partners rather than the selected endpoints.
Since the two source families are disjoint, the total scheduled consumption at each source is exactly its selected amount. That amount does not exceed its initial marking. After any prefix of the scheduled firings, the remaining marking therefore covers every remaining scheduled consumption, including the next firing.
The final matching and unmatched coordinates agree exactly with the original legal step. There are finitely many source pairs, and zero amounts are skipped.
Assessment: The decomposition is correct in any order and requires neither limiting behavior nor irrational portions.
The two established directions compose over finite sequences:
The marking bijection ensures that the prescribed endpoint is preserved exactly. The empty sequence is explicitly included on both sides.
Assessment: The equivalence establishes prescribed-target reachability, rather than merely reaching some stable allocation or approaching the target.
The place count \(m+\tau\) is correct. The transition count satisfies
\[
|T|\leq m(|B|+1)(|A|+1)=O(m\tau^2).
\]
Each transition has constant-size arc data apart from its place identifiers. Even a dense matrix representation would remain polynomial in the stated parameters.
Exact comparisons of binary-encoded rational benefits take polynomial time. Computing unmatched coordinates also has polynomial bit complexity: products of input denominators have bit lengths bounded by sums of operand bit lengths, and the corresponding numerator arithmetic remains polynomial.
The constructed markings are nonnegative by the input feasibility promise. Thus every hypothesis of the cited algorithm is met with a polynomial-size instance.
If \(E\) is empty, there are no transitions, and the same reachability formulation correctly reduces to equality of the initial and target markings. Ties are handled by strict source comparisons throughout.
Assessment: The claimed polynomial-time decision procedure follows. No polynomial bound on witness-sequence length is needed for this decision result.
None. The proof establishes the requested polynomial-time upper bound, and target stability is indeed unnecessary for the reduction.
⟨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.