Answer: Polynomial-time solvable: the decision problem is in \(\mathrm{P}\).
Theorem 5 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateMaximising social welfare is NP-complete even for 1-lists.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite type set \(T\), rational masses \(\mu_t\) summing to \(1\), and for each type \(t\) either no approved coalition profile or one integral profile \(a^t\in\mathbb{Z}_{\ge 0}^{T}\) with \(a^t_t\ge 1\), choose nonnegative masses \(x_q\) of coalitions with integral type-count vectors \(q\). Require \(\sum_q q_t x_q=\mu_t\) for every \(t\), and maximize the mass of agents in approved coalitions, \(\sum_q x_q\sum_{t:a^t=q}q_t\).
A society is given by its support: a nonempty list \(T\) of \(\tau\) types with positive binary rational masses \(\mu_t\) satisfying \(\sum_{t\in T}\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types.
Each type \(t\) approves either no coalition profile or exactly one profile \(a^t\in\mathbb{Z}_{\ge0}^{T}\), with \(a^t_t\ge1\); all profile coordinates are binary encoded. A type approves a coalition precisely when its profile equals its listed profile, and receives utility \(1\) if it approves and \(0\) otherwise.
Allowed coalition profiles are all \(q\in\mathbb{Z}_{\ge0}^{T}\setminus\{0\}\), including singleton profiles, with no imposed upper size bound. An allocation consists of finitely supported nonnegative real coalition masses \(x_q\) satisfying \(\sum_q q_t x_q=\mu_t\) for every \(t\).
Its welfare is \(W(x)=\sum_q x_q\sum_{t:\,a^t\text{ is listed and }a^t=q}q_t\). The input additionally contains a binary rational threshold \(B\in[0,1]\).
Let \(m=\max(\{1\}\cup\{\sum_t a^s_t:a^s\text{ is listed}\})\), and let \(L\) be the total binary input length. Running times are measured in \(m,\tau,L\), with polynomial time meaning polynomial in the binary input length \(L\).
Is deciding whether a feasible allocation \(x\) satisfies \(W(x)\ge B\) in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard?
For a finite society where each agent explicitly lists at most one approved coalition, deciding whether a partition satisfies at least a given number of agents is \(\mathrm{NP}\)-complete.
The decision problem is in \(\mathrm{P}\), with running time polynomial in the binary input length \(L\). The unbounded set of allowed profiles can be replaced by a linear feasibility problem with at most \(\tau\) variables.
Let \(\mathcal A=\{p^1,\ldots,p^k\}\) be the set of distinct listed approval profiles. Since each type lists at most one profile, \(k\le\tau\).
For every allowed profile \(q\), define its welfare coefficient by
\[ w(q)=\sum_{t:\,a^t\text{ is listed and }a^t=q}q_t. \]
Thus \(w(q)=0\) whenever \(q\notin\mathcal A\). For each \(j\), let \(c_j=w(p^j)\). These coefficients are computed directly from the input, grouping types that list the same profile.
Consider the following rational linear feasibility problem, with variables \(y_1,\ldots,y_k\):
\[ y_j\ge0\quad\text{for every }j, \]
\[ \sum_{j=1}^k p^j_t y_j\le\mu_t \quad\text{for every }t\in T, \]
\[ \sum_{j=1}^k c_jy_j\ge B. \]
We prove that this system is feasible exactly when the requested allocation exists.
Suppose \(x\) is a feasible allocation with \(W(x)\ge B\). Set \(y_j=x_{p^j}\).
For every type \(t\), nonnegativity of all coalition masses gives
\[ \sum_{j=1}^k p^j_t y_j \le \sum_q q_tx_q =\mu_t. \]
Moreover, profiles outside \(\mathcal A\) have zero welfare coefficient. Consequently,
\[ \sum_{j=1}^k c_jy_j =\sum_q w(q)x_q =W(x) \ge B. \]
Hence \(y\) satisfies the linear system.
Conversely, suppose \(y\) satisfies the system. For every type \(t\), define its residual mass by
\[ r_t=\mu_t-\sum_{j=1}^k p^j_ty_j\ge0. \]
Let \(e_t\) be the singleton profile containing one member of type \(t\) and no members of other types. Construct an allocation by assigning mass \(y_j\) to profile \(p^j\) and mass \(r_t\) to profile \(e_t\). If a profile occurs in both assignments, add the assigned masses.
Every assigned profile is allowed: each listed profile is nonzero because its approving type has a positive coordinate, and singleton profiles are expressly allowed. The allocation has support size at most \(k+\tau\le2\tau\).
For every type \(t\), its total allocated mass is
\[ \sum_q q_tx_q =\sum_{j=1}^k p^j_ty_j+r_t =\mu_t. \]
Thus the allocation is feasible. Its welfare satisfies
\[ W(x) =\sum_{j=1}^k c_jy_j+\sum_{t\in T}w(e_t)r_t \ge\sum_{j=1}^k c_jy_j \ge B, \]
because every singleton welfare coefficient is nonnegative. This calculation also handles approved singleton profiles correctly.
The two directions establish the required equivalence. If \(k=0\), all welfare is zero, so the answer is yes exactly when \(B=0\); singleton coalitions still give a feasible allocation.
The system has \(k\le\tau\) variables and \(k+\tau+1\le2\tau+1\) inequalities.
Every profile coordinate is at most \(m\). Also,
\[ 0<c_j\le\sum_{t\in T}p^j_t\le m, \]
since \(c_j\) sums a subset of the profile coordinates. Thus every integer coefficient requires \(O(\log(m+1))\) bits. The rational right-hand sides are the input masses and threshold.
The system therefore has encoding length
\[ O\!\left(\tau^2\log(m+1)+L\right). \]
Both \(\tau\) and \(\log(m+1)\) are polynomially bounded in \(L\): the support is explicitly listed, and \(m\) is a sum of at most \(\tau\) binary-encoded coordinates from one input profile, or equals one. Grouping identical profiles and computing the coefficients also take polynomial time.
The rational linear programming theorem states that feasibility of an explicitly encoded finite system of rational linear inequalities can be decided exactly in time polynomial in its total binary encoding length. Its hypotheses apply here: all coefficients are rational, and the entire system has polynomial encoding length. See [Khachiyan, *A polynomial algorithm in linear programming*](https://www.mathnet.ru/eng/dan42319).
Consequently, the algorithm runs in time polynomial in \(L\), without enumerating profiles up to size \(m\).
A finite partition must select whole coalitions of indivisible agents. Here the coalition masses are arbitrary nonnegative real numbers, and each type’s mass may be split among several profiles. The resulting constraints are linear inequalities without integrality requirements. Singleton profiles complete every feasible partial assignment.
Therefore, the stated finite-society \(\mathrm{NP}\)-completeness result does not establish hardness for this continuous allocation problem.
⟨structured verdict parsed — rendered above⟩
The prover resolves the intended existence question correctly: the continuous allocation problem is in \(\mathrm{P}\). No major or minor mathematical issues were found.
The set \(\mathcal A\) contains every distinct listed approval profile. Since each of the \(\tau\) types lists at most one profile, \(k\le\tau\). By the definition of approval, every profile outside \(\mathcal A\) has welfare coefficient zero. Grouping identical profiles and summing their approving coordinates computes each \(c_j\) correctly.
The variables represent nonnegative masses assigned to listed profiles. Each resource inequality limits consumption of type \(t\) to its available mass \(\mu_t\). The final inequality requires those assignments to contribute welfare at least \(B\). All coefficients and right-hand sides are explicitly specified rational numbers.
Setting \(y_j=x_{p^j}\) preserves nonnegativity. Dropping the remaining nonnegative resource-consumption terms gives the stated resource inequalities. Dropping profiles outside \(\mathcal A\) does not change welfare, because their welfare coefficients vanish. Thus this direction is valid, including the exact threshold case \(W(x)=B\).
Each residual \(r_t\) is nonnegative by the corresponding resource inequality. All listed profiles are nonzero by the approval-coordinate assumption, and all singleton profiles are allowed.
Adding the assigned masses when profiles coincide makes the construction well-defined. Each singleton contributes its residual only to its own type, so the displayed resource equality is correct. The resulting allocation has finite support of size at most \(k+\tau\).
Welfare is linear in profile masses. Consequently, the displayed welfare identity remains valid even when an approved profile is also a singleton: the initial assignment and residual assignment are additive contributions to that profile’s total mass. Since singleton welfare coefficients are nonnegative, the threshold is preserved.
The case \(k=0\) is handled correctly: welfare is always zero, and singleton allocations establish feasibility, so the answer is yes exactly when \(B=0\). The argument also covers \(\tau=1\), zero profile coordinates, approved singletons, and thresholds \(B=0\) and \(B=1\). No upper bound on allowed coalition size is needed.
Every coordinate of a listed profile is at most its total size, hence at most \(m\). Each distinct listed profile has at least one approving type whose coordinate is positive, establishing \(c_j>0\). Since \(c_j\) sums a subset of the profile’s coordinates, \(c_j\le m\).
The inequality count \(k+\tau+1\) is correct, including nonnegativity constraints. The stated encoding bound is valid. Explicit listing bounds \(\tau\) polynomially in \(L\), and summing at most \(\tau\) binary-encoded coordinates gives a polynomial bound on \(\log(m+1)\). Grouping profiles and performing the required integer arithmetic therefore take polynomial time in \(L\).
The prover states the applicable theorem precisely: feasibility of an explicitly encoded rational linear inequality system is decidable exactly in time polynomial in its binary encoding length. Its hypotheses are satisfied here. The cited [Khachiyan paper](https://www.mathnet.ru/eng/dan42319) establishes polynomial-time linear feasibility; the rational-coefficient formulation is the standard version of that result. No strict-feasibility, integrality, or numerical approximation assumption is introduced.
The explanation correctly distinguishes indivisible-agent partitions from allocations with real coalition masses. The finite-society hardness statement does not invalidate the demonstrated polynomial-time reduction.
Repair feedback: None required. The reduction, completion construction, and binary complexity analysis establish the claimed result.
⟨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.