The Incompatibility of Strategy-Proofness and Representation in Party-Approval Multi-Winner Elections

In party-approval multi-winner elections, the goal is to allocate the seats of a fixed-size committee to parties based on approval ballots of the voters over the parties. In particular, each can approve multiple parties and each party can be assigned multiple seats.

Three central requirements in this settings are:

• Anonymity: The result is invariant under renaming the voters.
• Representation:Every sufficiently large group of voters with similar preferences is represented by some committee members.
• Strategy-proofness: No voter can benefit by misreporting her true preferences.

We show that these three basic axioms are incompatible for party-approval multi-winner voting rules, thus proving a far-reaching impossibility theorem.

The proof of this result is obtained by formulating the problem in propositional logic and then letting a SAT solver show that the formula is unsatisfiable. The DRUP proof output by the SAT solver is then converted into Lammich's GRAT format and imported into Isabelle/HOL with some custom-written ML code.

This transformation is proof-producing, so the final Isabelle/HOL theorem does not rely on any oracles or other trusted external trusted components.