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

2752 Journal of Software 软件学报 Vol.32, No.9, September 2021

是相对于当前扩展规则领域最高效的 ERACC 而言,PERACC 已大大地缩短了与 SWCC 的距离.
Table 2 Experiment results on graph Colouring instances flat200-479 (CPU time/s)
表 2 图着色测试用例 flat200-479 实验结果(CPU time/s)
Problem ERACC ERACC+ PERACC(2) PERACC(4) SWCC
flat200-4 40.544 4.714 1.191 7.054 0.058
flat200-10 7.481 19.696 7.671 3.426 0.071
flat200-12 179.901 2.206 4.791 1.533 0.023
flat200-26 24.011 3.776 1.603 2.052 0.156
flat200-32 6.941 2.521 0.637 1.011 0.105
flat200-36 12.237 7.709 0.577 0.884 0.169
flat200-39 230.423 44.138 4.218 4.411 0.236
flat200-44 5.144 0.764 0.251 0.326 0.161
flat200-45 9.331 0.733 1.869 0.491 0.037
flat200-46 8.229 2.762 0.462 0.259 0.045
flat200-48 14.327 4.465 0.924 2.417 0.566
flat200-49 5.532 0.719 1.684 0.536 0.052
flat200-55 26.241 1.425 1.232 1.904 Time out
flat200-60 5.364 9.375 1.808 1.519 0.066
flat200-72 45.634 19.326 10.054 7.889 0.211
flat200-82 5.088 4.522 0.972 0.766 0.113
flat200-83 13.901 8.599 6.783 2.266 0.384
flat200-87 17.189 31.681 1.413 0.242 0.272
flat200-88 26.887 0.946 0.374 0.273 0.079
flat200-94 8.945 1.038 3.754 0.581 0.162
flat200-99 42.392 28.262 2.514 0.775 0.074
统计结果 735.742 199.377 54.782 40.615 3.04
我们将实验的证明继续扩大化,选择了 AIM 类问题.该类问题结构性很强,变量个数以及正负文字比例存在
一定规律,解的个数只有一个,求解难度较高.1_6 和 2_0 代表子句与变量的比率,测试用例的变量为 100 个.所以,
我们将运行 1 200s 未结束的测试用例定为 Time out.
从表 3 可以看出:在前 4 个测试用例中,并没有拉开 PERACC 和 ERACC 的差距,g2wsat 在规定时间内未找
到解,SWCC 的数据两极分化比较严重;后 4 个测试用例中,仍然体现出了 PERACC 的高效性,并且大大地拉开了
与 g2wsat 的求解差距.虽然在多半用例,我们仍然无法超越 SWCC.我们分析:对于结构性较强的 AIM 类问题,
局部搜索求解结构 SAT 问题并不占优势.对于少数测试结果,PERACC 算法超过了 SWCC 求解器,这在扩展规则
领域是史无前例的,从中也看出扩展规则方法在求解 SAT 问题上的巨大潜力.
Table 3 Experiment results on AIM instances (CPU time/s)
表 3 AIM 类问题测试实验结果(CPU time/s)
Problem ERACC PERACC SWCC g2wsat
aim-100-1_6-yes1-1 1 078.164 957.043 345.605 Time out
aim-100-1_6-yes1-2 933.439 895.485 338.992 Time out
aim-100-1_6-yes1-3 801.674 821.801 0.018 Time out
aim-100-1_6-yes1-4 753.224 740.931 0.017 Time out
aim-100-2_0-yes1-1 45.142 1.876 76 0.015 45.463
aim-100-2_0-yes1-2 21.203 1.033 97 160.536 17.531
aim-100-2_0-yes1-3 6.438 1.375 56 2.151 10.831
aim-100-2_0-yes1-4 16.321 0.151 98 3.362 235.010 6

以上实验结果表明:PERACC 算法在求解复杂性较高、规模较大的测试用例时,更能凸显 PERACC 的高效
性能,同时缩短了与 SWCC 求解器的差距,得到了比较良好的效果.
基于扩展规则的推理方式本身是与归结方法截然相反的求解过程,它是从问题的解空间入手来寻求答案.
基于扩展规则的 ERACC 算法相比于成熟的局部搜索求解器确有不足,因此,我们在原有基础上做出了一系列
改进,进一步研究扩展规则的适用性.我们相信,虽然扩展规则推理方法还处于初级阶段,但与不完备的局部搜
索方法相结合,必将发挥出它更大的潜力.