Adding New Clauses for Faster Local Search

No. 1: Agents, AI in Art and Entertainment, Knowledge Representation, and Learning

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 13

Stochastic Search

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 is much smaller in ANC than in weighting. (iii) There are several possible reasons for ANC’s superiority, one of which is that ANC returns the same local minima much less frequently than weighting.