Guided Local Search for Solving SAT and Weighted MAX-SAT Problems

In this paper, we show how Guided Local Search (GLS) can be applied to the SAT problem and show how the resulting algorithm can be naturally extended to solve the weighted MAX-SAT problem. GLS is a general, penalty-based metaheuristic, which sits on top of local search algorithms to help guide them out of local minima. GLS has been shown to be successful in solving a number of practical real life problems, such as the travelling salesman problem, BT's workforce scheduling problem, the radio link frequency assignment problem and the vehicle routing problem. We present empirical results of applying GLS to instances of the SAT problem from the DIMACS archive and also a small set of weighted MAX-SAT problem instances and compare them against the results of other local search algorithms for the SAT problem.

• Type: Journal
• Year: 2000
• Where: JAR
• Authors: Patrick Mills, Edward P. K. Tsang
• Keywords: JAR 2000, Local Search, Travelling Salesman Problem, Weighted Max-sat Problem