A randomized diversification strategy for solving satisfiability problem with long clauses  

作　　者：Jian GAO Ruizhi LI Minghao YIN 

机构地区：[1]College of Computer Science, Northeast Normal University [2]College of Information Science and Technology, Dalian Maritime University [3]Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education,Jilin University

出　　处：《Science China(Information Sciences)》2017年第9期117-127,共11页中国科学（信息科学）（英文版）

基　　金：supported by National Natural Science Foundation of China (Grant Nos. 61370156, 61402070, 61503074);Program for New Century Excellent Talents in University (Grant No. NCET13-0724);Natural Science Foundation of Liaoning Province (Grant No. 2015020023)

摘　　要：Satisfiability problem （SAT） is a central problem in artificial intelligence due to its computational complexity and usefulness in industrial applications. Stochastic local search （SLS） algorithms are powerful to solve hard instances of satisfiability problems, among which CScoreSAT is proposed for solving SAT instances with long clauses by using greedy mode and diversification mode. In this paper, we present a randomized variable selection strategy to improve efficiency of the diversification mode, and thus propose a new SLS algorithm. We perform a number of experiments to evaluate the new algorithm comparing with the recently proposed algorithms, and show that our algorithm is comparative with others for solving random instances near the phase transition threshold.Satisfiability problem （SAT） is a central problem in artificial intelligence due to its computational complexity and usefulness in industrial applications. Stochastic local search （SLS） algorithms are powerful to solve hard instances of satisfiability problems, among which CScoreSAT is proposed for solving SAT instances with long clauses by using greedy mode and diversification mode. In this paper, we present a randomized variable selection strategy to improve efficiency of the diversification mode, and thus propose a new SLS algorithm. We perform a number of experiments to evaluate the new algorithm comparing with the recently proposed algorithms, and show that our algorithm is comparative with others for solving random instances near the phase transition threshold.

关 键 词：SAT local search randomized diversification strategy phase transition long clause 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]