Leveraging SAT-SMT for TA Scheduling Optimization: Enhancing Efficiency and Effectiveness

The scheduling of teaching assistants (TAs) is a complex task, similar to the Nurse Rostering Problem. The TA scheduling problem involves finding the best way to assign TAs to different time slots. A feasible schedule must adhere to all the strict constraints, while an optimal schedule maximizes the flexible constraints. This paper discusses the methodology and implementation of an algorithm that produces an optimized schedule using Z3 and Google OR-Tools. It also evaluates the strengths and shortcomings of these libraries. Additionally, the paper explores research on preference modeling and potential methods for gathering preferences, which are informed by discussions and polls among TAs.