Combining Intensification and Diversification in Local Search for SAT

The propositional satisfiability problem (SAT) is to determine whether there is a truth assignment to Boolean variables such that every clause in conjunctive normal form is satisfied. Intensification refers to search strategies that intend to greatly improve a solution, while diversification refers to search strategies that help achieve a reasonable coverage in the search space. Roughly speaking, there are three classes of local search algorithms for solving SAT: non-weighting, clause weighting, and variable weighting. A non-weighting algorithm mainly focuses on intensifying the search. A clause weighting algorithm and a variable weighting algorithm use clause and variable weighting, respectively, to diversify the search.;One way to design a local search algorithm that is effective on many types of instances is allowing it to switch among heuristics in order to combine the strengths of these heuristics and eliminate the weaknesses of them. Two novel switching criteria, namely the evenness or unevenness of distribution of variable weights and the evenness or unevenness of distribution of clause weights, are proposed. These criteria are applied to our newly proposed heuristics and state-of-the-art heuristics. The resulting local search algorithms are FH (Four Heuristics), Hybrid, and NCVW (Non-, Clause, and Variable Weighting), each of which switches among two to four heuristics according to one or two of the proposed criteria in order to intensify or diversify the search when necessary.;FH, Hybrid, and NCVW have two main characteristics in common. First, they all combine intensification strategies with suitable diversification strategies. Second, they all intensify or diversify the search when necessary.;Experimental results show that, on a wide range of instances, each of algorithms FH, Hybrid, and NCVW exhibits generally better performance than its constituent heuristics. In addition, on a wide range of instances, each algorithm is generally effective, while state-of-the-art local search algorithms that include the best local search algorithms in the international SAT 2005 or SAT 2007 competitions, are not. Moreover, on representative instances, each algorithm shows better overall performance than 10 state-of-the-art local search algorithms, including the best local search algorithms in the international SAT 2005 and SAT 2007 competitions.