Multiwinner voting rules can be used to select a fixed-size committee from a larger set of candidates. We consider approval-based committee rules, which allow voters to approve or disapprove candidates. In this setting, several voting rules such as Proportional Approval Voting (PAV) and Phragm\'en's rules have been shown to produce committees that are proportional, in the sense that they proportionally represent voters' preferences; all of these rules are strategically manipulable by voters. On the other hand, a generalisation of Approval Voting gives a non-proportional but strategyproof voting rule. We show that there is a fundamental tradeoff between these two properties: we prove that no multiwinner voting rule can simultaneously satisfy a weak form of proportionality (a weakening of justified representation) and a weak form of strategyproofness. Our impossibility is obtained using a formulation of the problem in propositional logic and applying SAT solvers; a human-readable version of the computer-generated proof is obtained by extracting a minimal unsatisfiable set (MUS). We also discuss several related axiomatic questions in the domain of committee elections.

翻译：多赢家投票规则可用于从更大的候选人集合中选举出固定规模的委员会。我们考虑基于认可度的委员会选举规则，该规则允许选民对候选人表示认可或不认可。在此设定下，诸如比例认可投票（PAV）与法格曼规则等若干投票规则已被证明能产生具有比例代表性的委员会，即这些委员会能按比例反映选民的偏好；然而所有这些规则均可能受到选民策略性操纵的影响。另一方面，认可度投票的一种推广形式虽能提供防策略的投票规则，却缺乏比例代表性。我们证明这两种性质之间存在根本性权衡：通过命题逻辑形式化该问题并应用SAT求解器，我们证明了不存在任何多赢家投票规则能同时满足弱比例性条件（合理化代表性的弱化形式）与弱防策略性条件。该不可能性证明通过提取最小不可满足集（MUS）获得了计算机生成证明的可读版本。我们同时探讨了委员会选举领域中若干相关的公理化问题。