Analysis of One-to-One Matching Mechanisms via SAT Solving: Impossibilities for Universal Axioms
Ulle Endriss

Abstract:
We  develop  a  powerful  approach  that  makes  modern  SAT solving techniques available as a tool to support the axiomatic analysis of economic matching mechanisms. Our central result  is  a  preservation  theorem,  establishing  sufficient  conditions  under  which  the  possibility  of  designing  a  matching  mechanism  meeting  certain  axiomatic  requirements  for a given number of agents carries over to all scenarios with strictly fewer agents. This allows us to obtain general results about matching by verifying claims for specific instances using a SAT solver. We use our approach to automatically de-rive elementary proofs for two new impossibility theorems: (i) a strong form of Roth’s classical result regarding the impossibility of designing mechanisms that are both stable and strategyproof and (ii) a result establishing the impossibility of guaranteeing stability while also respecting a basic notion of cross-group fairness (so-called gender-indifference).