Our group has studied fast algorithms for satisfiability testing. We have performed extensive studies on the Davis-Putnam algorithm including a version, C-SAT by Dubois, Andre, Boufkhad and Carlier, and on a randomized algorithm called GSAT, introduced by Selman, Levesque and Mitchell. Some results are discussed in our paper On the Accuracy and Running Time of GSAT.
This research is experimental in character and requires well-designed sets of test cases. These test cases should be in some sense ``hard''. We have studied test cases generated randomly and the associated concept known as the cross-over region. We are also considering several refinements of the cross-over approach.
Interesting test cases can be obtained by encoding hard graph problems (colorability, hamiltonicity) as propositional theories. Also of interest as test cases are encodings of logic puzzles and Ramsey-type combinatorial problems. We are currently using such theories as test cases for experimenting with our version of a constraint satisfaction solver.