The research area of computational social choice deals with the application of techniques from computer science and AI to the design and analysis of economic mechanisms for collective decision making. In this talk, I will report on one of the most exciting recent developments in the field, namely the use of automated reasoning tools, and notably SAT solvers, to support economic theorists in their quest to gain a deeper understanding of what is and what is not possible when it comes to designing fair and efficient mechanisms for decision making. I will exemplify this approach with recent work on the design of matching markets, where the goal is to match, for instance, job seekers and companies on the basis of their preferences. No specialised technical background will be required to follow the exposition.