Improving probability selecting based weights for Satisfiability Problem
This addresses a gap in SAT solving for AI applications, but it is incremental as it builds on existing SLS methods.
The paper tackles the problem of solving both uniform random k-SAT and hard random SAT (HRS) by introducing a new stochastic local search algorithm called SelectNTS, which outperforms state-of-the-art algorithms on benchmark instances from SAT Competitions and randomly generated problems.
The Boolean Satisfiability problem (SAT) is important on artificial intelligence community and the impact of its solving on complex problems. Recently, great breakthroughs have been made respectively on stochastic local search (SLS) algorithms for uniform random k-SAT resulting in several state-of-the-art SLS algorithms Score2SAT, YalSAT, ProbSAT, CScoreSAT and on a hybrid algorithm for hard random SAT (HRS) resulting in one state-of-the-art hybrid algorithm SparrowToRiss. However, there is no an algorithm which can effectively solve both uniform random k-SAT and HRS. In this paper, we present a new SLS algorithm named SelectNTS for uniform random k-SAT and HRS. SelectNTS is an improved probability selecting based local search algorithm for SAT problem. The core of SelectNTS relies on new clause and variable selection heuristics. The new clause selection heuristic uses a new clause weighting scheme and a biased random walk. The new variable selection heuristic uses a probability selecting strategy with the variation of CC strategy based on a new variable weighting scheme. Extensive experimental results on the well-known random benchmarks instances from the SAT Competitions in 2017 and 2018, and on randomly generated problems, show that our algorithm outperforms state-of-the-art random SAT algorithms, and our SelectNTS can effectively solve both uniform random k-SAT and HRS.