In rank aggregation, the goal is to combine multiple input rankings into a single output ranking. In this paper, we analyze rank aggregation methods, so-called social welfare functions (SWFs), with respect to strategyproofness, which requires that no agent can misreport his ranking to obtain an output ranking that is closer to his true ranking in terms of the Kemeny distance. As our main result, we show that no anonymous SWF satisfies unanimity and strategyproofness when there are at least four alternatives. This result is proven by SAT solving, a computer-aided theorem proving technique, and verified by Isabelle, a highly trustworthy interactive proof assistant. Further, we prove by hand that strategyproofness is incompatible with majority consistency, a variant of Condorcet-consistency for SWFs. Lastly, we show that all SWFs in two natural classes have a large incentive ratio and are thus highly manipulable.

翻译：在排序聚合中，目标是将多个输入排序合并为一个输出排序。本文从策略不可操纵性角度分析排序聚合方法（即所谓的社会福利函数），该性质要求任何参与者均不能通过虚报其排序来获得在Kemeny距离度量下更接近其真实排序的输出排序。我们的主要结果表明：当备选方案不少于四个时，不存在满足全体一致性与策略不可操纵性的匿名社会福利函数。该结果通过SAT求解（一种计算机辅助定理证明技术）进行证明，并由高度可信的交互式证明辅助工具Isabelle验证。此外，我们通过人工证明策略不可操纵性与多数一致性（社会福利函数中孔多塞一致性的一种变体）不相容。最后，我们证明两个自然类别中的所有社会福利函数均具有较高的激励比率，因而具有高度可操纵性。