| paper | Strategyproofness and Proportionality in Party-Approval Multiwinner Elections |
| authors | — |
| venue | AAAI 2023 |
| filed under | multiwinner · multiwinner |
| judged by | gpt-5.6-luna / xhigh (triple__luna__xhigh__c2r1) |
| judge confidence | high |
| authors would recognise it | yes |
The paper has no named theorem asserting an algorithmic or computational-complexity result, so it fails ChoCo’s objective computational gate. Its party-approval population mirror is natural and authors would likely recognise it, but the proposed questions are axiomatic feasibility or newly formulated manipulation questions rather than mirrors of qualifying computational results. SAT and Isabelle are proof technologies, not complexity results.
fails bit a — no named computational result to mirror
The paper contains no named computational-complexity result; SAT- and Isabelle-assisted axiomatic proofs cannot serve as the required computational anchor.
fatal: True
The proposed mirror covers the impossibility results in Theorems 1 and 2 and the Thiele-rule characterization in Theorem 3; it leaves Theorem 4 and the detailed SAT-verification results without a distinct computational mirror.
The strongest positive case is real, but it comes with an important qualification: this paper has no named theorem stating NP-hardness, membership in P, W[1]-hardness, or a comparable complexity classification. Its named results are axiomatic impossibilities and characterizations, proved partly with SAT. Thus, under ChoCo’s strict “named complexity result” gate, this paper has no qualifying anchor. If computer-aided impossibility results count as computational results in the broader sense, the following is the best mirror.
The natural regime is a large parliamentary or participatory electorate. There may be millions of voters but only a moderate number of parties, and many voters share exactly the same approval ballot because they belong to the same party coalition, demographic bloc, or issue-alignment group. A type is a nonempty approval set \(A\subseteq P\); \(\mu_A\) is the fraction of voters with that ballot. The outcome remains an integral multiset of \(k\) party seats—not a lottery or fractional seat vector—so this continuizes the population only.
My lead anchor is Theorem 2, proved in this paper: no party-approval rule simultaneously satisfies anonymity, weak proportional representation, and strategyproofness when \(k\ge 3\), \(m\ge4\), and \(2k\mid n\). Proposition 1 is the SAT-proved base case, and Lemma 1 supplies the induction to general parameters.
The corresponding continuous problem is:
Continuous Weak-Proportionality/Strategyproofness Feasibility. Given \(m\) parties and \(k\) seats, does there exist a resolute rule
\[
F:\Delta(2^P\setminus\{\varnothing\})\to\mathcal W_k
\]
where \(\mathcal W_k\) is the set of size-\(k\) party multisets, such that for every distribution \(\mu\):
\[
\mu'=\mu-\varepsilon e_A+\varepsilon e_B,
\]
we have
\[
F(\mu)(A)\ge F(\mu')(A),
\]
where \(F(\mu)(A)=\sum_{x\in A}F(\mu)(x)\).
A solution is an explicit rule \(F\); the objective is axiom feasibility.
The \(\varepsilon\)-deviation is the crucial modelling choice. It says that a positive mass of indistinguishable voters may jointly change their report. It is not an outcome-space relaxation: parties, seats, approval ballots, and utility are exactly those in the paper. It is also the exact high-multiplicity translation of a one-voter deviation: a profile with \(n_A\) voters of type \(A\) corresponds to \(\mu_A=n_A/n\), and changing one ballot transfers mass \(1/n\) from \(A\) to \(B\).
Under this definition, Theorem 2 transfers directly. If such an \(F\) existed, restrict it to distributions \(\mu_A=n_A/n\) arising from finite profiles. Since \(F\) sees only the histogram, it is anonymous; the mass threshold gives weak proportional representation; and the transfer of \(1/n\) gives ordinary strategyproofness. This contradicts Theorem 2. Lemma 1(1) strengthens the interpretation: the same contradiction survives arbitrarily large multiplicities by duplicating every voter type. I therefore expect this mirror to be a B-like transfer of the obstruction, rather than a continuum-specific tractable escape.
A second, independently useful anchor is Theorem 3, also proved here: CCAV is the only Thiele rule satisfying weak representation and strategyproofness for unrepresented voters for all \(k,m,n\).
Here the continuous problem can be stated as a genuine witness problem. Given \(m,k\), a non-increasing Thiele vector \(w\), a rational society \(\mu\), and a type \(A\) with \(F_w(\mu)(A)=0\), where
\[
F_w(\mu)\in\arg\max_{W\in\mathcal W_k}
\sum_{B}\mu_B\sum_{j=1}^{W(B)}w_j,
\]
decide whether there exist a report \(C\) and \(0<\varepsilon\le\mu_A\) such that, after transferring \(\varepsilon\) mass from \(A\) to \(C\), the new winning committee \(W'\) satisfies \(W'(A)>0\). A solution is either such a pair \((C,\varepsilon)\), or a proof that none exists.
The expected classification is exact: for CCAV, no witness exists; for every other Thiele rule, the counterexample constructed in Claim 2 of Theorem 3 becomes a rational distribution and a positive mass-transfer witness. The proof of CCAV’s positive side is expressed through linear coverage inequalities and should extend from voter counts to masses. Any computational hardness in actually finding the winning committee is likely to come from the party/committee structure—hence Class B-like—not from population multiplicity.
The weakest point is unavoidable. With literal atomless individual strategyproofness, a single voter has zero mass and cannot change \(\mu\); strategyproofness becomes vacuous. For example, assigning
\[
q_x=\lfloor k\mu_{\{x\}}\rfloor
\]
seats to each singleton-approved party and filling the remaining seats lexicographically satisfies weak proportionality, and is automatically strategyproof against null deviations. That gives a trivial Class-A-looking mirror, but it has lost the strategic content of the paper. The positive-mass formulation is therefore doing genuine work: it preserves the finite high-multiplicity dictionary, while making explicit that it is a cohort-level strengthening rather than literal unilateral manipulation in an atomless population.
So the honest conclusion is: the paper admits a very natural population mirror, especially for Theorem 2 and Theorem 3, and its impossibility structure survives under the faithful positive-mass interpretation. But if ChoCo requires a standard complexity theorem as the anchor, this paper should be marked out of scope despite having a strong continuous axiomatic analogue.
The strongest case against starts with ChoCo’s scope, not with the modelling. This paper has no qualifying computational anchor. Theorem 1, Theorem 2, Proposition 1, and Theorem 4 are axiomatic impossibility or failure results; Theorem 3 is an axiomatic characterization. SAT solving and Isabelle/HOL are proof technologies, not complexity results about an input problem. No theorem gives worst-case complexity, an algorithm, approximation guarantee, or parameterized classification.
That defeats the proposed mirror of Theorem 2 under the programme’s strict gate. The proposed question asks whether there exists a rule
\[ F:\Delta(2^P\setminus\{\varnothing\})\to\mathcal W_k \]
satisfying global axioms. But an arbitrary \(F\) is an infinite object, and “find an explicit rule” has no specified finite encoding or output model. If one restricts the domain to rational histograms with denominator \(n\), one has simply reconstructed the paper’s finite rule-existence problem and its SAT encoding. If one allows all distributions, one has an axiomatic mechanism-design question over an infinite domain, not a computational problem on a continuous society. The positive-mass deviation is a sensible strengthening, but it is group strategyproofness for cohorts, not literally unilateral manipulation by an atomless individual; it therefore defines a new axiom rather than supplying the missing computational anchor.
Theorem 3 is the closest escape. Given a distribution, a Thiele vector, and an unrepresented type, one can certainly ask whether some mass transfer makes that type represented. But that is a newly invented local manipulation problem, not the theorem’s characterization. The theorem says that CCAV is uniquely characterized among Thiele rules by two axioms uniformly over all \(k,m,n\); it does not assert the complexity of finding a manipulation, testing one, or computing a winner. If the rule class is unrestricted, the infinite-rule representation problem returns. If it is restricted to Thiele rules, the proposed problem is a weighted finite-election problem whose continuous formulation has not been supplied by the paper or supported by a named complexity result. The proponent’s “expected classification” is therefore a research idea, not a mirror of an established computational result.
There is no honest substantive objection based on multiplicity here. Party-approval elections have exactly the kind of natural high-multiplicity regime ChoCo wants: a large electorate, finitely many approval types, anonymous voters, and utilities determined entirely by the type’s approved parties. Mass is meaningful, and the integral committee outcome can remain unchanged. Existing high-multiplicity work would support, rather than undermine, this modelling choice.
So the negative case is strong only as a scope decision: this is an axiomatic social-choice paper with computational proof assistance, not a computational social-choice paper in ChoCo’s stated sense. It does not support the stronger universal claim that no worthwhile continuous mirror exists. If ChoCo admits axiomatic feasibility or newly derived manipulation problems, the party-approval setting is in fact a credible mirror; rejecting it then requires narrowing the programme’s remit, not identifying a fundamental failure of continuization.
The adversarial triple: the proponent anchors on up to three named results; the opponent sees that case and must defeat every anchor; the judge decides which case convinced it. These are the pipeline’s own outputs, generated by tools/triple_run.py — no human edited them. The paper’s own text is not reproduced here beyond the quoted statement above.