Author(s): Deanna Garrett
Mentor(s): Russ Ross
Institution UTech
The University Course Timetabling Problem (UCTP) is the computational challenge of assigning university courses to rooms, timeslots, and instructors to create a conflict-free schedule. Ideally, this schedule would minimize overlaps between courses that students are likely to need to take at the same time such as courses required for the same major. Prioritizing and avoiding overlaps is especially important when courses only have one section offered per semester. Conflicts such as these can result in students being unable to take courses according to plan, hindering academic progress and potentially causing graduation delays. Alternatively, courses with multiple sections and times offered in a semester are less likely to cause interferences. Achieving a fully conflict-free schedule is usually impossible and finding an optimal schedule is computationally intractable. Solvers for the Boolean Satisfiability problem (SAT solvers) are tools that analyze combinatoric problems expressed in a rigidly defined formal logic encoding and determine whether a solution exists. By encoding Utah Tech’s course scheduling data for SAT, we can determine the lower bounds of conflicts that are unavoidable in high-priority categories. SAT solvers are constantly evolving technologies, and their efficacy is sensitive to encoding techniques. We are investigating methods to mitigate the most impactful conflicts, improving course availability for students and helping them stay on track toward graduation by testing different solvers and comparing encoding techniques. We will integrate the lower bounds established by SAT into a hybrid system with our current software to turn optimization efforts away from conflicts that a SAT solver has proven impossible to eliminate.