Scoring Functions Based on Second Level Score for K-SAT with Long Clauses

Abstract

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 k-SAT instances. However, compared to random 3-SAT instances where SLS algorithms have shown great success, random k-SAT instances with long clauses remain very difficult. Recently, the notion of second level score, denoted as score2, 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 score2. Despite their simplicity, these functions are very effective for solving random k-SAT with long clauses. The first function combines score and score2, 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 k-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 k-SAT (k > 3) instances at phase transition. We also study the computation of score2, including its implementation and computational complexity.