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

Authors

  • Ulle Endriss University of Amsterdam

DOI:

https://doi.org/10.1609/aaai.v34i02.5561

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

Downloads

Published

2020-04-03

How to Cite

Endriss, U. (2020). Analysis of One-to-One Matching Mechanisms via SAT Solving: Impossibilities for Universal Axioms. Proceedings of the AAAI Conference on Artificial Intelligence, 34(02), 1918-1925. https://doi.org/10.1609/aaai.v34i02.5561

Issue

Section

AAAI Technical Track: Game Theory and Economic Paradigms