← back to the atlas

Proportional Representation in Matching Markets: Selecting Multiple Matchings under Dichotomous Preferences (aamas22-00019)

Answer: Polynomial-time solvable; the problem belongs to \(\mathrm{P}\).

The anchor (named result in the paper)

Theorem 4.3 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateLet w be a weight sequence with w1 > w2 > 0. Given a matching election (N,A,k) and some number α ∈R, deciding whether there exists a committee M of size k with scw(M) ≥α is NP-complete for k = 2 and even if each agent approves at most three agents. In contrast to this, all w-Thiele rules are tractable in bipartite matching elections.

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

The continuous mirror question, as graded

Given a finite type set \(T\), rational masses \(\mu_t\) summing to \(1\), approval sets \(A_t\subseteq T\), rational \(w_1>w_2>0\), and threshold \(\alpha\), decide whether there exist two type-level mass matchings \(x^1,x^2\) satisfying \(2x^j_{\{t,t\}}+\sum_{u\ne t}x^j_{\{t,u\}}\le\mu_t\), using only pairs approved by at least one endpoint, together with \(z_{t,S}\ge0\) for \(S\subseteq\{1,2\}\), \(\sum_S z_{t,S}=\mu_t\), and \(\sum_{S\ni j}z_{t,S}=p_{t,j}\), where \(p_{t,j}\) is the mass of type \(t\) approving its partner in round \(j\), such that \(\sum_{t\in T}\sum_{S\subseteq\{1,2\}}z_{t,S}\sum_{i=1}^{|S|}w_i\ge\alpha\).

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

Definitions. An instance has a finite type set \(T\), rational masses \(\mu_t\ge0\) with \(\sum_t\mu_t=1\), approval sets \(A_t\subseteq T\), rational \(w_1>w_2>0\), and rational \(\alpha\). For each round \(j\in\{1,2\}\), a type-level mass matching is \(x^j_{\{t,u\}}\ge0\) on unordered pairs, with \(2x^j_{\{t,t\}}+\sum_{u\ne t}x^j_{\{t,u\}}\le\mu_t\), and \(x^j_{\{t,u\}}>0\) only if \(u\in A_t\) or \(t\in A_u\).
Let \(p_{t,j}=2\mathbf{1}[t\in A_t]x^j_{\{t,t\}}+\sum_{u\ne t:\,u\in A_t}x^j_{\{t,u\}}\). Also choose \(z_{t,S}\ge0\) for \(S\subseteq\{1,2\}\), with \(\sum_S z_{t,S}=\mu_t\) and \(\sum_{S\ni j}z_{t,S}=p_{t,j}\).

Target. Is deciding whether there are such variables with \(\sum_{t\in T}\sum_{S\subseteq\{1,2\}}z_{t,S}\sum_{i=1}^{|S|}w_i\ge\alpha\) solvable in polynomial time, or is it NP-hard?

Known results. The corresponding discrete matching-election decision problem is NP-complete for \(k=2\), for every \(w_1>w_2>0\), even when each agent approves at most three agents.
No result for this exact mass-matching formulation is stated by that discrete result.

Prover output (gpt-5.6-sol / xhigh, Bolzano prover prompt)

Classification: Polynomial-Time Solvable

Theorem

The stated mass-matching decision problem belongs to \(\mathrm{P}\). More precisely, it is the feasibility problem for a rational linear program of polynomial size. Consequently, it is not \(\mathrm{NP}\)-hard unless \(\mathrm{P}=\mathrm{NP}\).

Proof

Let \(n=|T|\), and define the set of admissible unordered pairs by

\(E=\{\{t,u\}:u\in A_t\text{ or }t\in A_u\}\).

For a disallowed pair, the condition that \(x^j_{\{t,u\}}>0\) is permitted only for admissible pairs is exactly enforced by setting \(x^j_{\{t,u\}}=0\). Equivalently, variables for disallowed pairs can simply be omitted.

Introduce the following variables:

There are only four subsets \(S\subseteq\{1,2\}\).

For every \(t\in T\) and \(j\in\{1,2\}\), impose the matching-capacity constraint

\(2x^j_{\{t,t\}}+\sum_{u\ne t}x^j_{\{t,u\}}\le \mu_t\),

where omitted or disallowed variables are understood to be zero. Define approved mass using the linear equality

\(p_{t,j}=2\mathbf{1}[t\in A_t]x^j_{\{t,t\}}+\sum_{u\ne t:\,u\in A_t}x^j_{\{t,u\}}\).

The required coupling constraints are

\(\sum_{S\subseteq\{1,2\}}z_{t,S}=\mu_t\)

and

\(\sum_{S\subseteq\{1,2\}:\,j\in S}z_{t,S}=p_{t,j}\)

for every \(t\in T\) and \(j\in\{1,2\}\).

Finally, impose the threshold constraint

