HIIT Kumpula Seminar: Using SAT to solve stable matching problems with couples

Abstract:Stable matching problems are common in many application areas, e.g., matching doctors into hospital programs. These problems involve finding a matching between two groups of agents. The matching must be stable in the sense that it must be immune to unilateral defections (i.e., defections involving a pair of agents, one from each group). The classical algorithm for finding stable matchings is the deferred acceptance algorithm of Gale and Shapely (DA). When each agent has preferences independent of the other agents, DA runs in polynomial time, always finds a stable matching, and has a number of other nice properties. However, when complementarities exist between agent's preferences finding a stable matching often becomes NP-Complete. The practically important hospital residence matching problem, where residents might be grouped into couples who have shared preferences (SMP-C), is an example of an NP-Hard stable matching problem. In this talk we examine SAT and IP encodings for solving SMP-C. We arrive at a SAT encoding that works well in practice, and better than the IP encoding. We use the SAT encoding to investigate empirically the set of stable matches for matching problems generated according to different distributions.

This is joint work with Joanna Drummond and Andrew Perrault, both from the University of Toronto.

Bio: Fahiem Bacchus is a professor of computer science at the University of Toronto. His research fits broadly in the area of knowledge representation and reasoning, a subfield of artificial intelligence. He has made a number of key contributions during his career, including the development of logics for representing different forms of probabilistic knowledge and automated planning algorithms that can exploit domain specific control knowledge expressed in linear temporal logic (LTL). For the past 15 years his work has concentrated on automated reasoning algorithms for solving various forms of the satisfiability problem: finding a model (SAT), counting the number of models (#SAT), solving quantified Boolean formulas (QBF), and finding optimal models (MaxSAT). His group has been successful in building award winning solvers for all of these problems. He has served as the program chair of several major AI conferences, including Uncertainty in AI (UAI), the International Conference on Automated Planning and Scheduling (ICAPS) and the International Conference on Theory and Applications of Satisfiability Testing (SAT); and will serve as conference chair of IJCAI-17. Fahiem is also a Fellow of the Association for the Advancement of AI (AAAI).