21 October 2013, Computational Social Choice Seminar, Christian Geist (Munich)

Abstract

Solving open problems in social choice using computer-aided proving techniques appears to be a promising direction of current research. While this approach (in particular combined with SAT solving) has been shown to be viable in the context of classical impossibility theorems (P. Tang and F. Lin, Artificial Intelligence Journal, 2009) as well as set extensions (C. G. and U. Endriss, Journal of Artificial Intelligence Research, 2011), we demonstrate that it can also be applied to the more complex setting of irresolute majoritarian social choice functions (SCFs) and corresponding notions of strategyproofness. These types of problems, however, require a more evolved encoding as otherwise the search space rapidly becomes much too large. Our contribution therefore is twofold: On the one hand, we present an efficient encoding for translating problems concerning irresolute majoritarian SCFs to SAT. On the other hand, we prove various results for Kelly- and Fishburn-strategyproofness using this framework. For example, we show that no Pareto-optimal majoritarian SCF satisfies Fishburn-strategyproofness.

For more information, see http://www.illc.uva.nl/~ulle/seminar/, or contact Ulle Endriss (ulle.endriss at uva.nl).