Scoring functions based on second level score for κ-SAT with long clauses

It is widely acknowledged that stochastic local search (SLS) algorithms can efficiently find models for satisfiable instances of the satisfiability (SAT) problem, especially for random κ-SAT instances. However, compared to random 3-SAT instances where SLS algorithms have shown great success, random κ-SAT instances with long clauses remain very difficult. Recently, the notion of second level score, denoted as score₂, was proposed for improving SLS algorithms on long-clause SAT instances, and was first used in the powerful CCASat solver as a tie breaker. In this paper, we propose three new scoring functions based on score₂. Despite their simplicity, these functions are very effective for solving random κ-SAT with long clauses. The first function combines score and score₂, and the second one additionally integrates the diversification property age. These two functions are used in developing a new SLS algorithm called CScoreSAT. Experimental results on large random 5-SAT and 7-SAT instances near phase transition show that CScoreSAT significantly outperforms previous SLS solvers. However, CScoreSAT cannot rival its competitors on random κ-SAT instances at phase transition. We improve CScoreSAT for such instances by another scoring function which combines score2 with age. The resulting algorithm HScoreSAT exhibits state-of-the-art performance on random κ-SAT (κ > 3) instances at phase transition. We also study the computation of score₂, including its implementation and computational complexity.