The Impossibility of Strategyproof Rank Aggregation

In Social Choice Theory, a social welfare function (SWF) is a function that takes a collection of individual preferences on some set of alternatives and returns an aggregated preference relation.

More formally: Consider finite sets of agents $N=\{1,\ldots,n\}$ and alternatives $A=\{x_1,\ldots,x_m\}$. The input of an SWF is an $n$-tuple of rankings (i.e. linear orders) of $A$, and its output is a ranking of $A$ as well.

Various desirable properties on SWFs can be defined:

• Anonymity: The SWF is invariant under permutation of the agents.
• Unanimity: If all voters prefer $x$ over $y$, then $x$ is preferred over $y$ in the output ranking as well.
• Majority consistency: If there exists a ranking $x_1, \ldots, x_{m}$ such that for every $i < j$, the alternative $x_i$ is preferred over $x_j$ by more than half of the agents, that ranking must be returned.
• Kemeny strategyproofness: Strategic voting is not possible for a single agent, i.e. no agent can achieve a result more aligned with their own preferences by lying about them.

This entry contains two impossibility results for SWFs with $m$ alternatives and $n$ agents:

• There exists no anonymous, unanimous, and Kemeny-strategyproof SWF for $m \geq 5$ and $n$ even or for $m = 4$ and $n$ a multiple of 4.
• There exists no majority-consistent and Kemeny-strategyproof SWF for $m = 4$ and $n \geq 3$ or $m \geq 4$ and $n \in \{9,11,13,15\}\cup\{17,\ldots\}$

For some of the base cases, SAT solving is used by letting specialised automation prove a large number of clauses, translating to the DIMACS format, and importing a proof pre-generated by an external SAT solver using Lammich's GRAT format.