Solving the Course-timetabling Problem of Cairo University Using Max-SAT

TL;DR

This paper encodes Cairo University's course timetabling problem into Max-SAT, demonstrating how modern Max-SAT solvers can efficiently generate conflict-free schedules for complex real-world problems.

Contribution

It presents a novel encoding of the university's course timetabling problem into Max-SAT, enabling automated and optimized timetable generation.

Findings

Max-SAT encoding effectively models complex scheduling constraints.

Automated timetable generation reduces conflicts compared to manual scheduling.

The approach demonstrates practical applicability for university scheduling problems.

Abstract

Due to the good performance of current SAT (satisfiability) and Max-SAT (maximum ssatisfiability) solvers, many real-life optimization problems such as scheduling can be solved by encoding them into Max-SAT. In this paper we tackle the course timetabling problem of the department of mathematics, Cairo University by encoding it into Max-SAT. Generating timetables for the department by hand has proven to be cumbersome and the generated timetable almost always contains conflicts. We show how the constraints can be modelled as a Max-SAT instance.