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 ^We evaluated different cardinality constraint encodings, solvers, and important special cases in order to significantly simplify the modeling in practice. We note that resource assignment constraints have been considered only for special cases, rather than in general. In addition, we investigated a maxSAT-based satisfiability modulo theories (SMT) approach. Another model we studied in this work is based on bitvectors. By using a series of bitvector operations (such as \emph ^Furthermore, to the best of our knowledge, it is the first time maxSAT is 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.