{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,17]],"date-time":"2026-04-17T23:37:16Z","timestamp":1776469036363,"version":"3.51.2"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2018,1,31]],"date-time":"2018-01-31T00:00:00Z","timestamp":1517356800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"TUM Institute for Advanced Study through a Hans Fischer Senior Fellowship"},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","award":["BR 2312\/7-2 and BR 2312\/10-1"],"award-info":[{"award-number":["BR 2312\/7-2 and BR 2312\/10-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2018,4,30]]},"abstract":"<jats:p>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\u2019 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.<\/jats:p>","DOI":"10.1145\/3125642","type":"journal-article","created":{"date-parts":[[2018,2,1]],"date-time":"2018-02-01T13:10:52Z","timestamp":1517490652000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Proving the Incompatibility of Efficiency and Strategyproofness via SMT Solving"],"prefix":"10.1145","volume":"65","author":[{"given":"Florian","family":"Brandl","sequence":"first","affiliation":[{"name":"Technische Universit\u00e4t M\u00fcnchen"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Felix","family":"Brandt","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t M\u00fcnchen"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manuel","family":"Eberl","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t M\u00fcnchen"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"Geist","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t M\u00fcnchen"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,1,31]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 28th AAAI Conference on Artificial Intelligence (AAAI\u201914)","author":"Aziz H."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jmateco.2015.06.014"},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"H. Aziz F. Brandl F. Brandt and M. Brill. 2018. On the tradeoff between efficiency and strategyproofness. Games and Economic Behavior. Forthcoming. H. Aziz F. Brandl F. Brandt and M. Brill. 2018. On the tradeoff between efficiency and strategyproofness. Games and Economic Behavior. Forthcoming.","DOI":"10.1016\/j.geb.2018.03.005"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.econlet.2013.09.006"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 12th International Conference on Autonomous Agents and Multiagent Systems (AAMAS\u201913)","author":"Aziz H."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00355-017-1059-3"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9246-5"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 8th International Workshop on Satisfiability Modulo Theories.","author":"Barrett C."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1006\/jeth.2000.2710"},{"key":"e_1_2_1_10_1","unstructured":"F. Brandl F. Brandt and C. Geist. 2016a. Proving the Incompatibility of Efficiency and Strategyproofness via SMT Solving. Technical Report. http:\/\/arxiv.org\/abs\/1604.05692. F. Brandl F. Brandt and C. Geist. 2016a. Proving the Incompatibility of Efficiency and Strategyproofness via SMT Solving. Technical Report. http:\/\/arxiv.org\/abs\/1604.05692."},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI\u201915)","author":"Brandl F."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.econlet.2016.01.028"},{"key":"e_1_2_1_13_1","volume-title":"Trends in Computational Social Choice","author":"Brandt F."},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"F. Brandt V. Conitzer U. Endriss J. Lang and A. Procaccia (Eds.). 2016. Handbook of Computational Social Choice. Cambridge University Press. F. Brandt V. Conitzer U. Endriss J. Lang and A. Procaccia (Eds.). 2016. Handbook of Computational Social Choice. Cambridge University Press.","DOI":"10.1017\/CBO9781107446984.002"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/3013558.3013574"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"F. Brandt C. Geist and D. Peters. 2017. Optimal bounds for the no-show paradox via SAT solving. Mathematical Social Sciences. Special Issue in Honor of Herv\u00e9 Moulin. Vol. 90. 18--27. F. Brandt C. Geist and D. Peters. 2017. Optimal bounds for the no-show paradox via SAT solving. Mathematical Social Sciences. Special Issue in Honor of Herv\u00e9 Moulin. Vol. 90. 18--27.","DOI":"10.1016\/j.mathsocsci.2016.09.003"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_2_1_18_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science","volume":"7795","author":"de Moura L."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1467-9248.2008.00746.x"},{"key":"e_1_2_1_20_1","first-page":"365","article-title":"A geometric proof of Gibbard\u2019s random dictatorship theorem","volume":"7","author":"Duggan J.","year":"1996","journal-title":"Economic Theory"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00355-006-0152-9"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00355-008-0299-7"},{"key":"e_1_2_1_23_1","unstructured":"M. Eberl. 2016a. A Formal Proof of the Incompatibility of SD-Efficiency and SD-Strategy-Proofness. Bachelor\u2019s Thesis. Technische Universit\u00e4t M\u00fcnchen. M. Eberl. 2016a. A Formal Proof of the Incompatibility of SD-Efficiency and SD-Strategy-Proofness. Bachelor\u2019s Thesis. Technische Universit\u00e4t M\u00fcnchen."},{"key":"e_1_2_1_24_1","unstructured":"M. Eberl. 2016b. The incompatibility of SD-efficiency and SD-strategy-proofness. Archive of Formal Proofs. Available at http:\/\/isa-afp.org\/entries\/SDS_Impossibility.shtml. M. Eberl. 2016b. The incompatibility of SD-efficiency and SD-strategy-proofness. Archive of Formal Proofs. Available at http:\/\/isa-afp.org\/entries\/SDS_Impossibility.shtml."},{"key":"e_1_2_1_25_1","unstructured":"D. Gale. 1987. College Course Assignments and Optimal Lotteries. Mimeo. D. Gale. 1987. College Course Assignments and Optimal Lotteries. Mimeo."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/2016945.2016950"},{"key":"e_1_2_1_27_1","unstructured":"C. Geist and D. Peters. 2017. Computer-aided methods for social choice theory. In Trends in Computational Social Choice U. Endriss (Ed.). C. Geist and D. Peters. 2017. Computer-aided methods for social choice theory. In Trends in Computational Social Choice U. Endriss (Ed.)."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.2307\/1914083"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.2307\/1911681"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1111\/papa.12029"},{"key":"e_1_2_1_31_1","unstructured":"J. W. Headlam. 1933. Election by Lot at Athens. Cambridge University Press. J. W. Headlam. 1933. Election by Lot at Athens. Cambridge University Press."},{"key":"e_1_2_1_32_1","unstructured":"A. Hylland. 1980. Strategyproofness of Voting Procedures With Lotteries as Outcomes and Infinite Sets of Strategies. Mimeo. A. Hylland. 1980. Strategyproofness of Voting Procedures With Lotteries as Outcomes and Infinite Sets of Strategies. Mimeo."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00355-012-0674-2"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jet.2005.05.001"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.mathsocsci.2008.07.003"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1006\/jeth.2001.2864"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s003550050120"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10058-012-0130-x"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jet.2017.05.004"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0"},{"key":"e_1_2_1_41_1","volume-title":"Lecture Notes in Computer Science","volume":"2283","author":"Nipkow T."},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","unstructured":"N. Nisan T. Roughgarden \u00c9. Tardos and V. Vazirani. 2007. Algorithmic Game Theory. Cambridge University Press. N. Nisan T. Roughgarden \u00c9. Tardos and V. Vazirani. 2007. Algorithmic Game Theory. Cambridge University Press.","DOI":"10.1017\/CBO9780511800481"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00433523"},{"key":"e_1_2_1_44_1","doi-asserted-by":"crossref","unstructured":"J. Rothe (Ed.). 2015. Economics and Computation: An Introduction to Algorithmic Game Theory Computational Social Choice and Fair Division. Springer. J. Rothe (Ed.). 2015. Economics and Computation: An Introduction to Algorithmic Game Theory Computational Social Choice and Fair Division. Springer.","DOI":"10.1007\/978-3-662-47904-9"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00355-011-0616-4"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0531(75)90050-2"},{"key":"e_1_2_1_47_1","volume-title":"Multiagent Systems: Algorithmic, Game-Theoretic, and Logical Foundations","author":"Shoham Y.","year":"2009"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10058-003-0102-2"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2009.02.005"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0531(90)90070-Z"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3125642","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3125642","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:30:06Z","timestamp":1750217406000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3125642"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,31]]},"references-count":50,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,4,30]]}},"alternative-id":["10.1145\/3125642"],"URL":"https:\/\/doi.org\/10.1145\/3125642","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,1,31]]},"assertion":[{"value":"2016-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-01-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}