Focused random walk with configuration checking and break minimum for satisfiability

Stochastic local search (SLS) algorithms, especially those adopting the focused random walk (FRW) framework, have exhibited great effectiveness in solving satisfiable random 3-satisfiability (3-SAT) instances. However, they are still unsatisfactory in dealing with huge instances, and are usually sensitive to the clause-to-variable ratio of the instance. In this paper, we present a new FRW algorithm dubbed FrwCB, which behaves more satisfying in the above two aspects. The main idea is a new heuristic called CCBM, which combines a recent diversification strategy named configuration checking (CC) with the common break minimum (BM) variable-picking strategy. By combining CC and BM in a subtle way, CCBM significantly improves the performance of FrwCB, making FrwCB achieve state-of-the-art performance on a wide range of benchmarks. The experiments show that FrwCB significantly outperforms state-of-the-art SLS solvers on random 3-SAT instances, and competes well on random 5-SAT, random 7-SAT and structured instances.