By Kevin Smyth (based on joint work with Holger Hoos and Thomas Stützle)
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 MAX-SAT 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.