Page 121 - 《软件学报》2021年第9期

李壮 等:基于局部搜索的并行扩展规则推理方法 2745

algorithm, the proposed algorithm not only can improve the efficiency of solution, but also can solve larger benchmark, which makes the
extension rule method break through the limitation of formula size again.
Key words: automated reasoning; local search; extension rule; configuration checking; parallel framework

可满足性问题(SAT)是公认的第一个 NP-完全问题,是人工智能领域最重要的研究方向之一.自人工智能发
展初期就引起了研究者的广泛关注,当今 SAT 求解器已能够解决很多现实问题.近年来,国内外的学者致力于求
解 SAT 问题的效率和求解能力,提出了多种方法.
1992 年,Selman 等人提出的 GSAT 算法证明了局部搜索算法可以应用于求解 SAT 问题,其强大的求解能力
[1]
为局部搜索求解 SAT 问题奠定了基础 .随着局部搜索方法在该领域的广泛应用,自 2002 年 SAT 比赛的开展以
来,众多基于局部搜索算法的求解器也相继问世并展现出了各自强大的求解能力.2005 年,Li 等人提出了 g2wsat
[2]
类算法,该算法结合随机选择和贪心双模式,在求解的过程中展现出良好的性能 .2011 年,Li 等人提出了利用变
[3]
量可满足历史记录的局部搜索求解器 SatTime,获得 SAT 2011 随机组银奖 .2016 年,KhudaBukhsh 等人提出了
[4]
SATenstein 求解框架,该框架结合了多个高性能局部搜索求解器,其求解效果胜过多个主流求解器 .近年来,由
Cai 等人提出的基于局部搜索的格局检测策略成为 SAT 比赛中最具影响力的策略之一.2011 年,Cai 等人设计的
[5]
SWCC 算法及相关求解器皆使 SAT 求解器的计算能力得到巨大地提升,并取得惊人的成绩 .随后,Cai 等人于
[6]
2012 年提出的 CCASat 获得 SAT 2012 年随机组金奖 .2014 年,Cai 等人提出的 CSCCSat 获得 SAT 2014 年比
[7]
赛 Hard-combinatorial 组铜奖和 SAT 2016 比赛 Random track 组银奖 .同时,基于局部搜索的格局检测策略用于
求解 Max-SAT 问题也取得了巨大的成功 [8,9] ,其中,CCLS 在 MAX-SAT 2013 非完备性求解器组中获得 4 项金奖.
2018 年,Cai 等人基于局部搜索算法,在完备算法上设计了 ReasonLS 求解器,并在同年 SAT 国际比赛中获得 No-
Limits track 组金奖 [10] .以上不难看出,局部搜索算法的广泛应用和强大的效率已得到不断突破.
经典的 SAT 求解器大多基于 DPLL 算法和归结方法,2003 年,Lin 等人提出的扩展规则方法打破了传统思
维的限制,开辟了 SAT 求解的新思路 [11] .作为归结方法的互补方法,通过寻找子句的极大项来判断 CNF 公式的
可满足性.他提出的 ER 算法得到了国内外的广泛认可,并为日后的研究打下了坚实的基础.基于 ER 的算法,Lin、
Wu、李莹和张立明等人分别提出了 IER [11] ,RER [12] ,NER [13] ,SER [14] 等算法,将完备的 ER 算法的求解效率提升了
几个数量级的高度.在扩展规则的应用方面,2010 年,殷明浩等人在可能性扩展规则的基础上提出了 EPPCCCL
理论,可作为可能性知识编译的目标语言 [15] .2016 年,刘磊等人提出了扩展反驳方法,并在该推理方法与知识编
译之间建立了联系 [16] .2017 年,王强等人提出两种加速#SAT 求解的启发式策略,提出了 CER_MW 和 CER_
LC&MW 两种算法,其求解速度是其他算法的 1.4 倍~100 倍,求解能力也在限定时间内可解更多的测试用例 [17] .
2018 年,杨洋等人在 SWCC 算法的基础上提出了 ERACC 算法,该算法突破了传统扩展规则推理对公式规模的
局限,求解效率有了极大提高 [18,19] .
不仅如此,各种经典的技术也相继应用于扩展规则求解的过程中,如启发式和并行处理等技术.2009 年,李
莹等人针对 IER 算法提出了 IMOM 和 IBOHM 两种启发式,其求解效率较 IER 提高了 10 倍~200 倍 [20] .Zhang
等人基于其 PSER 的半扩展规则策略提出了分割解空间的 PPSER 算法,证明了该算法具有合理的执行效率,并
优于 NER、DR、IER 等算法 [21] .
由以上不难看出,基于扩展规则的推理方法如今已得到了广泛的应用.但与局部搜索等推理方法相比,仍然
具有很大的提升空间和完善度.本文基于 ERACC 算法,从李莹的 IMOM 启发式算法和张立明的 PPSER 并行算
法中得到启示,提出了 PERACC 算法.该算法基于杨洋等人 [18,19] 的 ERACC 算法,调用启发式算法 CPVI,通过选
择变量并调用 PERM 算法,用变量的组合将原解空间分割成不同的子空间,每个子空间通过 SIMT 算法选择初
始极大项,随后进行并行处理.最后实验证明,该算法较 ERACC 算法的求解效率有较大的提高 [22] .
本文第 1 节介绍了局部搜索和扩展规则的基础知识并给出了相关定义.第 2 节提出启发式策略 CPVI 算法、
并行处理策略 PERM 算法和变量赋初始值策略 SIMT 算法,并将它们有机结合,在 ERACC 算法基础上提出了
PERACC 算法.第 3 节进行了实验的对比,证明了我们的算法在特定的问题上较原算法快出 1.6 倍~117 倍不等.