Comprehensive score: towards efficient local search for SAT with long clauses

摘要: 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 on random k-SAT instances. Compared to 3-SAT instances which have special statistical properties rendering them easy solve, with long clauses are similar structured ones and remain very difficult. This paper devoted efficient clauses. By combining a novel variable property subscore commonly used score, we design scoring function named comprehensive utilized develop new algorithm called CScoreSAT. The experiments show CScoreSAT outperforms state-of-the-art solvers, including winners recent SAT competitions, by one two orders magnitudes large 5-SAT 7-SAT In addition, significantly its competitors each k = 4; 5; 6; 7 from Challenge 2012, indicates robustness.