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

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

的 SWCC 求解器进行了对比.实验结果证明了 PERACC 算法不仅胜过了传统的扩展规则方法,而且大大地缩短
了与国际主流求解器的距离.
实验环境:Arch Linux 16.04 操作系统,12 核 CPU,内存 8GB.对于每一问题测试用例,均将算法执行 50 次,最
终取平均值作为结果.由于本文提出的算法属于不完备算法,所以解决的问题都是可满足性的问题.测试用例来
源于 https://www.cs.ubc.ca/~hoos/SATLIB/index-ubc.html,SWCC 的源代码来源于他的个人主页 https://lcs.ios.ac.
cn/~caisw/SAT.hrml,g2wsat 的源码来源于国际 SAT 比赛官网 https://www.satcompetition.org/.
首先,我们采用处于相变区域的 Uniform Random-3-SAT 问题,不论是对于系统的 SAT 求解器或者是随机的
局部搜索算法都是很难的问题.在以往的扩展规则算法测试中,由于受到求解规模的限制,只能求解一些小规模
的测试用例.而在文献[18]中,ERACC 求解器已经展现出了其强大的求解能力,可以求解先前求解器无法求解的
测试用例.所以在我们的测试中,首先选择了 ERACC 所能求解的规模最大的测试用例.我们选择变量 250、子句
数为 1 065 的规模最大的问题.由于测试用例规模较小,所以该组实验我们将运行 30 秒未结束的测试用例定为
Time out.由表 1 不难看出:传统的 SER 算法已经无法解决规模庞大的测试用例,而 ERACC 算法和 PERACC 算
法显然已经突破了传统算法的限制,发挥了极大的潜力.在这组测试用例中,PERACC 算法的求解效率并没有
ERACC 好.原因在于预处理的过程需要少量的时间,而 ERACC 算法没有预处理的过程.因此,在处理规模相对
较小的问题时,并不能凸显出 PERACC 算法的优势,即先前所能求解的测试用例已经无法凸显我们算法的优势.
在表 1 实验中,我们默认 PERACC 算法在预处理过程中选择 4 个变量,并不确定选择 4 个变量就是最优的
选择.

Table 1 Experiment results on uniform random-3-SAT instances uf250 (CPU time/s)
表 1 随机 3-SAT 测试用例 uf250 实验结果(CPU time/s)
Problem SER ERACC PERACC
uf250-01 Time out 0.021 0.130
uf250-02 Time out 0.089 0.158
uf250-03 Time out 0.056 0.134
uf250-04 Time out 0.006 0.124
uf250-05 Time out 0.047 0.135
uf250-06 Time out 0.016 0.129
uf250-07 Time out 0.043 0.176
uf250-08 Time out 0.061 0.134
uf250-09 Time out 0.088 0.135
uf250-10 Time out 0.002 0.135

带着以上两个问题,我们做出了以下实验.
表 2 选择了图着色问题中一些较难的大型 Random-3-SAT 测试用例.图着色类测试用例包含 200 个顶点和
479 条边,将 GCP 测试用例编译为 SAT 问题后,成为 600 个变量和 2 237 条子句.我们选择以下测试用例的原因
在于它们的复杂性更高,求解时间较长,所以该组实验我们将运行 500 秒未结束的测试用例定为 Time out.这些
测试用例与表 1 相比规模更大,更能突出 PERACC 的性能,符合我们对上述问题的实验论证.
为了测试 SIMT 算法的有效性,我们在表 2 中加入了基于 ERACC 算法,结合了 SIMT 的算法 ERACC+.通过
ERACC 和 ERACC+两组实验我们不难看出:在 21 个测试用例中,ERACC+组有 18 个测试用例优于 ERACC 组,
其中效果最好的一组对比数据提高了 82 倍.而平均时间也提高了近 3.5 倍.由此我们得知,加入 SIMT 算法比单
纯的将初值赋为 1 效果要好很多.
PERACC(i)代表启发式过程中选择 i 个变量.从 ERACC(2)和 PERACC(4)两组数据可以看出:针对比较复杂
的问题,PERACC(4)算法已经比较明显地凸显出了其性能的优势.从这两组数据也不难看出:选择变量的数量越
多,其求解效率越高.结合表 1 分析,虽然 PERACC 算法在启发式阶段花掉了少许时间,但是整体来看,
PERACC(4)比 ERACC 效率提高了 4 倍~25 倍不等,这也符合了磨刀不误砍柴工的道理.
我们将继续延伸我们的思路,加入了当前国际著名的局部搜索求解器 SWCC 进行对比.从数据上不难看出,
PERACC 比 ERACC 的效率提升了 1.6 倍~117 倍不等.虽然 PERACC 的求解效率并没有超过 SWCC 求解器,但