← back to the atlas

d4-conf-wine-2014-0014 (d4-conf-wine-2014-0014)

Answer: Polynomial-time solvable in \(m,\tau,L\). The exact least-core value is \(\epsilon^*=\Theta/W(\mu)-1\), attained by \(p_i^*=y_i^*/W(\mu)\), where \(y^*\) is any optimal dual solution for the grand-coalition matching linear program.

The anchor (named result in the paper)

Proposition 2 [1] — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximate[1] Computing the least-core and nucleolus of T MG is NP-hard if the core of the TMG is empty. In the following we restrict ourselves to threshold cardinality matching game (TCMG) Γ = (V ; T ) based on unweighted graph G = (V, E). That is, ∀S ⊆N, v(S) = 1 if the size of a maximum matching in G[S] is no less than T , and v(S) = 0 otherwise.

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

The continuous mirror question, as graded

Given \(\tau\) types with rational masses \(\mu_t\) summing to \(1\), nonnegative rational matching weights \(w_{ij}\), and a threshold \(\Theta\), let a coalition have masses \(q_t\in[0,\mu_t]\) and matching value \(W(q)=\max\sum_{i\le j}w_{ij}z_{ij}\), subject to \(2z_{ii}+\sum_{j\ne i}z_{ij}\le q_i\) and \(z_{ij}\ge0\). Its worth is \(1\) when \(W(q)\ge\Theta\), and \(0\) otherwise. For instances whose grand population reaches the threshold and whose core is empty, compute the least-core value and an allocation \(p_t\ge0\) satisfying \(\sum_t\mu_t p_t=1\) and maximizing \(\epsilon\) subject to \(\sum_t q_t p_t\ge v(q)+\epsilon\) for every \(q\in[0,\mu]\).

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

A society is given by its support: a list of \(\tau\) types with positive binary rational masses \(\mu_i\), where \(\sum_i\mu_i=1\); \(\tau\) is the support size, not the number of possible types. Input also includes nonnegative binary rational weights \(w_{ij}\) for all \(1\le i\le j\le\tau\), and a positive binary rational threshold \(\Theta\). Let \(m=\tau(\tau+1)/2\) be the number of weight entries and \(L\) the total input bit length.
A coalition is any real mass vector \(q\in\prod_i[0,\mu_i]\). Define \(W(q)=\max\{\sum_{i\le j}w_{ij}z_{ij}:z_{ij}\ge0,\ 2z_{ii}+\sum_{j<i}z_{ji}+\sum_{j>i}z_{ij}\le q_i\text{ for every }i\}\). Within-type matching is allowed and consumes twice its matching mass; unmatched mass is allowed.
Set \(v(q)=1\) if \(W(q)\ge\Theta\), and \(v(q)=0\) otherwise. An allocation assigns a constant payoff density \(p_i\ge0\) to each type, with \(\sum_i\mu_i p_i=1\). Promise \(W(\mu)\ge\Theta\) and an empty core, meaning no such allocation satisfies \(\sum_iq_ip_i\ge v(q)\) for every coalition.
The least-core value is the maximum real \(\epsilon\) for which an allocation satisfies \(\sum_iq_ip_i\ge v(q)+\epsilon\) for every coalition, including the empty and grand coalitions.

Is exact computation of this least-core value and an attaining allocation polynomial-time solvable in \(m,\tau,L\), or is it \(\mathrm{NP}\)-hard?

