The Runtime Characteristics of Great Explorations’ Prototype SAT-based Matching Algorithm

Registrants of the Great Explorations event rank their top six preferred workshops, three of which they get to attend during the day’s three workshop time-slots. My goal in this project was to write an algorithm that would assign each participant to as many of their most preferred workshops as possible. To this end, I choose to model this as a Boolean satisfiability (SAT) problem. Unfortunately, the exponential growth of the runtime makes realistically sized instances infeasible to solve. In this report, I outline how and why I modeled this problem in terms of SAT, benchmark the SAT solver’s speed at solving relatively small problem instances, then extrapolate the data to estimate how long it would take to solve a larger, real-world instance. It is my hope that this work will help inform future development of different kinds of matching algorithms for Great Explorations and other similar organizations. https://git.io/fjWl9