Automated Reasoning for Social Choice Theory

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.