High School Timetabling (HSTT) is a well known and widespread problem. It consists of coordinating resources (e.g. teachers, rooms), times, and events (e.g. lectures) with respect to various constraints. In this paper, I summarize the work I have done towards exploring the relationship between propositional logic and HSTT. This includes various modeling techniques in the form of maxSAT and bitvectors, data structures for local search algorithms, and the combination of maxSAT and metaheuristic algorithms. In addition, I discuss possible directions for future work as a part of a long-term research goal to combine complete and metaheuristic algorithms.