MaxSAT-based large neighborhood search for high school timetabling

High School Timetabling (HSTT) is a well known and wide spread problem. The problem consists of coordinating resources (e.g. teachers, rooms), times, and events (e.g. lectures) with respect to various constraints. Unfortunately, HSTT is hard to solve and just finding a feasible solution for simple variants of HSTT have been proven to be NP-complete. We propose a new algorithm for HSTT which combines local search with a novel maxSAT-based large neighborhood search. A local search algorithm is used to drive an initial solution into a local optimum and then more powerful large neighborhood search (LNS) techniques based on maxSAT are used to further improve the solution. We prove the effectiveness of our approach with experimental results on instances taken from the Third International Timetabling Competition 2011 and the XHSTT-2014 benchmark archive. We were able to model 27 out of 39 instances. The remaining 12 instances were not modeled because the currently used maxSAT formulation for XHSTT does not support resource assignments in general. For the instances which could be modeled, our algorithm shows good performance when compared to other XHSTT state-of-the-art solvers and for several instances new best known upper bounds have been computed.