Boosting SLS performance by incorporating resolution-based preprocessor
Anbu Anbulagan, Duc Nghia Pham, John Slaney, Abdul Rahman Sattar · ANU Open Research (Australian National University) · 2006
State of the art Stochastic Local Search (SLS) solvers have difficulty in solving many CNF-encoded realistic SAT problems, apparently because they are unable to exploit hidden structure as well as systematic solvers. Recent work has shown that SLS solvers may benefit from a preprocessing phase borrowed from systematic SAT solving. In this paper, we report an extensive empirical examination of the impact of SAT preprocessing on the performance of contemporary SLS solvers. It emerges that all the examined solvers do indeed benefit from preprocessing, and the effect of each preprocessor is close to uniform across solvers and across problems. Our results suggest that SLS solvers need to be equipped with multiple preprocessors if they are ever to match the performance of systematic solvers on highly structured problems.