Automated Reasoning for Course Scheduling

Visual of the final result on Google Calendar

Inspiration

Course scheduling is a real problem at many universities, as it is difficult to account for multiple factors like instructor availability, room sizes, etc., while making sure that all classes are eventually scheduled. Since much of this process is still done manually for departments at UMD, we wanted to come up with an automated solution to satisfy scheduling requirements with less intensive manual effort.

What it does

To put it simply, it is a class-to-room scheduler. Using SMT or SAT modulo theories, the course assistant takes in data about classes, including number of student, professors, available rooms, and room sizes to make the most efficient matches so that all classes are scheduled in rooms without any time conflicts.

How we built it

We set constraints for making class-to-room matches in Python, and used the Z3 SMT solver to find a solution that would take all of them into account and work around them. We then loaded the results into a .csv file that could be uploaded onto a Google Calendar to view the schedule more easily.

Challenges we ran into

It was difficult to make sure that the correct constrains were passed into the Z3 solver, add additional functionality like different class durations and professors, and integrate it with Google Calendar to display the finalized schedule as a sample for a week. Since we were working both virtually and in-person, we relied on good communication between team members to make sure code was combined accurately.

Accomplishments that we're proud of

Over the course of the weekend, we were able to implement (almost) all the features we planned for, and present a program that UMD could use to schedule their own classes if developed further. The progress we made is exciting and shows that SMT could be a viable solution for the problem of scheduling classes.

What we learned

SAT modulo theories and the Z3 solver on Python can be used to solve the satisfiability problem, or find a solution that agrees with a specific series of logic-based constraints. We learned how to apply the logic of SMT to the real-life example of course scheduling and how to work across different file types, integrating the Python code with the Google Calendar API for better visualization of the results.

What's next for Course Assistant

Additional features we could add include accounting for multiple courses and lectures, which is necessary for correct and optimal performance with larger sets of data. It would also be important to take professor's preferences for time and location into account if the project was implemented in the CS department. We could also make sure that small classes would not get scheduled into disproportionately big rooms if smaller rooms were available by giving the solver more constraints, and add even more variety for days and times to account for 1-credit classes taking place only once a week.