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.
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.
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.
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).