Experimental Results on the Application of Satisfiability Algorithms to Scheduling Problems

Planning and Scheduling

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 12

Scheduling

Considerable progress has been made in recent years in understanding and solving propositional satisfiabilit y problems. Much of this work has been based on experiments on randomly generated 3SAT problems . One generally accepted shortcoming of this work is that it is not clear how the results and algorithms developed will carry over to "real" constraint-satisfaction problems. This paper reports on a series of experiments applying satisfiability algorithms to scheduling problems. We have found that scheduling problems bear fairly little resemblance to the previously studied hard randomly generated 3SAT problems. In particular, scheduling problems tend to be quite large but under-constrained, Further, forward checking (e.g., unit propagation) seems to be much more important on these problems than on hard random 3SAT problems. We have also found that the domain-specific heuristics developed to solve scheduling problems make surprisingly little difference in the time required to solve the problems. We suggest that the best algorithms for this problem class will probably be hill-climbing algorithms that incorporate some sort of forward checking.