Solving hard stable marriage problems using logic-based methods

Official URL: https://risc01.sabanciuniv.edu/record=b2767372_(Table of contets)

Matching problems have been studied in economics, starting with the seminal paper of Gale and Shapley, which has led to a Nobel Prize in 2012, utilizing game theory methods with the goal of a mechanism design. One of the well-known matching problems is the Stable Marriage Problem (SM). In SM, for a set of n men and n women, we are given the preferences of individuals: for each man, a complete ranking of the women is specified as preferred partners; similarly, for each woman, a complete ranking of the men is specified as preferred partners. The goal is to marry all men and women (i.e., to find n couples) in such a way that marriages are stable: no man and woman in different couples prefer each other to their partners. We consider a variant of SM, called SMTI, where rankings may be incomplete (i.e., some partners are not acceptable) or may include ties (i.e., some partners are preferred equally). We investigate three hard variants of SMTI, that aim to compute optimal stable matchings with respect to different measures of fairness: Sex-Equal SMTI (maximizes the equality of satisfaction among sexes), Egalitarian SMTI (maximizes the total satisfaction of the preferences of all agents), and Max Cardinality SMTI (minimizes the number of singles). We introduce a suite of novel declarative methods to solve these hard variants of SMTI, using Answer Set Programming (ASP), Constraint Programming (CP), and Propositional Satisfiability (SAT). We empirically evaluate the scalability of methods over randomly generated instances, as the probability of incompleteness and probability of ties change. For Max Cardinality SMTI, we also compare these methods with the existing approaches based on Integer Linear Programming (ILP) and iv Local Search (including Hill-Climbing and Genetic Algorithms). We observe that the declarative methods (ASP, ILP, CP, SAT) are more promising compared to the local search algorithms as the problems get harder with more ties and incompleteness.