Answer: Distinguishing-coalition existence and equivalence are both in \(\mathrm{P}\). A rational distinguishing coalition can be computed in \(\ell\,\operatorname{poly}(\tau,k,L)+k\,\operatorname{poly}(\tau,\ell,L)\) bit time.
Theorem 4 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateThe problem of checking whether any two given vector weighted voting games are equivalent is co-NP- complete, even if all weights are equal to 0 or 1 (and hence the games are monotone).
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite set of types \(T\), rational masses \(\mu_t\) summing to \(1\), two rational quota vectors \(b,\hat b\), and type weight vectors \(a_t\in\{0,1\}^k\) and \(\hat a_t\in\{0,1\}^{\ell}\), decide whether the two games accept exactly the same mass coalitions \(x\) with \(0\le x_t\le\mu_t\). A coalition is accepted by the first game when \(\sum_t x_ta_t\ge b\), and by the second when \(\sum_t x_t\hat a_t\ge\hat b\), with inequalities interpreted coordinatewise; return a distinguishing \(x\) if one exists.
A society is given by its support: a nonempty list \(T\) of \(\tau\) 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.
The input also gives positive integers \(k,\ell\), weights \(a_t\in\{0,1\}^k\), \(\hat a_t\in\{0,1\}^{\ell}\), and binary rational quotas \(b\in\mathbb Q^k\), \(\hat b\in\mathbb Q^{\ell}\), with no sign restrictions on quotas. Let \(m=k+\ell\) and let \(L\) be the total input bit length.
A mass coalition is any real vector \(x\in\prod_{t\in T}[0,\mu_t]\); its total mass need not equal one. The first game accepts it exactly when \(\sum_{t\in T}x_ta_t\ge b\), and the second exactly when \(\sum_{t\in T}x_t\hat a_t\ge\hat b\), coordinatewise. Equality meets a quota; rejection means a strict failure in at least one coordinate.
The equivalence problem asks whether both games accept exactly the same mass coalitions, and requests a rational distinguishing coalition when they differ.
Is deciding whether a distinguishing mass coalition exists in P or NP-hard, with running times stated in \(m,\tau,L,k,\ell\)?
For finite indivisible voters, equivalence is coNP-complete, and existence of a distinguishing coalition is NP-complete, even with binary weights; equivalence is polynomial-time solvable when both dimensions are fixed and weights are binary. [Source](https://cdn.aaai.org/AAAI/2008/AAAI08-011.pdf)
No result settling this exact mass-coalition problem was identified in the literature search.
Existence of a distinguishing mass coalition is in \(\mathrm{P}\), and equivalence is also in \(\mathrm{P}\). A rational distinguishing coalition can be computed in polynomial time whenever one exists. Neither dimension needs to be fixed.
More precisely, the algorithm uses at most:
Its bit running time is \(\ell\,\operatorname{poly}(\tau,k,L)+k\,\operatorname{poly}(\tau,\ell,L)\), hence \(m\,\operatorname{poly}(\tau,m,L)\) and therefore polynomial in \(L\).
Enumerate the support as \(T=\{1,\ldots,\tau\}\). Define matrices \(A\in\{0,1\}^{k\times\tau}\) and \(\widehat A\in\{0,1\}^{\ell\times\tau}\) by \(A_{it}=(a_t)_i\) and \(\widehat A_{jt}=(\hat a_t)_j\). Write \(\mu=(\mu_1,\ldots,\mu_\tau)\).
The two acceptance sets are
\(P=\{x\in\mathbb R^\tau:0\le x\le\mu,\ Ax\ge b\}\),
\(Q=\{x\in\mathbb R^\tau:0\le x\le\mu,\ \widehat A x\ge\hat b\}\).
These are closed subsets of the compact box \(\prod_t[0,\mu_t]\), so they are compact whenever nonempty. A distinguishing coalition exists exactly when \(P\ne Q\).
Nonnegativity of the weights gives a simple emptiness test:
\(P\ne\varnothing\quad\Longleftrightarrow\quad A\mu\ge b\).
Indeed, if \(x\in P\), then \(x\le\mu\) and \(A\) has nonnegative entries, so \(A\mu\ge Ax\ge b\). Conversely, if \(A\mu\ge b\), then \(\mu\in P\). The same argument applies to \(Q\).
Consequently:
These conclusions hold for arbitrary signed quotas.
Assume now that \(P\) and \(Q\) are nonempty.
For each \(j\in\{1,\ldots,\ell\}\), compute
\(\displaystyle \alpha_j=\min\{\widehat A_{j\cdot}x:0\le x\le\mu,\ Ax\ge b\}\).
This is a linear program over \(P\). Its minimum is attained because \(P\) is nonempty and compact.
Claim. There is a coalition accepted by the first game and rejected by the second if and only if \(\alpha_j<\hat b_j\) for some \(j\).
Proof. If \(x\in P\setminus Q\), then some second-game coordinate fails strictly: \(\widehat A_{j\cdot}x<\hat b_j\). Therefore \(\alpha_j\le\widehat A_{j\cdot}x<\hat b_j\).
Conversely, if \(\alpha_j<\hat b_j\), any minimizing coalition \(x^{(j)}\in P\) satisfies \(\widehat A_{j\cdot}x^{(j)}=\alpha_j<\hat b_j\). It is accepted by the first game and rejected by the second. \(\square\)
Likewise, for each \(i\in\{1,\ldots,k\}\), compute
\(\displaystyle \beta_i=\min\{A_{i\cdot}x:0\le x\le\mu,\ \widehat A x\ge\hat b\}\).
The same proof shows that a coalition in \(Q\setminus P\) exists exactly when \(\beta_i<b_i\) for some \(i\).
Thus, when both acceptance sets are nonempty,
\(P=Q\quad\Longleftrightarrow\quad (\alpha_j\ge\hat b_j\text{ for every }j) \text{ and } (\beta_i\ge b_i\text{ for every }i)\).
This handles the boundary convention exactly: a minimum equal to a quota does not establish rejection.
The algorithm first performs the emptiness tests above. If both acceptance sets are nonempty, it solves the directional linear programs, stopping and returning an optimizer whenever a strict quota violation is found. If every comparison passes, it reports equivalence.
We use the standard exact rational linear-programming theorem: a linear program with rational coefficients can be solved in time polynomial in its binary encoding length; when a finite optimum is attained, an optimal rational solution can be returned. Polynomial bit complexity and exact LP algorithms are discussed in [Dadush, Huiberts, Natura, and Végh](https://link.springer.com/article/10.1007/s10107-023-01956-2).
All hypotheses hold here:
In particular, the algorithm compares rational optimum values with rational quotas exactly. It does not replace strict rejection by a chosen numerical tolerance.
For a more explicit running-time statement, let \(p(n,r,B)\) be a polynomial upper bound for an exact LP routine on \(n\) variables, \(r\) inequalities, and total encoding length \(B\). In a dense representation, the box constraints add at most \(O(\tau^2)\) bits, so each LP has encoding length at most \(B_0=O(L+\tau^2)\). The total time is bounded by
\(O\!\left(\operatorname{poly}(L) +\ell\,p(\tau,k+2\tau,B_0) +k\,p(\tau,\ell+2\tau,B_0)\right)\).
This gives the bounds stated above. Since the explicit input contains all \(\tau\) weight vectors of length \(m=k+\ell\), both \(m\) and \(\tau\) are bounded by \(L\). Hence the algorithm is polynomial in total input bit length, even when all parameters vary.
Exact LP already supplies a polynomial-size rational witness. We can also prove a concrete existence bound:
Whenever the games differ, there is a distinguishing rational coalition with total encoding length
\(O\!\left(\tau\bigl(L+\tau\log(\tau+1)\bigr)\right)\).
The witness \(\mu\) in the empty-set cases already satisfies this bound. Consider a directional LP whose optimum strictly violates a quota.
There is an optimal vertex \(v\) of its feasible polytope. To justify this even for a lower-dimensional polytope, start with the compact set of optimizers and successively minimize its first, second, and remaining coordinates. The final set is a singleton \(\{v\}\). If \(v\) were a nontrivial convex combination of two feasible points, optimality would force both points into the optimizer set; the successive coordinate minima would then force both to equal \(v\). Thus \(v\) is a vertex.
At a vertex, the normals of active constraints span \(\mathbb R^\tau\). Otherwise, a nonzero direction orthogonal to all active normals would allow sufficiently small movements in both signs: active constraints remain equalities, and the finitely many inactive constraints remain satisfied because they have positive slack. This would contradict the vertex property.
Choose \(\tau\) linearly independent active constraints. Written as equalities, they form
\(Mv=r\),
where \(M\in\{0,1\}^{\tau\times\tau}\) is nonsingular. Its rows are game-weight rows or unit vectors from active box bounds. Each entry of \(r\) is zero, a mass, or an active quota. Moreover, \(0\le r_s\le1\): an active game quota equals a binary-weighted sum of coordinates, which is at most \(\sum_t\mu_t=1\).
Let \(D\) be the product of the positive denominators of all input masses and quotas. Then \(Dr\) is integral and \(\log_2D\le L\). By Cramer’s rule,
\(\displaystyle v_t=\frac{\det M_t(Dr)}{D\det M}\),
where \(M_t(Dr)\) replaces column \(t\) of \(M\) by \(Dr\).
Hadamard’s inequality gives \(|\det M|\le\tau^{\tau/2}\). The replaced column has Euclidean norm at most \(D\sqrt{\tau}\), and every other column has norm at most \(\sqrt{\tau}\), so
\(|\det M_t(Dr)|\le D\tau^{\tau/2}\).
Thus each coordinate has a rational representation using \(O(L+\tau\log(\tau+1))\) bits. Since \(v\) is optimal for the directional LP, it retains the strict quota violation and is a distinguishing witness.
The [cited finite-voter paper](https://cdn.aaai.org/AAAI/2008/AAAI08-011.pdf) represents coalitions by vectors in \(\{0,1\}^n\). Here, each mass coordinate varies throughout an interval. Each directional test is therefore ordinary rational linear programming, which settles this mass-coalition problem in polynomial time.
⟨structured verdict parsed — rendered above⟩
Verdict: proved. The output resolves the stated mass-coalition problem. Both existence of a distinguishing coalition and equivalence are decidable in polynomial bit time, and the algorithm returns a rational distinguishing coalition whenever one exists. I found no mathematical errors or substantive gaps.
The definitions of \(P\) and \(Q\) exactly match the task. In particular, neither definition imposes a total-mass equality.
Both sets are intersections of finitely many closed halfspaces with the compact box \(\prod_t[0,\mu_t]\). Thus they are compact when nonempty. A distinguishing coalition exists precisely when \(P\ne Q\).
The emptiness equivalence
\[
P\ne\varnothing\quad\Longleftrightarrow\quad A\mu\ge b
\]
is correct. Nonnegative matrix entries imply \(Ax\le A\mu\) for every admissible \(x\), and \(\mu\) itself is admissible. The same reasoning applies to \(Q\).
All three branches of the emptiness test are valid:
Negative, zero, and unattainably large quotas cause no exception to this reasoning.
For each second-game coordinate, the minimization defining \(\alpha_j\) has a continuous linear objective on the nonempty compact set \(P\). Its minimum therefore exists and is attained.
Both implications in the directional claim are correct. A point in \(P\setminus Q\) strictly violates at least one second-game quota, so the corresponding minimum is strictly below that quota. Conversely, an optimizer whose objective value is strictly below that quota belongs to \(P\setminus Q\).
The reverse-direction argument for \(\beta_i\) is identical in structure and valid.
Consequently, the stated collection of comparisons is equivalent to both inclusions \(P\subseteq Q\) and \(Q\subseteq P\). Equality of an optimum and its quota correctly counts as acceptance. No replacement of strict rejection by a non-strict inequality occurs.
The invoked theorem is stated sufficiently precisely for this application: rational LPs can be solved in time polynomial in binary encoding length, with an exact rational optimizer returned when a finite optimum is attained.
The cited article discusses polynomial LP algorithms in the bit-complexity model in its introduction. Its specialized interior-point algorithm is not needed for the prover’s argument; the output invokes the general rational-LP theorem. [Dadush, Huiberts, Natura, and Végh](https://link.springer.com/article/10.1007/s10107-023-01956-2).
Every required hypothesis is satisfied:
An exact rational optimizer gives an exact rational objective value, so comparison with a rational quota is valid even when the strict violation is very small.
The constraint counts are correct. A forward LP has \(k\) game inequalities and \(2\tau\) box inequalities; a reverse LP has \(\ell\) game inequalities and \(2\tau\) box inequalities. The maximum number of LP calls is respectively \(\ell\) and \(k\).
The encoding estimate \(B_0=O(L+\tau^2)\) is valid for the stated dense representation. The game matrix, rational right-hand sides, and objective coefficients come from the explicit input. Writing the box rows densely adds \(O(\tau^2)\) constant-size entries.
The emptiness tests use polynomial-time rational arithmetic. The displayed total-time bound therefore follows from the exact LP theorem:
\[
O\!\left(\operatorname{poly}(L)
+\ell\,p(\tau,k+2\tau,B_0)
+k\,p(\tau,\ell+2\tau,B_0)\right).
\]
Since the input explicitly contains \(\tau\) weight vectors of length \(m\), and \(k,\ell,\tau\) are positive, both \(m\) and \(\tau\) are bounded by \(L\). The claimed polynomial dependence on total input length is justified.
The additional witness-size argument is correct.
The optimizer set is nonempty, compact, and convex. Successive coordinate minimizations retain these properties and eventually fix every coordinate, producing a singleton. The stated convex-combination argument correctly establishes that its point is a vertex of the original feasible polytope, including when that polytope is lower-dimensional.
The active-normal spanning argument is valid. If their span were proper, a nonzero orthogonal direction would preserve all active equalities. Finitely many inactive inequalities with positive slack allow sufficiently small movements in both directions, contradicting extremality.
The resulting nonsingular matrix \(M\) can indeed have binary entries: game equalities use binary weight rows, while either active box bound can be written using a positive unit row. Its right-hand side consists of zeros, masses, and active game quotas.
The assertion \(0\le r_s\le1\) is valid even though input quotas may be signed. An active game quota equals a nonnegative binary-weighted coordinate sum bounded by \(\sum_t\mu_t=1\). Negative quotas cannot be active.
The product \(D\) of input denominators clears every selected right-hand side, and \(\log_2D\le L\). Cramer’s rule is applied correctly:
\[
v_t=\frac{\det M_t(Dr)}{D\det M}.
\]
The column-norm bounds used in Hadamard’s inequality yield exactly the stated determinant bounds. They also cover \(\tau=1\). Numerator and denominator lengths consequently give the claimed total witness encoding bound
\[
O\!\left(\tau\bigl(L+\tau\log(\tau+1)\bigr)\right).
\]
Because the vertex remains optimal, it retains the strict quota violation.
The finite-voter paper explicitly represents coalitions by binary incidence vectors. The output’s comparison with interval-valued mass coordinates is accurate. [On the Dimensionality of Voting Games](https://cdn.aaai.org/AAAI/2008/AAAI08-011.pdf).
The proof establishes polynomial-time solvability for arbitrary varying dimensions under the task’s explicit rational encoding. No additional mathematical clarification 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.