Proving the Incompatibility of Efficiency and Strategyproofness via SMT Solving
Proving the Incompatibility of Efficiency and Strategyproofness via SMT Solving
复制标题
通过SMT求解证明效率和策略证明的不相容性
DOI：
10.1145/3125642
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Christian Geist
中科院分区：
文献类型：
--
作者：
Florian Brandl;Felix Brandt;Manuel Eberl;Christian Geist
当聚集多个代理的偏好时，两个重要的要求是结果应该是经济有效的，并且聚集机制不应该被操纵。在这篇文章中，我们使用随机聚集机制的这两个条件，提供了一个彻底不可能的计算机辅助证明。更准确地说，我们证明了每一种有效的聚集机制都可以被操纵为所有期望的代理偏好的效用表示。这解决了一个悬而未决的问题，并加强了几个已有的定理，包括在赋值的特殊领域内所示的语句。我们的证明是通过将索赔表示为实值算术中谓词上的可满足性问题来获得的，然后使用可满足性模理论(SMT)求解器进行验证。为了验证结果的正确性，SMT求解器返回的最小不可满足约束集被转换回高阶逻辑中的证明，并由交互式定理证明器自动验证。据我们所知，这是SMT解算器在计算社会选择中的第一次应用。
Two important requirements when aggregating the preferences of multiple agents are that the outcome should be economically efficient and the aggregation mechanism should not be manipulable. In this article, we provide a computer-aided proof of a sweeping impossibility using these two conditions for randomized aggregation mechanisms. More precisely, we show that every efficient aggregation mechanism can be manipulated for all expected utility representations of the agents’ preferences. This settles an open problem and strengthens several existing theorems, including statements that were shown within the special domain of assignment. Our proof is obtained by formulating the claim as a satisfiability problem over predicates from real-valued arithmetic, which is then checked using a satisfiability modulo theories (SMT) solver. To verify the correctness of the result, a minimal unsatisfiable set of constraints returned by the SMT solver was translated back into a proof in higher-order logic, which was automatically verified by an interactive theorem prover. To the best of our knowledge, this is the first application of SMT solvers in computational social choice.
登录
查看更多内容
策略证明的主要决策方案
影响因子：
0.9
作者：
Bhaskar Dutta;H. Peters;Arunava Sen
通讯作者：
Arunava Sen
影响因子：
0.2
作者：
通讯作者：
--
通过 SAT 求解找到策略证明的社会选择函数
DOI：
10.1613/jair.4959
发表时间：
2016
期刊：
影响因子：
--
作者：
F. Brandt;C. Geist
通讯作者：
C. Geist
吉巴德随机独裁定理的另一种直接证明
DOI：
--
发表时间：
2004
期刊：
Review of Economic Design (Springer-Verlag) 8
影响因子：
--
作者：
Kudo;Noritaka;石井 明;石井 明;Akira Ishii;石井 明;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;田中 靖人;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;Yasuhito Tanaka;田中 靖人;田中 靖人;Yasuhito Tanaka (田中 靖人);Yasuhito Tanaka (田中 靖人)
通讯作者：
Yasuhito Tanaka (田中 靖人)
吉伯德随机独裁结果的另一种证明
影响因子：
0.9
作者：
S. Nandeibam
通讯作者：
S. Nandeibam