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 courses1. 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 classrooms1, whereas teachers
are identified with a number between 0 and teachers.size1.

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.