AI 中文总结
本文通过约束 Horn 子句推理与多面体计算，综合无限域投票方法，验证其性质，证明四名候选人存在满足 Condorcet 获胜者等四个核心公理的投票方法。
AI 中文摘要
社会选择中的一个常见问题是确定是否存在满足某些期望标准的社会选择程序（如投票方法），SAT求解等计算机辅助方法有时可回答此类问题。但在典型编码下，SAT求解器仅能综合有限域上的投票方法，而我们可能需要无限域上的投票方法，例如固定候选人数、选民数为任意有限值的所有偏好构型构成的域。本文采用基于约束 Horn 子句推理与多面体计算的方法，综合得到无限域上的投票方法，随后使用 SMT 和 Lean 验证其性质。主要结果是关于投票理论中四个知名标准的可能性定理：Condorcet 获胜者标准、Condorcet 失败者标准、正参与性和可分辨性。已有研究表明，对于五名及以上候选人，不存在满足这些公理的投票方法；对于四名候选人，不存在满足这些核心公理外加一个不变性公理的投票方法。本文证明，对于四名候选人，确实存在一种满足核心公理及更多性质的投票方法。
英文摘要
A common problem in social choice is to determine whether there is a social choice procedure, such as a voting method, satisfying some desired criteria. Computer-aided methods such as SAT solving can sometimes answer these questions. However, under typical encodings, a SAT solver may only synthesize a voting method on a finite domain, while we may want one on an infinite domain, such as the domain of all preference profiles for a fixed number of candidates but any finite number of voters. In this paper, we use an approach based on reasoning with constrained Horn clauses and computation with polyhedra to synthesize a voting method on an infinite domain. We then use SMT and Lean to verify its properties. Our main result is a possibility theorem about four well-known criteria from voting theory: the Condorcet winner and loser criteria, positive involvement, and resolvability. Previous work has shown that for five or more candidates, there is no voting method satisfying these axioms, and that for four candidates, there is no method satisfying these core axioms plus one more invariance axiom. Here we show that for four candidates, there does exist a method satisfying the core axioms and more.
Comments10 pages, 1 figure
