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

2020-06-02

Proceedings of the AAAI Conference on Artificial Intelligence, 34

Volume

Vol. 34 No. 02: AAAI-20 Technical Tracks 2

AAAI Technical Track: Game Theory and Economic Paradigms

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 derive 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).

10.1609/aaai.v34i02.5561