Adding New Clauses for Faster Local Search

Abstract

A primary concern when using local search methods for CNF satisfiability is how to get rid of local minimas. Among many other heuristics, Weighting by Morris (1993) and Selman and Kautz (1993) works overwhelmingly better than others (Cha and Iwama 1995). Weighting increases the weight of each clause which is unsatisfied at a local minima. This paper introduces a more sophisticated weighting strategy, i.e., adding new clauses (ANC) that are unsatisfied at the local minima. As those new clauses, we choose resolvents of the clauses unsatisfied at the local minima and randomly selected neighboring clauses. The idea is that ANC is to make the slope of search space more smooth than the simple weighting. Experimental data show that ANC is faster than simple weighting: (i) When the number of variables is 200 or more, ANC is roughly four to ten times as fast as weighting in terms of the number of search steps. (ii) It might be more important that the divergence of computation time for each try ...