Answer: Both Pareto-improvement detection and Pareto-optimality verification are in \(\mathrm P\), with bit running time \(\left(L(m+1)^4+m+\tau\right)^{O(1)}\).
Theorem 3.3 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateDeciding whether a given matching 𝑀 is Pareto-optimal for the stable many-to-many matching problem under lexicographic preferences is co-NP-complete, even for complete matchings. It is also co-NP-hard to decide whether 𝑀 is a maximum size Pareto-optimal matching.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a bipartite market with supported agent types, rational masses \(\mu_t\), capacities \(k_t\le 4\), and rankings of acceptable counterpart types, together with a feasible complete mass allocation \(y_{t,b}\) over integral partner-count bundles \(b\), decide whether \(y\) is Pareto-optimal. A Pareto improvement is a feasible reassignment of the same mass from old bundles to weakly preferred new bundles in which a positive mass strictly improves.
The market has two nonempty sides of nonatomic agent types, with mutual acceptability and strict rankings of acceptable counterpart types; every acceptable partner is preferred to an empty slot. Each type \(t\) has capacity \(k_t\in\{1,2,3,4\}\). A society is given by its support: the list of the \(\tau\) types with positive mass, each with its mass \(\mu_t\) as a binary rational, with \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types. Let \(m\) be the number of mutually acceptable type pairs and \(L\) the total input bit length; state running times in \(m,\tau,L\).
A bundle \(b\) for type \(t\) is an integral vector of acceptable counterpart-type counts, with \(b_s\geq0\) and \(\sum_s b_s\leq k_t\). Multiple partners of one type are allowed, representing distinct individuals. Between distinct bundles, the preferred bundle has the larger count at the highest-ranked type whose counts differ; write this order as \(\succ_t\).
An allocation \(z\) consists of nonnegative bundle masses satisfying \(\sum_b z_{t,b}=\mu_t\) and, for every acceptable pair \(t,s\), \(\sum_b z_{t,b}b_s=\sum_c z_{s,c}c_t\). These conditions define feasibility. The input explicitly lists a feasible allocation \(y\) with binary-rational entries; it is complete, meaning \(y_{t,b}>0\) only when \(\sum_s b_s=k_t\).
A reassignment consists of nonnegative real masses \(x_{t,b,c}\) satisfying \(\sum_c x_{t,b,c}=y_{t,b}\), with \(x_{t,b,c}=0\) unless \(c=b\) or \(c\succ_t b\), and inducing a feasible allocation \(z_{t,c}=\sum_b x_{t,b,c}\). It is a Pareto improvement if \(\sum_{t,b,c:\,c\succ_t b}x_{t,b,c}>0\). New bundles may leave capacity unused. The allocation \(y\) is Pareto-optimal if no such improvement exists.
Is deciding whether \(y\) admits a Pareto improvement in \(\mathrm P\), or is it \(\mathrm{NP}\)-hard—equivalently, is Pareto-optimality verification in \(\mathrm P\), or is it \(\mathrm{coNP}\)-hard?
Discrete Pareto-optimality verification under lexicographic preferences is coNP-complete even for complete bipartite matchings with capacities at most four. For fractional edge matchings with lexicographic comparisons of edge weights, a strong-core matching can be computed in quadratic time in the number of edges; that result concerns a different continuous model. [Biró and Csáji (2024)](https://doi.org/10.1016/j.geb.2024.03.010)
1. Result
Both deciding whether \(y\) admits a Pareto improvement and verifying Pareto-optimality are in \(\mathrm P\).
The key is that capacity at most four gives polynomially many integral bundles per supported type. Real masses assigned to allowed bundle transitions can then be handled by a polynomial-size rational linear program. This preserves the bundle-level preference comparisons in the question.
2. Enumerating bundles and allowed transitions
Let \(A\) and \(B\) be the two sides of the support, and let \(E\) be their mutually acceptable pairs. Only supported counterpart types need be considered: a type of zero mass cannot supply any partners, because feasibility equates the corresponding nonnegative partner counts to zero. Thus \(|E|\leq m\).
For a supported type \(t\), let \(d_t\) be its number of acceptable supported counterpart types, and let \(\mathcal B_t\) be its set of bundles. Counting nonnegative integer vectors with total at most \(k_t\) gives
\( \displaystyle |\mathcal B_t|=\binom{d_t+k_t}{k_t}\leq\binom{m+4}{4}. \)
Indeed, adding a slack coordinate converts the condition that the total is at most \(k_t\) into an equality with total \(k_t\); the displayed count follows by stars and bars. This enumeration includes bundles with unused capacity and repeated counterpart types.
Define
\( \displaystyle \mathcal Y_t=\{b:y_{t,b}>0\},\qquad r=\sum_t|\mathcal Y_t|. \)
Because \(y\) is explicitly listed, \(r\leq L\). For each \(b\in\mathcal Y_t\), enumerate
\( \displaystyle \mathcal C_{t,b}=\{c\in\mathcal B_t:c=b\text{ or }c\succ_t b\}. \)
Membership is decidable directly from the given ranking: find the highest-ranked coordinate at which the two bundles differ and compare its counts.
Introduce a variable \(x_{t,b,c}\) for every \(b\in\mathcal Y_t\) and \(c\in\mathcal C_{t,b}\). The number \(N\) of variables satisfies
\( \displaystyle N\leq r\binom{m+4}{4}=O\!\left(L(m+1)^4\right). \)
Old bundles with zero mass require no variables: their reassignment row sums force all their transition masses to zero.
3. The linear program and its correctness
Require nonnegativity and preservation of every old bundle mass:
\( \displaystyle x_{t,b,c}\geq0,\qquad \sum_{c\in\mathcal C_{t,b}}x_{t,b,c}=y_{t,b}\quad(t,\ b\in\mathcal Y_t). \)
For every acceptable pair \((a,s)\in E\), with \(a\in A\) and \(s\in B\), impose partner-count balance:
\( \displaystyle \sum_{b\in\mathcal Y_a}\sum_{c\in\mathcal C_{a,b}}c_sx_{a,b,c} - \sum_{b\in\mathcal Y_s}\sum_{c\in\mathcal C_{s,b}}c_ax_{s,b,c} =0. \)
Maximize the total mass receiving a strictly preferred bundle:
\( \displaystyle F(x)=\sum_{t}\sum_{b\in\mathcal Y_t}\sum_{\substack{c\in\mathcal C_{t,b}\\c\succ_t b}}x_{t,b,c}. \)
There are \(Q=r+|E|\leq L+m\) equality constraints. All matrix coefficients are integers of absolute value at most four; the right-hand sides are input rationals.
The feasible region is nonempty. Set \(x_{t,b,b}=y_{t,b}\) and all other variables to zero. Partner-count balance then follows from feasibility of \(y\).
It is also bounded. Summing the old-bundle equations gives
\( \displaystyle \sum_{t,b,c}x_{t,b,c}=\sum_{t,b}y_{t,b}=\sum_t\mu_t=1. \)
Consequently every variable lies in \([0,1]\), and \(0\leq F(x)\leq1\). The feasible region is closed, so its maximum \(F^\ast\) exists.
We now prove the required equivalence.
\( \displaystyle z_{t,c}=\sum_{\substack{b\in\mathcal Y_t\\c\in\mathcal C_{t,b}}}x_{t,b,c}. \)
Nonnegativity is immediate. Summing the old-bundle equations yields \(\sum_cz_{t,c}=\mu_t\), and the pair equations give every required partner-count balance. Every transition preserves or improves the old bundle, and the strictly improved mass is \(F(x)>0\). Thus this point is a Pareto improvement.
Therefore
\( \displaystyle y\text{ admits a Pareto improvement}\quad\Longleftrightarrow\quad F^\ast>0. \)
4. Exact positivity and running time
Polynomial-time rational linear programming already permits exact determination of \(F^\ast\). The following explicit bound also shows why arbitrarily small real improvement masses cause no difficulty.
Write the equality constraints as \(Mx=h\), and let \(q\leq Q\) be the rank of \(M\). A linear objective on a nonempty bounded polyhedron attains its maximum at a vertex. For a standard-form polyhedron, a vertex has linearly independent positive-variable columns: otherwise a nonzero dependence would allow small perturbations in both directions, contradicting extremality. Extend those columns to a basis of \(q\) columns and choose \(q\) independent rows. The resulting square matrix \(H\) is nonsingular and integral, and the vertex coordinates are its basic solution, with all other coordinates zero.
Each column of \(M\) contains one old-bundle coefficient equal to one, together with signed target-bundle counts. Since a target bundle has total count at most four,
\( \displaystyle \|M_{\cdot j}\|_2^2=1+\sum_s c_s^2\leq1+\left(\sum_s c_s\right)^2\leq17. \)
Deleting rows cannot increase a column norm. Hadamard’s determinant inequality therefore gives
\( \displaystyle |\det H|\leq17^{q/2}\leq5^q. \)
Let \(D\) be the product of the denominators of the positive entries of \(y\), in their explicit binary rational encoding. Their total encoding length is at most \(L\), so \(D\leq2^L\), and \(Dh\) is integral.
By Cramer’s rule, every basic coordinate, and hence its objective value, has the form of an integer divided by \(D\det H\). Thus, if the optimal vertex has positive objective,
\( \displaystyle F^\ast\geq\frac{1}{D|\det H|}\geq2^{-L}5^{-Q}\geq2^{-(L+3Q)}. \)
Set \(\varepsilon=2^{-(L+3Q)}\). We have proved
\( \displaystyle F^\ast>0\quad\Longleftrightarrow\quad \text{the LP constraints together with }F(x)\geq\varepsilon\text{ are feasible}. \)
The threshold has \(O(L+Q)\) encoding length. Each original variable column has at most five nonzero entries, so the entire rational LP has polynomial encoding length in \(m,\tau,L\). Bundle enumeration and all preference tests also take polynomial time.
Applying the standard theorem that rational linear-program feasibility is decidable in time polynomial in its binary encoding length gives an overall bit running time of
\( \displaystyle \left(L(m+1)^4+m+\tau\right)^{O(1)}. \)
This is a polynomial bound, without a claim of quadratic running time.
5. Consequence
The algorithm answers yes precisely when the threshold LP is feasible. Reversing its answer verifies Pareto-optimality in the same polynomial time.
The distinction from discrete verification is that each old bundle cohort may be split into real masses across several allowed transitions. The LP imposes exactly the reassignment conditions stated in the question. Completeness of \(y\) is compatible with the argument, but is unnecessary: the same algorithm works for an explicitly listed feasible allocation containing incomplete old bundles.
⟨structured verdict parsed — rendered above⟩
The prover’s conclusion is correct: both Pareto-improvement detection and Pareto-optimality verification are in \(\mathrm P\) for the stated input model. The argument preserves preferences over integral bundles while allowing real masses of agents to move between those bundles. No mathematical gaps or incorrect steps were found.
Restricting attention to supported types is justified. Any unsupported type has zero total allocation mass; nonnegativity and pairwise balance therefore force all partner counts involving that type to be zero.
For a supported type \(t\), introducing one slack coordinate gives exactly
\[
|\mathcal B_t|=\binom{d_t+k_t}{k_t}.
\]
The bound by \(\binom{m+4}{4}\) holds because \(d_t\leq m\) and \(k_t\leq4\). This enumeration includes the empty bundle, partially filled bundles, and repeated partners of the same type, as required.
Comparing two enumerated bundles at their highest-ranked differing coordinate implements precisely the preference relation in the task. No preference assumption is changed.
The restriction to positive old-bundle masses is valid: a reassignment row with zero prescribed mass contains only nonnegative entries and thus must vanish.
Because the input explicitly lists \(y\), its number \(r\) of positive entries is at most its encoding length \(L\). Consequently,
\[
N\leq r\binom{m+4}{4}=O\!\left(L(m+1)^4\right).
\]
Enumerating bundles and testing allowable transitions therefore require polynomial time. The fixed capacity bound is essential to this estimate.
The row equations preserve the mass of each old-bundle cohort. Variables exist only for unchanged or strictly preferred target bundles, so the restriction on allowable transitions is enforced exactly.
The pair equations correctly count target partners on both sides of each acceptable pair. They are exactly the balance conditions for the induced allocation.
Summing the cohort equations for a fixed type gives its required total mass \(\mu_t\). Hence there is no missing type-mass constraint.
The objective counts precisely the mass undergoing a strict improvement. It neither counts unchanged transitions nor replaces bundle preferences with comparisons of aggregate edge weights.
The identity reassignment is feasible because \(y\) is feasible and every unchanged transition is allowed.
Summing all cohort equations gives
\[
\sum_{t,b,c}x_{t,b,c}=1.
\]
Together with nonnegativity, this bounds every variable between zero and one and bounds the objective between zero and one. The feasible set is closed and finite-dimensional, so it is compact and the maximum exists.
Both directions are established correctly.
Any reassignment allowed by the task restricts to an LP-feasible point: omitted zero-mass rows vanish, and unsupported partner coordinates cannot occur with positive mass. Its objective equals its strictly improved mass.
Conversely, an LP-feasible point induces a nonnegative allocation with the required type masses and pair balances. Extending omitted transitions by zero gives a reassignment satisfying every condition in the task. A positive objective supplies the required positive strictly improved mass.
Thus the asserted equivalence
\[
y\text{ admits a Pareto improvement}\iff F^\ast>0
\]
is valid, including for improvements using irrational real masses.
The theorem that a linear objective on a nonempty bounded polyhedron has a vertex maximizer applies: nonemptiness and boundedness have already been verified.
The justification for independent positive-variable columns is sound. A dependence supported on positive coordinates would permit sufficiently small feasible perturbations in both directions, contradicting extremality.
Extending those columns to a column basis and selecting independent rows produces the claimed nonsingular square matrix \(H\). Coordinates outside that basis vanish, so the vertex is represented by its basic solution.
Each original column has one cohort coefficient equal to one and pair coefficients corresponding to the target-bundle counts. Therefore
\[
\|M_{\cdot j}\|_2^2
=1+\sum_s c_s^2
\leq1+\left(\sum_s c_s\right)^2
\leq17.
\]
Restricting rows cannot increase the norm. Hadamard’s inequality consequently gives
\[
|\det H|\leq17^{q/2}\leq5^q.
\]
Both constants and inequalities are correct.
The product \(D\) of the input denominators satisfies \(D\leq2^L\), since their combined binary encoding length is at most \(L\). Multiplying the right-hand side by \(D\) makes it integral.
Cramer’s rule gives a common denominator \(D\det H\) for the basic coordinates. The objective has integer coefficients, so its value has that same denominator form. A positive optimal vertex objective therefore satisfies
\[
F^\ast\geq\frac{1}{D|\det H|}
\geq2^{-L}5^{-Q}
\geq2^{-(L+3Q)}.
\]
The final inequality uses \(5\leq2^3\) and is correct.
Consequently, adding \(F(x)\geq\varepsilon\), with the stated \(\varepsilon\), decides positivity exactly. This argument addresses arbitrarily small real improvements without assuming that an initially given improving reassignment is rational.
An original column has at most five nonzero entries: one cohort coefficient and at most four distinct partner-type coefficients. Adding the objective threshold introduces at most one additional coefficient per column.
The coefficients, input right-hand sides, indices, and threshold all have polynomial total encoding length. The cited theorem—rational LP feasibility is decidable in time polynomial in its binary encoding length—is stated sufficiently precisely, and its hypotheses are satisfied.
The reported bit running time
\[
\left(L(m+1)^4+m+\tau\right)^{O(1)}
\]
is therefore justified. Reversing the decision answer establishes polynomial-time Pareto-optimality verification.
The observation that completeness is unnecessary is also supported: none of the construction or correctness arguments requires old bundles to fill capacity. No additional clarification or repair 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.