Experiment al Results on the Application of Sat isfiability Algorithms to Scheduling Problems
James M. Crawford, Andrew B. Baker · 1994
Considerable progress has been made in recent years in understanding and solving propositional satisfiability 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" constraintsatisfaction 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 pr...