I used a SAT solver awhile ago to build a program that scheduled retail employees based on preferences set by both the employer and the employees.