Comprehensive Score: Towards Efficient Local Search for SAT with Long Clauses

Abstract

It is widely acknowledged that stochastic local search (SLS) algorithms can efficiently find models of satisfiable formulae for the Boolean Satisfiability (SAT) problem. There has been much interest in studying SLS algorithms on random k-SAT instances. Compared to random 3-SAT instances which have special statistical properties rendering them easy to solve, random k-SAT instances with long clauses are similar to structured ones and remain very difficult. This paper is devoted to efficient SLS algorithms for random k-SAT instances with long clauses. By combining a novel variable property subscore with the commonly used property score, we design a scoring function named comprehensive score, which is utilized to develop a new SLS algorithm called CScoreSAT. The experiments show that CScoreSAT outperforms state-of-the-art SLS solvers, including the winners of recent SAT competitions, by one to two orders of magnitudes on large random 5-SAT and 7-SAT instances. In addition, CScoreSAT significantly outperforms its competitors on random k-SAT instances for each k = 4, 5, 6, 7 from SAT Challenge 2012, which indicates its robustness.