改进的基于概率选择权的可满足性问题
Improving probability selecting based weights for Satisfiability Problem
摘要：
布尔可满足性问题（SAT）是人工智能领域的一个重要问题，也是其求解对复杂问题影响的一个重要方面。近年来，在均匀随机k-SAT问题的随机局部搜索（SLS）算法和硬随机SAT问题的混合算法上分别取得了突破性进展，提出了Score 2SAT，YalSAT，ProbSAT，CScoreSAT等几种最新的SLS算法，并提出了SparrowToRiss等一种最新的混合算法。然而，目前还没有一种算法可以有效地解决均匀随机k-SAT和HRS。本文针对均匀随机k-SAT和HRS提出了一种新的SLS算法SelectNTS。SelectNTS是一种改进的基于概率选择的局部搜索算法。SelectNTS的核心是新子句和变量选择算法。新子句选择启发式算法使用新子句加权方案和有偏随机游走。新的变量选择启发式算法采用一种概率选择策略，并基于一种新的变量加权方案对CC策略进行了改进。在2017年和2018年SAT竞赛中的著名随机基准测试实例以及随机生成的问题上进行的大量实验结果表明，我们的算法优于最先进的随机SAT算法，并且我们的SelectNTS可以有效地解决均匀随机k-SAT和HRS。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
