Optimally scheduling real world sports leagues by reduction to SAT

Several types of constraints must be satisfied by schedules of real world sports leagues, e. g. stadium unavailability, fixed matches, forbidden matches, minimum number of breaks. Taking into account such constraints, determining a feasible schedule becomes a challenging task. Usually, there is no schedule satisfying all given constraints and, hence, some of the constraints are considered as 'soft' ones. There are various models appropriately describing the environment of real sport leagues. Only heuristic methods are known from the literature for solving instances of such models for real dimensions. We consider here a model which satisfies the demands of many sports leagues. We solve our model by a method which consists in formulating the problem as series of instances of the propositional satisfiability problem and adaption of a satisfiability solver for these specific instances. We test our method on two real world sports leagues and solve the problem optimally in each case. Our solver shows good computational results also on generated test instances, which are motivated by real life requirements of sports league scheduling. Our solver can be easily extended to meet the demands of other sports leagues.