An effective variable selection heuristic in SLS for weighted Max-2-SAT

Stochastic local search (SLS) is an appealing method for solving the maximum satisfiability (Max‐SAT) problem. This paper proposes a new variable selection heuristic for Max‐SAT local search algorithms, which works particularly well for weighted Max‐2‐SAT instances. Evolving from the recent configuration checking strategy, this new heuristic works in three levels and is called CCTriplex. According to the CCTriplex heuristic, a variable that is both decreasing and configuration changed has the higher priority to be flipped than a decreasing variable, which in turn has the higher priority than a configuration changed variable. The CCTriplex heuristic is used to develop a new SLS algorithm for weighted Max‐2‐SAT called CCMaxSAT. We evaluate CCMaxSAT on random benchmarks with different densities, and the hand crafted Frb benchmark, as well as weighted Max‐2‐SAT instances encoded from MaxCut, MaxClique and sports scheduling problems. Compared with the state‐of‐the‐art SLS solver for weighted Max‐2‐SAT called ITS and the best SLS solver in Max‐SAT Evaluation 2012 namely ubcsat‐IRoTS, as well as the famous complete solver wMaxSATz, our algorithm CCMaxSAT shows rather good performance on all the benchmarks.