Byungki Cha

AAAI Conference 1997 Conference Paper

Local Search Algorithms for Partial MAXSAT

• Byungki Cha
• Yahiko Kambayashi

AAAI Conference 1996 Conference Paper

Adding New Clauses for Faster Local Search

• Byungki Cha

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.

IJCAI Conference 1995 Conference Paper

Performance Test of Local Search Algorithms Using New Types of Random CNF Formulas

• Byungki Cha
• Kazuo lwama

New types of test-instance generators have been developed for generating random CNF (Conjunctive Normal Form) formulas with controlled attributes. In this paper, we use these generators to test the performance of localsearch-based SAT algorithms. For this purpose, the generator which produces formulas having exactly one satisfying truth assignment is especially desirable. It is shown that (i) among several different strategies of local search, the weighting strategy is overwhelmingly faster than the others and that (ii) local search works significantly better for instances of larger clause/variable ratio, which allows us to come up with a new strategy for making local search even faster.