SAT-Based approaches for the general high school timetabling problem / von Emir Demirović
VerfasserDemirović, Emir
Begutachter / BegutachterinMusliu, Nysret
ErschienenWien, 2017
Umfangxi, 127 Seiten
HochschulschriftTechnische Universität Wien, Dissertation, 2017
Schlagwörter (EN)maxSAT / optimization / search / timetabling / bitvectors / modeling / satisfiability / heuristics / local search
URNurn:nbn:at:at-ubtuw:1-98875 Persistent Identifier (URN)
 Das Werk ist frei verfügbar
SAT-Based approaches for the general high school timetabling problem [0.91 mb]
Zusammenfassung (Englisch)

High School Timetabling (HSTT) is a well known and widespread 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. In this work, we consider the general HSTT problem, abbreviated as XHSTT. Despite significant research efforts for XHSTT and other timetabling problems, no \emph used within a large neighborhood search scheme. We carried out thorough experimentation on important benchmark instances that can be found in the repository of the third international timetabling competition (ITC 2011) and compared with the state-of-the-art algorithms for XHSTT. Detailed experiments were performed in order to determine the most appropriate maxSAT solvers and cardinality constraint encodings, evaluate our SMT approach, and compare with integer programming and the ITC 2011 results. Computational results demonstrate that we outperform the integer programming approach on numerous benchmarks. We are able to obtain even better results by combining several maxSAT solvers. When compared to the leading KHE engine for XHSTT, the bitvector modeling approach provided significant improvements for local search algorithms such as hill climbing and simulated annealing. Lastly, our large neighborhood search algorithm excelled in situations when limited computational time is allocated, being able to obtain better results than the state-of-the-art solvers and the pure maxSAT approach in many benchmarks.