Local Search Strategies for Satisfiability Testing
Bart Selman, Henry Kautz, Bram Cohen · 1995
It has recently been shown that local search is surprisingly good at finding satisfying assignments for certain classes of CNF formulas (Selman et al. 1992). In this paper we demonstrate that the power of local search for satisfiability testing can be further enhanced by employing a new strategy, called "mixed random walk", for escaping from local minima. We present a detailed comparison of this strategy with simulated annealing, and show that mixed random walk is the superior strategy on several classes of computationally difficult problem instances. We also present results demonstrating the effectiveness of local search with walk for solving circuit synthesis and diagnosis problems. Finally, we show that mixed random walk improves upon the results of Hansen and Jaumard on MAX-SAT problems. 1 Introduction Local search algorithms have been successfully applied to many optimization problems. Hansen and Jaumard (1990) describe experiments using local search for MAX-SAT, i.e., the prob...