Analysis of One-to-One Matching Mechanisms via SAT Solving: Impossibilities for Universal Axioms
| Authors | |
|---|---|
| Publication date | 2020 |
| Book title | AAAI-20, IAAI-20, EAAI-20 proceedings |
| Book subtitle | Thirty-Fourth AAAI Conference on Artificial Intelligence, Thirty-Second Conference on Innovative Applications of Artificial Intelligence, The Tenth Symposium on Educational Advances in Artificial Intelligence : February 7–12th, 2020, New York Hilton Midtown, New York, New York, USA |
| ISBN |
|
| Series | Proceedings of the AAAI Conference on Artificial Intelligence |
| Event | 34th AAAI Conference on Artificial Intelligence, AAAI 2020 |
| Volume | Issue number | 2 |
| Pages (from-to) | 1918-1925 |
| Publisher | Palo Alto, California: AAAI Press |
| Organisations |
|
| 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 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).
|
| Document type | Conference contribution |
| Language | English |
| Published at | https://doi.org/10.1609/aaai.v34i02.5561 |
| Downloads |
5561-Article Text-8786-1-10-20200512
(Final published version)
|
| Permalink to this page | |
