Application of satisfiability to examination timetabling

Abstract

This thesis describes approaches for solving non-boolean problems, especially examination timetabling problems, develops and implements three non-boolean procedures--the NB-GSAT procedure, the NB-WalkSAT procedure and the WSAT(OIP) procedure, and uses them on six groups of examination problems and compares the results of the three approaches. When the number of constraints is small (less than 500), the performances of the three procedures do not make much difference. When the number of constraints is larger than 1000, the WSAT(OIP) procedure outperforms the other two procedures, the NB-WalkSAT procedure outperforms the NB-GSAT procedure, with search time especially considered.