Using SAT to solve stable matching problems with couples

Speaker:        Professor Fahiem Bacchus
                Department of Computer Science
                University of Toronto

Title:          "Using SAT to solve stable matching problems with couples"

Date:           Thursday, 12 May 2016

Time:           3:00pm - 4:00pm

Venue:          Lecture Theater G (near lift 25/26), HKUST

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.

**********************
Biography:

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 sub-field 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 UAI, ICAPS
and SAT; and will serve as Conference Chair of IJCAI-17. Fahiem is also a
Fellow of the Association for the Advancement of AI (AAAI).