Algorithmic mechanism design, as practised today, is a manual process; however, manual design and reasoning do not scale well with the complexity of design tasks. In this paper, we study computer-aided mechanism design as an alternative to manual construction and analysis of mechanisms.
In our approach, a mechanism is a program that receives inputs from agents with private preferences, and produces a public output. Rather than programming such a mechanism manually, the human designer writes a high-level partial specification that includes behavioral models of agents and a set of logical correctness requirements (for example, truth-telling) on the desired mechanism. A program synthesis algorithm is now used to automatically search a large space of candidate mechanisms and find one that satisfies the requirements. The algorithm is based on a reduction to automated first-order logic theorem proving -- specifically, deciding the satisfiability of quantifier-free formulas in the first-order theory of reals.
We present an implementation of our synthesis approach on top of a Satisfiability Modulo Theories solver. The system is evaluated through several case studies where we automatically synthesize a set of classic mechanisms and their variations, including the Vickrey auction, a multistage auction, a position auction, and a voting mechanism.