Analysis of One-to-One Matching Mechanisms via SAT Solving: Impossibilities for Universal Axioms
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).
Cite
Text
Endriss. "Analysis of One-to-One Matching Mechanisms via SAT Solving: Impossibilities for Universal Axioms." AAAI Conference on Artificial Intelligence, 2020. doi:10.1609/AAAI.V34I02.5561Markdown
[Endriss. "Analysis of One-to-One Matching Mechanisms via SAT Solving: Impossibilities for Universal Axioms." AAAI Conference on Artificial Intelligence, 2020.](https://mlanthology.org/aaai/2020/endriss2020aaai-analysis/) doi:10.1609/AAAI.V34I02.5561BibTeX
@inproceedings{endriss2020aaai-analysis,
title = {{Analysis of One-to-One Matching Mechanisms via SAT Solving: Impossibilities for Universal Axioms}},
author = {Endriss, Ulle},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2020},
pages = {1918-1925},
doi = {10.1609/AAAI.V34I02.5561},
url = {https://mlanthology.org/aaai/2020/endriss2020aaai-analysis/}
}