Iterated Robust Tabu Search for MAX-SAT

MAX-SAT, the optimisation variant of the satisfiability problem in propositional logic, is an important and widely studied combinatorial optimisation problem with applications in AI and other areas of computing science. In this paper, we present a new stochastic local search (SLS) algorithm for MAXSAT that combines Iterated Local Search and Tabu Search, two well-known SLS methods that have been successfully applied to many other combinatorial optimisation problems. The performance of our new algorithm exceeds that of current state-of-the-art MAX-SAT algorithms on various widely studied classes of unweighted and weighted MAX-SAT instances, particularly for Random-3-SAT instances with high variance clause weight distributions. We also report promising results for various classes of structured MAX-SAT instances.

• Type: Conference
• Year: 2003
• Where: AI
• Authors: Kevin Smyth, Holger H. Hoos, Thomas Stützle
• Keywords: AI 2003, Artificial Intelligence, Combinatorial Optimisation Problems, Max-SAT Instances, Weighted Max-sat Instances