 |
    |
A Method to Avoid Duplicative Flipping in Local Search for SAT
Thach-Thao Duong, Duc Nghia Pham, and Abdul Sattar
Queensland Research Laboratory, NICTA and Institute for Integrated and Intelligent Systems, Griffith University, QLD, Australiathao.duong@nicta.com.au
duc-nghia.pham@nicta.com.au
abdul.sattar@nicta.com.au
Abstract. Stochastic perturbation on variable flipping is the key idea of local search for SAT. Observing that variables are flipped several times in an attempt to escape from a local minimum, this paper presents a duplication learning mechanism in stagnation stages to minimise duplicative variable flipping. The heuristic incorporates the learned knowledge into a variable weighting scheme to effectively prevent the search from selecting duplicative variables. Additionally, probability-based and time window smoothing techniques are adopted to eliminate the effects of redundant information. The integration of the heuristic and gNovelty + was compared with the original solvers and other state-of-the-art local search solvers. The experimental results showed that the new solver outperformed other solvers on the full set of SAT 2011 competition instances and three sets of real-world verification problems.
LNAI 7691, p. 218 ff.
lncs@springer.com
© Springer-Verlag Berlin Heidelberg 2012