Backbone guided local search for maximum satisfiability

Maximum satisfiability (Max-SAT) is more general and more difficult to solve than satisfiability (SAT). In this paper, we first investigate the effectiveness of Walksat, one of the best local search algorithms designed for SAT, on Max-SAT. We show that Walksat is also effective on Max-SAT, while its effectiveness degrades as the problem is more constrained. We then develop a novel method that exploits the backbone information in the local minima from Walk-sat and applies the backbone information in different ways to improve the performance of the Walk-sat algorithm. We call our new algorithm backbone guided Walksat (BGWalksat). On large random SAT and Max-SAT problems as well as instances from the SATLIB, BGWalksat significantly improves Walk-sat's performance.