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

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsScheduling and Timetabling Solutions · Constraint Satisfaction and Optimization · Formal Methods in Verification