\(\sum_{t\in T}\bigl(w_1z_{t,\{1\}}+w_1z_{t,\{2\}}+(w_1+w_2)z_{t,\{1,2\}}\bigr)\ge\alpha\).

This is exactly the objective inequality in the question because the contribution is zero for \(S=\varnothing\), equals \(w_1\) for either singleton, and equals \(w_1+w_2\) for \(S=\{1,2\}\).

All these constraints are linear, and all their coefficients are rational.

There are at most \(n(n+1)\) matching variables over the two rounds, \(2n\) variables \(p_{t,j}\), and \(4n\) variables \(z_{t,S}\). Thus the total number of variables and constraints is polynomial in \(n\), and their encoding length is polynomial in the input encoding length. Feasibility of a rational linear program is decidable in polynomial time by standard rational linear-programming algorithms.

Therefore the decision problem belongs to \(\mathrm{P}\).

Structure of the Two-Round Coupling

The coupling variables do not conceal an integral choice. Fix a type \(t\), and write \(a=p_{t,1}\), \(b=p_{t,2}\), and \(q=z_{t,\{1,2\}}\). The coupling equalities force

\(z_{t,\{1\}}=a-q\),

\(z_{t,\{2\}}=b-q\),

and

\(z_{t,\varnothing}=\mu_t-a-b+q\).

Hence nonnegativity is equivalent to

\(\max\{0,a+b-\mu_t\}\le q\le\min\{a,b\}\).

The matching-capacity constraints imply \(0\le a,b\le\mu_t\), so this interval is always nonempty. The contribution of type \(t\) is

\(w_1(a+b)+(w_2-w_1)q\).

Because \(w_1>w_2\), an optimal coupling takes

\(q=\max\{0,a+b-\mu_t\}\).

Thus the optimized contribution is the concave piecewise-linear function

\(w_1(a+b)\) when \(a+b\le\mu_t\), and

\(w_1\mu_t+w_2(a+b-\mu_t)\) when \(a+b\ge\mu_t\).

The original \(z\)-variable formulation is precisely a linear extended formulation of this function.

Relation to the Discrete Hardness Result

The discrete \(\mathrm{NP}\)-completeness result does not transfer to this formulation. In the discrete problem, agents are indivisible and their identities across rounds create combinatorial choices. Here each type mass can be split fractionally among edges and among the four round-approval patterns. The resulting feasible region is a rational polyhedron with no integrality requirement.

⟨structured verdict parsed — rendered above⟩

Adversarial review (gpt-5.6-sol / high, Bolzano verifier prompt)

Verification Report

Overall assessment

The prover correctly classifies the problem as polynomial-time solvable. The proposed linear program is an exact formulation of the stated feasibility problem, has polynomial size, and has rational coefficients of polynomial encoding length. No integrality condition is present in the problem statement, so rational linear-programming feasibility applies directly.

Step-by-step audit

Defining \(E\) as the set of unordered pairs satisfying at least one directed approval condition exactly captures the stated support restriction. Omitting variables for disallowed pairs is equivalent to requiring those variables to equal zero.

There are at most \(n(n+1)/2\) unordered pairs including loops, hence at most \(n(n+1)\) matching variables across both rounds. The \(2n\) variables \(p_{t,j}\) and \(4n\) variables \(z_{t,S}\) are also polynomially many.

The displayed capacity constraint correctly gives a loop twice the mass usage of a non-loop edge. Treating omitted variables as zero preserves the original constraint exactly.

The equality defining \(p_{t,j}\) matches the problem definition, including the factor \(2\) for an approved self-loop. Although the prover does not explicitly impose \(p_{t,j}\ge 0\), this follows from its equality to a nonnegative linear combination of nonnegative \(x\)-variables.

The two families of equalities for \(z_{t,S}\) reproduce the required marginal conditions exactly. Since there are only four subsets of two rounds, these constraints do not cause exponential growth.

The coefficients are correct: the empty pattern contributes zero, either singleton contributes \(w_1\), and the two-round pattern contributes \(w_1+w_2\). Thus the threshold inequality is exactly the target welfare inequality.

Every coefficient is either rational input data or a fixed integer. The resulting rational LP has polynomially many variables and constraints and polynomial total encoding length. Standard bit-complexity results for rational linear-programming feasibility therefore establish membership in \(\mathrm{P}\).

The derived expressions for the four \(z\)-variables and the interval
\[ \max\{0,a+b-\mu_t\}\le q\le\min\{a,b\} \]
are correct. The interval is nonempty when \(0\le a,b\le\mu_t\), which follows from the matching-capacity constraints. Because \(w_2-w_1<0\), minimizing \(q\) maximizes the contribution, and the stated piecewise-linear expression follows. This section is consistent with, though unnecessary for, the main LP argument.

The prover correctly avoids importing the discrete NP-completeness result. The stated continuous formulation contains no indivisibility or integrality restriction, so that discrete result does not contradict the LP classification.

No substantive or expositional defect was found.

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