Exercise ‹4›:

College schedules
Note: this problem has been taken from the Logic in Information Technology subject at Barcelona School of Informatics.

Solve the following exercise by means of a reduction to SAT:
• Plan the weekly schedule of a college. The college opens 5 days a week, from 8 to 20h (12 hours/day). A course consists of a list of subjects. Each subject belongs to a course, and has a certain amount of weekly sessions, a set of classrooms suitable for it (at least one), and a set of teachers that can teach it (at least one). There can’t be two sessions of the same subject in the same day. All the sessions of a given subject must be imparted in the same class and by the same teacher. Each teacher has a set of hours in which it is available. Naturally, there can’t be more than one class per classroom or teacher at the same time. Each course must have a compact schedule (without spare hours between classes of that course in the same day), and no more than 6 hours of class per day. Sessions from the same course cannot overlap. Find a planning, if possible, fulfilling all these restrictions.
The input of the exercise and the output with the solution (when the input is solvable) are as follows:
• courses: int
classrooms: int
teachers: array of array of int
subjects: array of struct {
course: int
hours: int
classrooms: array of int
teachers: array of int
}

The numbers courses and classrooms denote the number of elements of each type. The array teachers contains one element per teacher: the position $i$ contains the list of forbidden hours for the $i$’th teacher. Hours are identified by a number between 0 (first hour of Monday) and 59 (last hour of Friday). The array subjects contains one element per subject. The numbers subjects[i].course and subjects[i].hours denote the course and the number of weekly sessions of the $i$’th subject, respectively. Courses are identified by a number between 0 and courses-1. Similarly, subjects[i].classrooms and subjects[i].teachers denote the classrooms and teachers compatible with the $i$’th subject. Classrooms are identified by a number between 0 and classrooms-1, whereas teachers are identified with a number between 0 and teachers.size-1.
• planning: array of struct {
classroom: int
teacher: int
hours: array of int
}

The output consists of an array with one element per subject. The fields planning[i].classroom and planning[i].teacher denote the classroom and teacher assigned to the $i$’th subject in subjects. The field planning[i].hours is the array with the hours of the sessions of the $i$’th subject.
Authors: Nil Mamano (adaptation) / Documentation:
 reduction { // Write here your reduction to SAT... } reconstruction { // Write here your solution reconstruction... } To be able to submit you need to either log in, register or become a guest.