This is the website for tutorial T7 at AAMAS-2023. If you plan to attend the tutorial, please come back to check this website a few days in advance.
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. Participants 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.