← back to the atlas

d4-conf-sagt-2009-0026 (d4-conf-sagt-2009-0026)

Answer: \(\mathrm{P}\)

The anchor (named result in the paper)

Theorem 4.1 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateThe problems {\sc Super-Imputation-Sta\-bi\-li\-ty-WVG} and {\sc CoS-WVG} are $\conp$-com\-plete.

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

The continuous mirror question, as graded

Given finitely many types \(T\) with rational masses \(\mu_t>0\), \(\sum_{t\in T}\mu_t=1\), rational per-member weights \(a_t\ge 0\), quota \(0\le q\le\sum_{t\in T}\mu_t a_t\), and subsidy bound \(\Delta\ge 0\), does there exist a nonnegative per-member payoff \(p_t\) for each type such that \(\sum_{t\in T}\mu_t p_t\le 1+\Delta\) and \(\sum_{t\in T}p_t x_t\ge 1\) for every winning mass vector \(x\) with \(0\le x_t\le\mu_t\) and \(\sum_{t\in T}a_t x_t\ge q\)?

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

A society is given by its support: a nonempty list \(T\) of \(\tau=|T|\) types with positive binary rational masses \(\mu_t\), where \(\sum_{t\in T}\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types. Each type has a binary rational per-member weight \(a_t\ge0\); the quota and subsidy bound are binary rationals satisfying \(0<q\le\sum_{t\in T}\mu_t a_t\) and \(\Delta\ge0\). Let \(L\) be the total input bit length; state running times in \(\tau\) and \(L\) (there is no separate candidate parameter \(m\)).
A coalition is any real mass vector \(x\) satisfying \(0\le x_t\le\mu_t\); it has value \(1\) when \(\sum_{t\in T}a_t x_t\ge q\), and value \(0\) otherwise. Thus equality at the quota wins, the empty coalition loses, and the whole society wins.
A payoff assigns a finite real per-member amount \(p_t\ge0\) uniformly within each type. The decision problem asks whether there exists such a payoff with \(\sum_{t\in T}\mu_t p_t\le1+\Delta\) and \(\sum_{t\in T}p_t x_t\ge1\) for every winning coalition \(x\).

Is this continuous subsidy-feasibility decision problem in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard?

For finite weighted voting games, deciding whether the cost of stabilizing the grand coalition is at most a given subsidy is \(\mathrm{coNP}\)-complete for binary integer weights and quota, and polynomial-time solvable for unary weights ([source](https://arxiv.org/html/0907.4385)).
No result settling exactly the continuous decision problem above was located in the literature search.

Modeling choices made when packaging the task

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

Result

The continuous subsidy-feasibility problem is in \(\mathrm{P}\). In fact, its optimal subsidy has an explicit formula.

Define the total weight
\(W=\sum_{t\in T}\mu_t a_t\).
By hypothesis, \(0<q\le W\). The minimum total payoff satisfying all winning-coalition constraints is exactly \(W/q\). Consequently, the instance is feasible if and only if
\[ W\le q(1+\Delta), \]
and the minimum subsidy is \(\Delta_{\min}=W/q-1\).

Proof of the exact optimum

For a payoff vector \(p\), write its total payment as
\(C(p)=\sum_{t\in T}\mu_t p_t\).

Lower bound. Suppose \(p\) satisfies every winning-coalition constraint. Consider the coalition
\(x_t^*=(q/W)\mu_t\) for every \(t\in T\).

Since \(0<q/W\le1\), each coordinate satisfies \(0\le x_t^*\le\mu_t\), so this is an admissible coalition. Its weight is
\[ \sum_{t\in T}a_t x_t^* =\frac qW\sum_{t\in T}a_t\mu_t =q. \]
Equality at the quota wins, so the payoff constraint for this coalition gives
\[ 1\le\sum_{t\in T}p_t x_t^* =\frac qW C(p). \]
Multiplying by the positive number \(W/q\) yields \(C(p)\ge W/q\).

Attainment. Define \(p_t^*=a_t/q\) for every \(t\in T\). These per-member payoffs are finite and nonnegative because \(q>0\) and \(a_t\ge0\). For any winning coalition \(x\),
\[ \sum_{t\in T}p_t^*x_t =\frac1q\sum_{t\in T}a_tx_t \ge1. \]
Thus \(p^*\) satisfies every required constraint, and its total payment is
\[ C(p^*)=\sum_{t\in T}\mu_t\frac{a_t}{q} =\frac Wq. \]

The lower bound is therefore attained. A payoff within the prescribed budget exists exactly when \(W/q\le1+\Delta\), equivalently \(W\le q(1+\Delta)\). Since \(W\ge q\), the stated minimum subsidy is nonnegative.

Exact algorithm and running time

Compute \(W\) using rational arithmetic, then test \(W\le q(1+\Delta)\). If the answer is yes, the formula \(p_t^*=a_t/q\) supplies an explicit feasible payoff.

For completeness, all arithmetic can be performed with polynomially bounded integer lengths. Write each product \(\mu_ta_t\) as \(n_t/d_t\), with a positive denominator, without requiring reduction. The common denominator \(H=\prod_{t\in T}d_t\) has bit length \(O(L)\), because the sum of the input denominator lengths is at most \(L\). The corresponding numerator of \(W\) also has bit length \(O(L)\): indeed, \(\sum_t\mu_t=1\) and nonnegative weights imply \(W\le\max_t a_t\), whose bit length is bounded by the input length. The same bounds hold for intermediate partial sums.

Writing \(W=N/H\), \(q=Q/R\), and \(\Delta=D/S\), with positive denominators, the decision is the integer comparison
\[ NRS\le HQ(S+D). \]
Every integer here has bit length \(O(L)\). Using elementary integer multiplication, sequential rational summation and this comparison take \(O(\tau L^2)\) bit operations. This proves membership in \(\mathrm{P}\) in the requested parameters.

Why the discrete hardness does not transfer

The cited finite-game hardness theorem concerns coalitions consisting of subsets of indivisible players. [Theorem 4.1 of *The Cost of Stability in Coalitional Games*](https://arxiv.org/html/0907.4385).

The decisive coalition here takes the fraction \(q/W\) of every supported type. Such a coalition is always admissible in the continuous model, whereas a corresponding subset need not exist in a finite game. This continuous coalition forces the lower bound that the proportional payoff attains.

⟨structured verdict parsed — rendered above⟩

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

Verdict

The proof is correct and resolves the assigned problem. The continuous decision problem is in \(\mathrm{P}\), and the stated exact optimum and running-time bound are justified. No major or minor mathematical issues were found.

Step-by-step verification

The definition \(W=\sum_{t\in T}\mu_ta_t\) matches the task. The assumptions \(0<q\le W\) ensure \(W>0\), so every division by \(W\) or \(q\) is valid.

The proposed coordinates \(x_t^*=(q/W)\mu_t\) satisfy \(0\le x_t^*\le\mu_t\), because \(0<q/W\le1\). The model permits arbitrary real mass coordinates, so this coalition is admissible without any integrality or representation restriction.

The computation \(\sum_ta_tx_t^*=q\) is exact. Equality wins under the task’s explicit convention. Consequently, every feasible payoff satisfies \(1\le(q/W)C(p)\), and multiplication by \(W/q>0\) correctly gives \(C(p)\ge W/q\). This reasoning applies to every allowable real payoff vector.

The vector \(p_t^*=a_t/q\) has finite, nonnegative coordinates. For every winning coalition, its payment is \((\sum_ta_tx_t)/q\ge1\). Its total payment is exactly \(W/q\). Thus the argument establishes an attained minimum, rather than merely an infimum.

Necessity follows from the lower bound; sufficiency follows from the exhibited payoff. Hence feasibility is equivalent to \(W/q\le1+\Delta\), and then to \(W\le q(1+\Delta)\). Since \(W/q\ge1\), the minimum subsidy \(W/q-1\) is nonnegative.

The proof covers zero-weight types, a single supported type, \(q=W\), and \(\Delta=0\). Zero-weight types receive zero under the proposed payoff. When \(q=W\), the lower-bound coalition is the whole society and the optimum is \(1\). No excluded case is used.

The unreduced denominator of each product \(\mu_ta_t\) has length bounded by the combined lengths of its input denominators. Therefore \(H=\prod_td_t\) has bit length \(O(L)\). The bound \(W\le\max_ta_t\), together with this denominator bound, justifies an \(O(L)\)-bit numerator. Nonnegative partial sums satisfy the same value bound and have denominators with \(O(L)\) bits.

The cross-multiplied comparison \(NRS\le HQ(S+D)\) is correct because all denominators are positive. Every operand and product has \(O(L)\) bits.

Sequential unreduced rational summation requires \(O(\tau)\) arithmetic operations on integers of \(O(L)\) bits. Elementary multiplication therefore supports the claimed \(O(\tau L^2)\) bit-operation bound, including the final comparison. The explicit payoff coordinates also have polynomial-size rational representations. The complexity statement uses precisely the requested parameters.

The cited paper defines coalitions as subsets of finitely many players; Theorem 4.1 establishes the stated binary-encoding hardness in that setting. The prover correctly treats this as contextual information, with no application of that theorem to the continuous model. Its observation that the fractional coalition need not correspond to a discrete subset is valid. [Source: definitions and Theorem 4.1](https://arxiv.org/html/0907.4385).

Repair feedback

No additional lemma, clarification, or correction 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.