SAT Model for the Curriculum-Based Course Timetabling Problem

Two widely used problems are the Satisability problem (SAT) and the Curriculum-Based Course Timetabling (CB-CTT) prob- lem. The SAT problem searches for an assignment that make true a cer- tain boolean formula. On the other side, the CB-CTT involves the task of scheduling lectures of courses to rooms, considering teacher availability, a specied curricula, and a set of constraints. Given the advances achieved in the solution of the SAT Problem, this research proposes a SAT Model of the CB-CTT problem, to aid in the construction of timetables. To demonstrate that the model can aid in the solution of real instances of the CB-CTT problem, a case of study derived from a university in Mex- ico was considered. This special case of CB-CTT involves the constraint where each teacher cannot teach more than one course in the same cur- riculum, which is included in the set of 3 hard constraints and 2 soft constraints analyzed in this research. According to the results obtained, the considered complete SAT solver required a few minutes to nd a solution for the instance.