Weight-enhanced diversification in stochastic local search for satisfiability

Thach-Thao Duong, Duc Nghia Pham, Abdul Rahman Sattar, M. A. Hakim Newton · University of Southern Queensland ePrints (University of Southern Queensland) · 2013

Intensification and diversification are the key fac-tors that control the performance of stochastic lo-cal search in satisfiability (SAT). Recently, Novelty Walk has become a popular method for improving diversification of the search and so has been inte-grated in many well-known SAT solvers such as TNM and gNovelty+. In this paper, we introduce new heuristics to improve the effectiveness of Nov-elty Walk in terms of reducing search stagnation. In particular, we use weights (based on statistical in-formation collected during the search) to focus the diversification phase onto specific areas of interest. With a given probability, we select the most fre-quently unsatisfied clause instead of a totally ran-dom one as Novelty Walk does. Amongst all the variables appearing in the selected clause, we then select the least flipped variable for the next move. Our experimental results show that the new weight-enhanced diversification method significantly im-proves the performance of gNovelty+ and thus out-performs other local search SAT solvers on a wide range of structured and random satisfiability bench-marks. 1

Read the paper · More papers on PaperTik