Answer: \(\mathrm{P}\): blocking-coalition existence is decidable in \((L+\tau m^4)^{O(1)}\) bit operations.
Theorem 3 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateInStrictCore is co-NPC even when agents have separable lexicographic preferences over p ≥2 types.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given finite item-class sets \(Q_1,Q_2\), a finite set \(T\) of complete agent types, rational masses \(\mu_t\), type-specific endowments \(e_i(t)\), separable lexicographic rankings with common importance order \(1\triangleright2\), and a feasible current mass allocation \(a_{t,b}\) over integral bundles \(b\in Q_1\times Q_2\), decide whether there exists a positive-mass coalition represented by transfers \(z_{t,b,b'}\ge0\) with \(b'\succeq_t b\), \(z_{t,b,b'}\le a_{t,b}\), conservation of every participating item-class mass, and \(\sum_{t,b,b':\,b'\succ_t b}z_{t,b,b'}>0\).
Let \(Q_1,Q_2\) be finite nonempty item-class sets, \(B=Q_1\times Q_2\), and \(m=|Q_1|+|Q_2|\). Each agent consumes one item of each class category; items within a class are interchangeable.
A society is given by its support: the list \(T\) of \(\tau\) complete types with positive binary-rational masses \(\mu_t\), normalized by \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types.
Each type specifies an initial endowment \(e(t)=(e_1(t),e_2(t))\in B\) and strict linear rankings of each \(Q_i\), inducing separable lexicographic preferences \(\succ_t\) with common importance order \(1\triangleright2\); \(\succeq_t\) includes equality.
The input also gives nonnegative binary-rational current allocation masses \(a_{t,b}\), with \(\sum_b a_{t,b}=\mu_t\) and \(\sum_{t,b:b_i=q}a_{t,b}=\sum_{t:e_i(t)=q}\mu_t\) for every \(i\in\{1,2\}\) and \(q\in Q_i\).
A coalition selects portions of the mass currently receiving each bundle. Its reassignment is specified by nonnegative real masses \(z_{t,b,b'}\), permitted only when \(b'\succeq_t b\), with \(\sum_{b'}z_{t,b,b'}\le a_{t,b}\). Write \(c_t=\sum_{b,b'}z_{t,b,b'}\).
The coalition reallocates its initial endowments: for every \(i\in\{1,2\}\) and \(q\in Q_i\), require \(\sum_{t,b,b':b'_i=q}z_{t,b,b'}=\sum_{t:e_i(t)=q}c_t\). It blocks when \(\sum_{t,b,b':b'\succ_t b}z_{t,b,b'}>0\), which also ensures positive coalition mass.
Is deciding whether such a blocking coalition exists in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard? State running times in \(m\), \(\tau\), and the total input bit length \(L\).
For finite agents with distinct individually owned items, strict-core membership is \(\mathrm{coNP}\)-complete even with two categories and separable lexicographic preferences sharing \(1\triangleright2\); consequently, existence of a blocking coalition is \(\mathrm{NP}\)-complete. [Sikdar, Adalı, and Xia (2017)](https://sujoyksikdar.github.io/papers/core_multitype.pdf)
No result settling this exact mass-blocking decision problem was identified in the literature search.
Blocking-coalition existence is in \(\mathrm{P}\). An exact algorithm runs in \((L+\tau m^4)^{O(1)}\) bit operations.
In fact, the decision depends only on which current-allocation masses are positive, together with the endowments and preferences. The magnitudes of the positive masses do not affect the answer.
Write \(k=|B|=|Q_1||Q_2|\). Since \(|Q_1|+|Q_2|=m\), we have \(k\le m^2/4\).
Let
\(J=\{(t,b,b'):a_{t,b}>0,\ b'\succeq_t b\}\).
Introduce a nonnegative variable \(x_j\) for every \(j\in J\). These variables will first describe a reassignment direction, without imposing the allocation-capacity bounds.
For each \(j=(t,b,b')\), define
\(h_j=1\) if \(b'\succ_t b\), and \(h_j=0\) otherwise.
Define a matrix \(A\), whose rows are indexed by pairs \((i,q)\) with \(i\in\{1,2\}\) and \(q\in Q_i\), by
\(A_{(i,q),(t,b,b')}=\mathbf{1}[b'_i=q]-\mathbf{1}[e_i(t)=q]\).
Consequently, \(Ax=0\) says precisely that the reassignment consumes, in each item class, the amount contributed by the participating type masses.
Consider the following rational linear feasibility problem:
\(x_j\ge0\quad(j\in J),\qquad Ax=0,\qquad \sum_{j\in J}h_jx_j=1.\)
Every matrix coefficient belongs to \(\{-1,0,1\}\), and every right-hand side belongs to \(\{0,1\}\). In particular, the program has no strict inequalities.
We prove that this feasibility problem has a solution if and only if a blocking coalition exists.
Suppose \(z\) specifies a blocking coalition. If \(a_{t,b}=0\), nonnegativity and the capacity inequality imply \(z_{t,b,b'}=0\) for every \(b'\). Thus every nonzero permitted coordinate belongs to \(J\).
Let its strictly improved mass be
\(H=\sum_{j\in J}h_jz_j\).
By the definition of blocking, \(H>0\).
Set \(x_j=z_j/H\). Nonnegativity is preserved. The coalition’s resource equations give \(Az=0\), hence \(Ax=0\). Finally,
\(\sum_{j\in J}h_jx_j=H/H=1\).
Thus \(x\) satisfies the feasibility problem.
Conversely, suppose \(x\) satisfies the feasibility problem. For each current type-bundle pair, let
\(d_{t,b}=\sum_{b':(t,b,b')\in J}x_{t,b,b'}\),
with an empty sum interpreted as zero.
Because \(\sum_jh_jx_j=1\), at least one \(d_{t,b}\) is positive. Whenever \(d_{t,b}>0\), the definition of \(J\) ensures \(a_{t,b}>0\).
There are finitely many such pairs, so
\(\lambda=\min_{(t,b):d_{t,b}>0}a_{t,b}/d_{t,b}\)
is well-defined and strictly positive.
Set \(z_j=\lambda x_j\) for \(j\in J\), and set all other coordinates to zero. For every \((t,b)\),
\(\sum_{b'}z_{t,b,b'}=\lambda d_{t,b}\le a_{t,b}\):
this follows from the choice of \(\lambda\) when \(d_{t,b}>0\), and from nonnegativity when \(d_{t,b}=0\).
Every positive coordinate assigns a weakly preferred bundle. Also, \(Az=\lambda Ax=0\). Explicitly, if \(c_t=\sum_{b,b'}z_{t,b,b'}\), then for every \((i,q)\),
\(\sum_{t,b,b':b'_i=q}z_{t,b,b'}-\sum_{t:e_i(t)=q}c_t =\sum_{j\in J}A_{(i,q),j}z_j=0.\)
These are exactly the required resource equations. Finally, the strictly improved mass is
\(\sum_{j\in J}h_jz_j=\lambda\sum_{j\in J}h_jx_j=\lambda>0\).
Therefore \(z\) is a blocking coalition. This completes the equivalence.
For each type, preprocess its two rankings into rank functions \(r_{t,i}\), where a smaller rank means a better item. Then
\(b'\succeq_t b\ \Longleftrightarrow\ r_{t,1}(b'_1)<r_{t,1}(b_1) \ \text{or}\ \bigl(b'_1=b_1\ \text{and}\ r_{t,2}(b'_2)\le r_{t,2}(b_2)\bigr).\)
Thus weak and strict comparisons require a constant number of rank lookups.
Enumerating all candidate triples requires \(O(\tau k^2)\) comparisons. The feasibility problem has:
The equations have small integer coefficients. A dense encoding of their coefficient matrix uses \(O((m+1)N)\) entries. Including dimensions and indexing overhead, its binary encoding length is bounded by
\(S=O(\tau m^5\log(2\tau m))\).
The standard polynomial-time theorem for rational linear programming decides feasibility exactly in time polynomial in the binary encoding length. It applies here because all constraints are linear and rational; neither boundedness nor full dimensionality is required. [Khachiyan, *A polynomial algorithm in linear programming*](https://www.mathnet.ru/eng/dan42319).
Reading the original input and constructing this program therefore gives a total bound of
\((L+\tau m^4)^{O(1)}\)
bit operations: the displayed bound on \(S\) is itself polynomial in \(L+\tau m^4\).
Since the sets and supported types are explicitly supplied, this is also \(L^{O(1)}\). The algorithm enumerates only the supplied \(\tau\) types.
The strict-improvement requirement is handled exactly by normalization and scaling. No numerical tolerance or guessed improvement threshold is needed.
The cited finite-agent problem requires whole-agent participation and indivisible item reassignment. Its strict-core membership problem is \(\mathrm{coNP}\)-complete under the stated preference restrictions. [Sikdar, Adalı, and Xia, Theorem 3](https://sujoyksikdar.github.io/papers/core_multitype.pdf).
The present problem allows arbitrary portions of each current type-bundle mass to participate and to receive different bundles. That permission makes the scaling argument valid and yields an exact linear formulation. The finite-agent hardness theorem therefore does not settle this mass-blocking problem.
The target decision problem is polynomial-time solvable.
⟨structured verdict parsed — rendered above⟩
The prover resolves the assigned mass-blocking decision problem correctly. The equivalence is rigorous, and the stated polynomial bit-complexity bound is valid. No major or minor mathematical issues were found.
The set \(J\) includes exactly the weakly improving reassignment coordinates whose source allocation mass is positive. Excluding coordinates with \(a_{t,b}=0\) is justified: nonnegativity and the capacity constraint force every corresponding reassignment mass to vanish.
The indicator \(h_j\) correctly distinguishes strict improvement from equality. Strict linear bundle preferences make this distinction unambiguous.
Each column of \(A\) records the destination bundle’s consumption minus the participating type’s initial endowment. Consequently, after summing over reassignment coordinates, \(Ax=0\) expresses precisely the resource equations in USER_TASK.
In particular, the contribution term counts total participating type mass, rather than current consumption. This correctly follows the task’s endowment-based coalition definition.
For a blocking coalition, the strictly improved mass \(H\) is positive by definition. Every nonzero coordinate belongs to \(J\), so normalization by \(H\) preserves nonnegativity and the homogeneous resource equations and gives \(\sum_j h_jx_j=1\).
No capacity constraint is needed for this direction problem. Removing those constraints at this stage is justified by the converse scaling argument.
The normalization guarantees at least one positive \(d_{t,b}\). Every such pair has positive \(a_{t,b}\), by the definition of \(J\). Since the index set is finite and the coordinates of a feasible real vector are finite, the minimum defining \(\lambda\) exists and is strictly positive.
Scaling by \(\lambda\) satisfies every capacity bound. Pairs with \(d_{t,b}=0\) receive zero participating mass, including pairs excluded from \(J\).
The displayed expansion of \(Az=0\) correctly yields all required resource balances with the stated \(c_t\). Weak improvement holds coordinatewise, and strictly improved mass equals \(\lambda>0\). Thus every requirement for blocking is verified.
Arbitrarily small positive capacities cause no difficulty: the task requires positive improvement mass, without a fixed lower threshold.
The direction system uses allocation masses only through the condition \(a_{t,b}>0\). Their magnitudes enter solely into the positive scaling factor. The claimed support dependence therefore follows, for valid inputs with the same endowments and preferences.
The stated comparison formula exactly implements separable lexicographic preferences with common importance order \(1\triangleright2\). Strict rankings justify using item equality in the first category.
The bound \(k\le m^2/4\) is correct. Enumerating candidate triples takes \(O(\tau k^2)\) comparisons, and \(N\le\tau k^2=O(\tau m^4)\). Constantly many rank lookups per comparison need not mean constant bit cost; any indexing overhead remains within the claimed polynomial bit bound.
The invoked theorem is appropriately stated: feasibility of a finite rational linear system is decidable exactly in time polynomial in its binary encoding length, without boundedness or full dimensionality assumptions. This is the standard rational linear-programming result associated with [Khachiyan’s cited paper](https://www.mathnet.ru/eng/dan42319).
Its hypotheses hold here. All coefficients and right-hand sides are integers of constant bit length. Equality constraints and nonnegativity constraints are legitimate rational linear constraints. Redundant resource equations do not invalidate the theorem.
The dense encoding bound \(S=O(\tau m^5\log(2\tau m))\) is a valid upper bound, including the nonnegativity constraints through their variable-bound representation. It is polynomial in \(L+\tau m^4\), so the resulting running time \((L+\tau m^4)^{O(1)}\) bit operations follows.
Explicitly supplied class sets and supported rankings ensure that \(m\) and \(\tau\) are polynomially bounded by \(L\). The further conclusion \(L^{O(1)}\) is justified. The algorithm never enumerates unsupported possible types.
Singleton categories, absence of any strictly improving coordinate, and redundant or zero resource rows are all covered by the formulation. If every \(h_j=0\), normalization is infeasible, correctly ruling out blocking.
The finite-agent hardness statement matches [Sikdar, Adalı, and Xia, Theorem 3](https://sujoyksikdar.github.io/papers/core_multitype.pdf); its construction uses separable lexicographic preferences with common importance order. The prover correctly distinguishes whole-agent participation from divisible mass participation. That contextual theorem is not used to establish the continuous result.
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.