Solving the Course-timetabling Problem of Cairo University Using Max-SAT
This solves a specific scheduling problem for a university department, but it is incremental as it applies an existing Max-SAT method to a new dataset.
The paper tackled the course timetabling problem for the mathematics department at Cairo University by encoding it into Max-SAT, resulting in a method to generate timetables that avoids conflicts, though no concrete performance numbers are provided.
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.