Optimal bounds for the no-show paradox via SAT solving

Felix Brandt, Christian Geist, Dominik Peters

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

11 Scopus citations

Abstract

Voting rules allow multiple agents to aggregate their preferences in order to reach joint decisions. Perhaps one of the most important desirable properties in this context is Condorcet-consistency, which requires that a voting rule should return an alternative that is preferred to any other alternative by some majority of voters. Another desirable property is participation, which requires that no voter should be worse off by joining an electorate. A seminal result in social choice theory by Moulin [28] has shown that Condorcet-consistency and participation are incompatible whenever there are at least 4 alternatives and 25 voters. We leverage SAT solving to obtain an elegant human-readable proof of Moulin's result that requires only 12 voters. Moreover, the SAT solver is able to construct a Condorcet-consistent voting rule that satisfies participation as well as a number of other desirable properties for up to 11 voters, proving the optimality of the above bound. We also obtain tight results for set-valued and probabilistic voting rules, which complement and significantly improve existing theorems.

Original languageEnglish
Title of host publicationAAMAS 2016 - Proceedings of the 2016 International Conference on Autonomous Agents and Multiagent Systems
PublisherInternational Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS)
Pages314-322
Number of pages9
ISBN (Electronic)9781450342391
StatePublished - 2016
Event15th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2016 - Singapore, Singapore
Duration: 9 May 201613 May 2016

Publication series

NameProceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS
ISSN (Print)1548-8403
ISSN (Electronic)1558-2914

Conference

Conference15th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2016
Country/TerritorySingapore
CitySingapore
Period9/05/1613/05/16

Keywords

  • Computer-aided theorem proving
  • Condorcet
  • No-show paradox
  • Participation
  • SAT
  • Social choice theory

Fingerprint

Dive into the research topics of 'Optimal bounds for the no-show paradox via SAT solving'. Together they form a unique fingerprint.

Cite this