One of the most exciting developments in computational social choice in recent years has been the use of tools for automated reasoning developed in AI, notably SAT solvers, to support researchers in social choice theory in their quest of getting a deeper understanding of the axiomatic foundations of collective decision making. This short course, based on the course on computational social choice I teach at the ILLC in Amsterdam, will enable participants to employ these tools in their own research. Lectures will cover both introductory material on the axiomatic method in social choice theory and a hands-on session on how to use a modern SAT solver to (partly) automate the proof of the seminal Gibbard-Satterthwaite Theorem. Participants will also have the opportunity to complete a programming assignment and to present a recent paper from the relevant literature in class.

**Instructor:**Ulle Endriss (ILLC, University of Amsterdam)**Time and Place:**Tuesday, 1 October 2019 (9:00-12:00 and 14:00-17:00) in Room B510 and Tuesday, 8 October 2019 (14:00-17:00) in Room C108, LAMSADE, Paris-Dauphine University**Slides:**PDF

**Prerequisites.**
The course is equally suited for those carrying out research in
(computational) social choice themselves and those who are new to the
field. The only prerequisites for being able to fully benefit from the
course are some very basic programming skills in Python and familiarity
with classical propositional (boolean) logic. If you are not sure
whether you have the right background, you are very welcome to send me
an email. Or just show up. It probably will be fine.
If you plan to do some programming yourself, have a look at these
technical notes sometime before the first session.

**Session 1.**
This will be an introduction to the axiomatic method in social choice
theory, and voting theory in particular. In particular, we are going to prove the
seminal Gibbard-Satterthwaite Theorem regarding the impossibility of
designing a reasonable voting rule that cannot be manipulated by a
strategic voter. Much of this material and more is
covered in the expository paper below.

- U. Endriss. Logic and Social Choice Theory. In A. Gupta and J. van Benthem (eds.),
*Logic and Philosophy Today*. College Publications, 2011.

**Session 2.**
This will be a hands-on session in which we are going to see how we
can largely automate the proof of the Gibbard-Satterthwaite Theorem by
translating its statment for the special case of three
alternatives and two voters into a (huge) formula in propositional
logic, which we can then analyse with the help of a SAT solver. The
first expository paper cited below reviews this methodology and the
second one discusses its relevance from the point of view of Economics.

- C. Geist and D. Peters. Computer-Aided
Methods for Social Choice Theory. In U. Endriss (ed.),
*Trends in Computational Social Choice*. AI Access, 2017. - S. Chatterjee and A. Sen. Automated Reasoning in Social Choice
Theory: Some Remarks.
*Mathematics in Computer Science*, 8(1):5-10, 2014.

**Session 3.**
The programme for this final session depends on the wishes of the
participants. We could discuss your solutions to the exercises; or some of
you might want to give a talk
about a relevant paper in this area of
computational social choice; or we could brainstorm about possible
future research directions. As for the papers you may want to present,
you can choose from the list below (or talk to me if you have
other suggestions).

- P. Tang and F. Lin. Computer-Aided Proofs of Arrow's and
other Impossibility Theorems.
*Artificial Intelligence*, 173(11):1041-1053, 2009. - C. Geist and U. Endriss. Automated Search for Impossibility Theorems in Social Choice Theory: Ranking Sets of Objects.
*Journal of Artificial Intelligence Research*, 40:143-174, 2011. - F. Brandt and C. Geist. Finding Strategyproof
Social Choice Functions via SAT Solving.
*Journal of Artificial Intelligence Research*, 55:565-602, 2016. - F. Brandl, F. Brandt, C. Geist, and J. Hofbauer. Strategic Abstention Based on Preference Extensions: Positive Results and Computer-Generated Impossibilities. IJCAI-2015.
- F. Brandt, C. Geist, and D. Peters. Optimal
Bounds for the No-Show Paradox via SAT Solving.
*Mathematical Social Sciences*, 90:18-27, 2017. - D. Peters. Proportionality and Strategyproofness in Multiwinner Elections. AAMAS-2018.
- F. Brandl, F. Brandt, M. Eberl, and C. Geist. Proving the
Incompatibility of Efficiency and Strategyproofness via SMT
Solving.
*Journal of the ACM*, 65(2):6, 2018.