求解恰当可满足性问题的随机局部搜索算法  

Stochastic local search algorithm for solving exact satisfiability problem

作　　者：赵星宇 王晓峰[1,2] 杨易 庞立超 杨澜 ZHAO Xingyu;WANG Xiaofeng;YANG Yi;PANG Lichao;YANG Lan(School of Computer Science and Engineering,North Minzu University,Yinchuan Ningxia 750021,China;Key Laboratory of Images&Graphics Intelligent Processing of State Ethnic Affairs Commission(North Minzu University),Yinchuan Ningxia 750021,China)

机构地区：[1]北方民族大学计算机科学与工程学院,银川750021 [2]图像图形智能处理国家民委重点实验室(北方民族大学),银川750021

出　　处：《计算机应用》2024年第3期842-848,共7页journal of Computer Applications

基　　金：国家自然科学基金资助项目(62062001);宁夏青年拔尖人才项目(2021)。

摘　　要：可满足性问题(SAT)是一种NP完全问题,被广泛运用于人工智能和机器学习等研究。恰当可满足性问题(XSAT)是SAT中一类重要的子问题。目前的大部分关于XSAT的研究主要为理论层面,对高效的求解算法特别是具有高效验证性的随机局部搜索算法研究很少。针对以上问题,分析了基础编码和等价编码两种转化方式的公式的部分性质,提出一种直接求解XSAT的随机局部搜索算法WalkXSAT。首先使用随机局部搜索框架进行基础搜索与条件判定;其次加入变元所属文字的恰当不可满足计分值,优先处理不易恰当满足的变元;然后使用防重复选择翻转变元的启发式策略减小搜索空间;最后,采用多种来源以及多种格式的实例进行对比实验。在直接求解XSAT时,相较于ProbSAT,WalkXSAT的变元翻转次数与求解时间显著减少;在求解基础编码转化后的实例中,当实例变元规模大于100时,ProbSAT已失效,而WalkXSAT依然能够在短时间内求解。实验结果表明,所提WalkXSAT精确性高、稳定性强、收敛快。SATisfiability problem(SAT)is a NP complete problem,which is widely used in artificial intelligence and machine learning.Exact SATisfiability problem(XSAT)is an important subproblem of SAT.Most of the current research on XSAT is mainly at the theoretical level,but few efficient solution algorithms are studied,especially the stochastic local search algorithms with efficient verifiability.To address above problems and analyze some properties of both basic and equivalent coding formulas,a stochastic local search algorithm WalkXSAT was proposed for solving XSAT directly.Firstly,the random local search framework was used for basic search and condition determination.Secondly,the appropriate unsatisfiable scoring value of the text to which the variables belonged was added,and the variables that were not easily and appropriately satisfied were prioritized.Thirdly,the search space was reduced using the heuristic strategy of anti-repeat selection of flipped variables.Finally,multiple sources and multiple formats of examples were used for comparison experiments.Compared with ProbSAT algorithm,the number variable flips and the solving time of WalkXSAT are significantly reduced when directly solving the XSAT.In the example after solving the basic encoding transformation,when the variable size of the example is greater than 100,the ProbSAT algorithm is no longer effective,while WalkXSAT can still solve the XSAT in a short time.Experimental results show that the proposed algorithm WalkXSAT has high accuracy,strong stability,and fast convergence speed.

关 键 词：随机局部搜索算法 恰当可满足性问题 可满足性问题 基础编码 等价编码 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]