×

zbMATH — the first resource for mathematics

A switching criterion for intensification and diversification in local search for SAT. (English) Zbl 1159.68571
Summary: We propose a new switching criterion, namely the evenness or unevenness of the distribution of variable weights, and use this criterion to combine intensification and diversification in local search for SAT. We refer to the ways in which state-of-the-art local search algorithms adaptG\(^2{\text{WSAT}}_{\text P}\) and VW select a variable to flip, as heuristic adaptG\(^2{\text{WSAT}}_{\text P}\) and heuristic VW, respectively. To evaluate the effectiveness of this criterion, we apply it to heuristic adaptG\(^2{\text{WSAT}}_{\text P}\) and heuristic VW, in which the former intensifies the search better than the latter, and the latter diversifies the search better than the former. The resulting local search algorithm, which switches between heuristic adaptG\(^2{\text{WSAT}}_{\text P}\) and heuristic VW in every step according to this criterion, is called Hybrid.
Our experimental results show that, on a broad range of SAT instances presented in this paper, Hybrid inherits the strengths of adaptG\(^2{\text{WSAT}}_{\text P}\) and VW, and exhibits generally better performance than adaptG\(^2{\text{WSAT}}_{\text P}\) and VW. In addition, Hybrid compares favorably with state-of-the-art local search algorithm R+adaptNovelty+ on these instances. Furthermore, without any manual tuning parameters, Hybrid solves each of these instances in a reasonable time, while adaptG\(^2{\text{WSAT}}_{\text P}\), VW, and R+adaptNovelty+ have difficulty on some of these instances.
MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Software:
UnitWalk; QingTing1
PDF BibTeX XML Cite