Improving probability selecting based weights for Satisfiability Problem

TL;DR

This paper introduces SelectNTS, a novel local search algorithm with new heuristics that effectively solves both uniform random k-SAT and HRS, outperforming existing state-of-the-art algorithms on benchmark instances.

Contribution

The paper presents SelectNTS, a new probability selecting based local search algorithm with innovative clause and variable heuristics for solving diverse SAT problems.

Findings

SelectNTS outperforms existing algorithms on benchmark instances.

It effectively solves both uniform random k-SAT and HRS.

Experimental results demonstrate superior performance on SAT competition benchmarks.

Abstract

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.