For finite weighted threshold matching games with empty core, computing the least-core and nucleolus is \(\mathrm{NP}\)-hard; the unweighted least-core is polynomial-time computable ([Fang et al.](https://arxiv.org/pdf/1409.5987)).
For finite fractional matching games whose worth equals the matching value without thresholding, the least-core and nucleolus are polynomial-time computable ([Chen, Lu and Zhang](https://ojs.aaai.org/index.php/AAAI/article/download/8242/8101)). No result settling the mass-and-threshold problem above was located.

Modeling choices made when packaging the task

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

Exact polynomial-time solution

The problem is polynomial-time solvable in \(m,\tau,L\). Its least-core value is
\[ \epsilon^*=\frac{\Theta}{W(\mu)}-1. \]
An attaining allocation is obtained by normalizing any optimal solution of the dual matching linear program.

The proof applies whenever \(W(\mu)\ge\Theta>0\), including the promised empty-core case.

1. Matching linear program and its dual

Index the matching variables by pairs \((i,j)\) with \(i\le j\). Define the matrix \(A\in\mathbb{Q}^{\tau\times m}\) so that its column for \((i,j)\) is \(e_i+e_j\) when \(i<j\), and \(2e_i\) when \(i=j\). Here \(e_i\) is the \(i\)-th coordinate vector. Thus \(Az\) records the mass consumed at each type.

For any coalition \(q\), the matching problem is
\[ W(q)=\max\{w^{\mathsf T}z:Az\le q,\ z\ge0\}. \]

This linear program is feasible because \(z=0\) is feasible. Its feasible region is compact: each diagonal variable satisfies \(z_{ii}\le q_i/2\), and each off-diagonal variable satisfies \(z_{ij}\le\min\{q_i,q_j\}\). Hence its maximum is finite and attained.

Its dual is
\[ \min\left\{\sum_iq_i y_i: y_i\ge0,\quad y_i+y_j\ge w_{ij}\ (i<j),\quad 2y_i\ge w_{ii}\right\}. \]

The dual is feasible: taking every \(y_i=\max_{k\le l}w_{kl}\) satisfies its constraints. Strong linear-programming duality therefore applies.

Write \(M=W(\mu)\). There exists an optimal dual vector \(y^*\) satisfying
\[ y^*\ge0,\qquad A^{\mathsf T}y^*\ge w,\qquad \mu^{\mathsf T}y^*=M. \]

The promise gives \(M\ge\Theta>0\).

2. A coalition giving a universal upper bound

The matching value is positively homogeneous. For every nonnegative capacity vector \(q\) and every scalar \(a>0\), the map \(z\mapsto az\) is a bijection between the feasible matching vectors for \(q\) and those for \(aq\). Objectives scale by \(a\), so
\[ W(aq)=aW(q). \]

Set \(c=\Theta/M\). Since \(0<c\le1\), the vector \(q^0=c\mu\) is an admissible coalition. Homogeneity gives
\[ W(q^0)=cM=\Theta, \]
so \(q^0\) is winning.

For every admissible allocation \(p\), normalization implies
\[ (q^0)^{\mathsf T}p=c\,\mu^{\mathsf T}p=c. \]

Consequently, its least-core constraint requires \(c\ge1+\epsilon\). Every feasible least-core value therefore satisfies
\[ \epsilon\le c-1=\frac{\Theta}{M}-1. \]

3. A dual allocation attaining the bound

Define \(p_i^*=y_i^*/M\). Then \(p^*\ge0\), and
\[ \mu^{\mathsf T}p^*=\frac{\mu^{\mathsf T}y^*}{M}=1. \]
Thus \(p^*\) is an admissible allocation.

For any coalition \(q\) and any matching vector \(z\) feasible for \(q\), dual feasibility and nonnegativity give
\[ w^{\mathsf T}z \le (y^*)^{\mathsf T}Az \le (y^*)^{\mathsf T}q. \]
Taking the maximum over feasible \(z\) yields \(W(q)\le(y^*)^{\mathsf T}q\).

If \(q\) is winning, then
\[ q^{\mathsf T}p^* =\frac{(y^*)^{\mathsf T}q}{M} \ge\frac{W(q)}{M} \ge\frac{\Theta}{M}=c. \]
Hence its constraint holds with \(\epsilon=c-1\).

If \(q\) is losing, nonnegativity gives \(q^{\mathsf T}p^*\ge0\). Since \(c\le1\), we have \(0\ge c-1=v(q)+\epsilon\), so its constraint also holds.

This includes the empty coalition, which is losing because \(\Theta>0\), and the grand coalition, whose payoff is \(1\). Thus every coalition constraint holds. Together with the upper bound,
\[ \boxed{\epsilon^*=\frac{\Theta}{W(\mu)}-1,\qquad p_i^*=\frac{y_i^*}{W(\mu)}.} \]

4. Exact computation and bit complexity

Only the following rational linear program must be solved:
\[ \min\ \sum_i\mu_i y_i, \]
subject to \(y_i\ge0\), \(y_i+y_j\ge w_{ij}\) for \(i<j\), and \(2y_i\ge w_{ii}\).

It has \(\tau\) variables and \(m+\tau\) inequalities. Its coefficients comprise the supplied rational masses and weights, together with integers of bounded size. Its encoding length is polynomial in \(m,\tau,L\).

The standard polynomial-time theorem for rational linear programming computes an exact rational optimum and an optimal rational solution in time polynomial in the program’s binary encoding length. Exact recovery uses the polynomial bit-length bounds for rational basic solutions; see the [MIT notes on linear-programming algorithms](https://courses.csail.mit.edu/6.854/21/Notes/n14-LP_algorithms.html).

The hypotheses hold here: the program is feasible, and strong duality identifies its finite optimum with \(M\). An optimal basic solution has polynomial encoding length, as follows by clearing denominators and applying Cramer’s rule to its active constraints.

After obtaining \(y^*\), compute \(M=\sum_i\mu_i y_i^*\), then return \(p_i^*=y_i^*/M\) and \(\epsilon^*=\Theta/M-1\). These exact rational arithmetic operations also take polynomial time and produce outputs of polynomial encoding length.

5. Empty-core promise and the finite-game comparison

Under \(M\ge\Theta>0\), the core is empty exactly when \(\Theta<M\):

Thus the promised case has \(\epsilon^*<0\), with no additional algorithmic difficulty.

The finite weighted threshold-matching hardness result reported by [Fang et al.](https://arxiv.org/pdf/1409.5987) concerns indivisible players. Here, arbitrary real coalition masses permit the proportional winning coalition \(q^0\); fractional matching and duality supply the allocation attaining its universal bound. These arguments completely settle the stated mass-and-threshold problem.

⟨structured verdict parsed — rendered above⟩

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

Verification report

The claimed polynomial-time solution is correct. The proof establishes both the exact least-core value and an attaining allocation for the stated continuous model. No major or minor issues requiring repair were found.

1. Matching formulation and duality

The matrix \(A\) correctly represents mass consumption: an off-diagonal matching variable consumes one unit at each endpoint, while a diagonal variable consumes two units at its type. Thus the primal LP is exactly the matching problem in USER_TASK.

For every admissible coalition \(q\), the zero matching is feasible. The stated coordinate bounds are correct, including when some \(q_i=0\). Together with closedness, they establish compactness of the feasible region and attainment of a finite optimum.

The displayed dual has the correct objective, inequality directions, and nonnegativity restrictions. Its proposed feasible vector works because all weights are nonnegative. The strong-duality application is valid: the primal is feasible with a finite optimum, and the dual is feasible. Consequently, the optimal dual vector \(y^*\) and the equality \(\mu^{\mathsf T}y^*=M\) are justified.

The promise \(M\ge\Theta>0\) ensures that every subsequent division by \(M\) is valid.

2. Universal upper bound

The homogeneity argument is correct. For every positive scalar \(a\), scaling by \(a\) maps feasible matching vectors for \(q\) bijectively onto those for \(aq\), and scales the objective by \(a\).

Since \(c=\Theta/M\) satisfies \(0<c\le1\), the vector \(q^0=c\mu\) lies in the allowed coalition box. Its matching value equals \(\Theta\), so it is winning under the task’s inclusive threshold convention.

For every admissible allocation, normalization gives \((q^0)^{\mathsf T}p=c\). Applying the winning-coalition constraint therefore yields \(\epsilon\le c-1\). The quantifier is correct: this bounds every feasible allocation and least-core value.

3. Attainment

The proposed allocation \(p^*=y^*/M\) is nonnegative and satisfies the required normalization.

The inequality chain
\(w^{\mathsf T}z\le(y^*)^{\mathsf T}Az\le(y^*)^{\mathsf T}q\)
is valid. Its first inequality uses dual feasibility and \(z\ge0\); its second uses primal feasibility and \(y^*\ge0\).

Thus every winning coalition receives at least \(\Theta/M=c\), exactly the payoff required when \(\epsilon=c-1\).

For losing coalitions, the required lower bound is \(c-1\le0\), while their payoff is nonnegative. This covers all losing coalitions without additional assumptions.

The empty coalition is losing because its matching value is zero and \(\Theta>0\). The grand coalition is winning by the promise and receives payoff one. Both constraints are satisfied.

Accordingly, the upper bound is attained, proving
\(\epsilon^*=\Theta/W(\mu)-1\)
and the stated allocation formula. The argument establishes a maximum, not merely a supremum.

4. Exact computation and bit complexity

The computational claim is valid in the binary input model.

The dual LP has \(\tau\) variables and \(m+\tau\) inequalities. Its rational data come directly from the input, with constraint coefficients restricted to bounded integers. Its encoding length is therefore polynomial in the specified parameters.

The prover states the relevant rational-LP theorem: an exact rational optimal value and optimal rational solution can be computed in time polynomial in the binary encoding length. The required hypotheses—rational data, feasibility, and a finite attained optimum—have been verified. The cited [MIT LP notes](https://courses.csail.mit.edu/6.854/21/Notes/n14-LP_algorithms.html) discuss polynomial-time LP algorithms, polynomial vertex encoding bounds, and recovery of exact optimal vertices.

The reference to optimal basic solutions and Cramer’s rule correctly supports polynomial output length. It does not claim that enumerating bases is polynomial time.

Computing \(M\), dividing the selected rational optimal vector by \(M\), and computing \(\Theta/M-1\) require only polynomially many rational arithmetic operations on numbers of polynomial bit length.

“Any optimal solution” is valid for the mathematical allocation formula; the exact algorithm can return a rational optimal solution as specified in Section 4.

5. Empty-core promise and comparison

The claimed core characterization follows from the arguments already supplied:

These cases exhaust the promised range. Hence the empty-core promise implies \(\epsilon^*<0\).

The finite-game comparison is accurate. [Fang et al.](https://arxiv.org/pdf/1409.5987) define coalitions as subsets of graph vertices and report empty-core hardness in Proposition 2. That setting differs from the arbitrary real coalition masses used in this proof. The comparison is contextual and supplies no missing premise.

Required feedback

No repair or additional clarification is needed. The output fully resolves the requested exact computation of the least-core value and an attaining allocation.

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