Automated Reasoning for Social Choice Theory

This is the website for a tutorial given at the 26th European Conference on Artificial Intelligence (ECAI-2023).

Description: One of the most exciting developments in the field of computational social choice in recent years has been the use of automated reasoning tools—and SAT solvers in particular—to support scientists in their quest to obtain a deeper understanding of the foundations of multiagent decision making. This approach has allowed the community to construct new proofs for seminal impossibility results in the literature on social choice theory, to prove important new results that otherwise might have been elusive, and in some cases even to fully automate the discovery of new results. This tutorial will be a hands-on introduction to this powerful new approach and provide attendees with the background knowledge as well as the practical tools they need to apply it in their own research. It will be accessible and useful for both people already working in computational social choice and those new to the field.

Background: No programming skills (except for reading simple snippets of code) will be required to follow the tutorial. But basic programming skills in Python will make it easier to apply what you have learned in your own research. Prior exposure to social choice theory is helpful but not required.

Practicalities: You will be provided with simple code fragments that not only will allow you to easily reproduce everything I present in the tutorial (in real time, for those who want to), but that also should prove useful as a starting point for adapting the approach to the specific needs of your own research.

Setting up your laptop: To try things out for yourself, you need to be able to run Jupyter Notebooks for Python 3 and you need to have PySAT installed on your machine. Download and run the notebook setup.ipynb (download) to check whether your local setup is working as intended.

History: I have previously taught the same material at AAMAS-2023.