扩展规则推理方法在经典的可满足性问题求解中已得到广泛应用,若干个基于扩展规则的推理方法已被提出,皆得到国内外的认可,例如完备的NER,IMOMH_IER,PPSER算法以及基于局部搜索的不完备算法ERACC等,都具有良好的求解效果.其中,ERACC算法是当前扩展规则求解器中求解效率最高、能力最强的算法.但是,串行的ERACC算法在启发式和预处理上仍然具有可提升的空间.基于此,设计了相应的并行框架,提出了PERACC算法.该算法基于格局检测的局部搜索方法,从变量赋初始值、化简解空间和启发式这3个阶段出发,将原极大项空间分解成为若干极大项子空间,并对原子句集进行化简后,并行处理各个子空间.通过实验显示:该算法与原算法相比,不仅在求解效率方面有较大提高,而且可以求解规模更大的测试用例,使扩展规则方法再次突破公式规模的限制.
Extension rule reasoning method has been widely used in solving the classical satisfiability problem. Several reasoning methods based on extension rule have been proposed, which have been recognized around the world. These methods include the complete algorithms like NER, IMOMH_IER, PPSER, and local search-based incomplete algorithm like ERACC. All of them have sound performance. ERACC algorithm is the most efficient and powerful algorithm in the current extension rule solver. However, the serial algorithm ERACC still needs improvement on heuristics and preprocessing. Therefore, a parallel framework is designed and it is called PERACC algorithm. Based on the configuration checking of local search method, the algorithm decomposes the original maximum term space into several maximum term subspaces, from three stages of assigning initial values to variables, simplifying solution space, and heuristic, simplifying the original clause set, then processing each subspace in parallel. Experiments show that, compared with the original 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.
可满足性问题(SAT)是公认的第一个NP-完全问题, 是人工智能领域最重要的研究方向之一.自人工智能发展初期就引起了研究者的广泛关注, 当今SAT求解器已能够解决很多现实问题.近年来, 国内外的学者致力于求解SAT问题的效率和求解能力, 提出了多种方法.
1992年, Selman等人提出的GSAT算法证明了局部搜索算法可以应用于求解SAT问题, 其强大的求解能力为局部搜索求解SAT问题奠定了基础[
经典的SAT求解器大多基于DPLL算法和归结方法, 2003年, Lin等人提出的扩展规则方法打破了传统思维的限制, 开辟了SAT求解的新思路[
不仅如此, 各种经典的技术也相继应用于扩展规则求解的过程中, 如启发式和并行处理等技术.2009年, 李莹等人针对IER算法提出了IMOM和IBOHM两种启发式, 其求解效率较IER提高了10倍~200倍[
由以上不难看出, 基于扩展规则的推理方法如今已得到了广泛的应用.但与局部搜索等推理方法相比, 仍然具有很大的提升空间和完善度.本文基于ERACC算法, 从李莹的IMOM启发式算法和张立明的PPSER并行算法中得到启示, 提出了PERACC算法.该算法基于杨洋等人[
本文第1节介绍了局部搜索和扩展规则的基础知识并给出了相关定义.第2节提出启发式策略CPVI算法、并行处理策略PERM算法和变量赋初始值策略SIMT算法, 并将它们有机结合, 在ERACC算法基础上提出了PERACC算法.第3节进行了实验的对比, 证明了我们的算法在特定的问题上较原算法快出1.6倍~117倍不等.
SAT问题的求解是按照某种特定规则对变量进行选取、赋值和剪枝等过程, 找到可满足的解释.完备的算法如DPLL, 其功能在于不仅可以判断子句集的可满足性, 而且可以找到可满足的解.局部搜索作为不完备的方法采取完全不同的方式对SAT问题进行求解, 该方法通过不断变换部分子句空间所有变量赋值使得可满足的子句不断增加, 最终达到子句集可满足的目的.当处理不可满足的问题时, 由于子句集无解而使变量赋值无限地变换下去.因此, 局部搜索只能求解可满足的子句集, 且其求解效率远高于完备的算法, 却无法处理不可满足的子句集.
传统的归结方法是通过归结出空子句来判断子句集不可满足; 而作为归结的互补方法, 扩展规则是通过对CNF公式中的子句能否扩展出所有极大项来判断其可满足性.其基本定义如下.
初始的扩展规则推理方法是通过计数每个子句所能扩展出的极大项个数, 利用容斥原理计算所能扩展出极大项总数.如果极大项个数是2
基于局部搜索的扩展规则推理方法的本质在于: 以寻找极大项空间不可扩展的极大项为目标, 利用贪心策略限定极大项空间, 以变量的邻居变量设定格局信息, 从而减少了冗余搜索步骤, 牺牲了算法完备性, 从而达到了高效求解的效果.
ERACC算法的精髓在于对极大项中反转变量的选择, 通过最大左度和最小右度的概念, 限定两集合中的变量.如果集合为空, 则退一步选择得分高的变量取反.精确了变量的选择直接控制了极大项的变换, 使得推理过程更加精确(算法的具体流程见文献[
传统的基于扩展规则的并行推理方法将子句集的极大项空间分解为若干个子空间, 并对其进行逐一求解.这种并行方式并未加入启发式信息, 使得分割空间无层次.即使分割的子空间彼此毫无关联, 但整体推理的空间复杂度并无降低.
本文提出的并行处理是一种结合了对解空间化简的预处理方法.在选择特定的变量之后, 对原子句集进行化简, 化简后的子句集与原子句集是逻辑等价的, 这也极大地降低了对整个子句集求解的空间需求; 并在ERACC算法中加入了对初始值的赋值限制, 改变了ERACC对初始值赋为1的单调做法, 使求解器整体求解能力得到了较大地提升.
我们通过选取变量的启发式算法, 对出现在每个子句中的文字赋予权值.从文字出现在各个子句中的累计次数计算出得分最高的变量.首先, 遍历原始子句集获得所有文字的数组, 从数组中选取最大数对应的变量.如果同等数量的变量有若干个, 那么从中随机选取需求个数作为初始变量, 变量个数由所划分的解空间参数决定.变量选取算法如下, 其中,
输入: CNF公式
输出: CNF公式
1
2 {
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
算法1采取一种遍历求和排序的方式来计算各个变量的得分集合, 从而选取权重最高的变量作为化简子句集的初始变量.算法第2行表示程序遍历了整个子句集
变量得分的计算, 令
在以上公式中,
以上公式给出了变量得分的计算方式, 基本思想为: 根据文字出现在子句中的形式取相应的值.正文字取1(变量所对应文字为
例1:令CNF公式
●
●
●
●
●
●
●
由例1可以看出: 给定CNF公式
我们的目的在于对原解空间进行最大程度化简, 因此选择了得分最高的变量作为初始变量.最理想的情况是存在某个变量出现在每个子句中, 这样可以最大程度地降低子句集规模, 得到的问题规模最小.即: 在预处理阶段约简了原子句集, 其约简后的结果与原子句集是逻辑等价的.
证明: 固定了极大项中的文字之后, 原子句集中带有互补文字的子句可直接忽略, 因为这样的子句是无法扩展出当前极大项的; 而带有相同的文字可以忽略不计, 只看除了该文字剩余部分的子句.这样, 剩余变量的模型组成了新的极大项, 与化简后的子句集相对应, 即, 同原极大项和原子句集是逻辑等价的.
例2:令CNF公式
由例2可以看出: 在保证了逻辑等价的前提下, 化简后的子句集规模已经远远地小于原子句集的规模.实验证明: 不论在时间还是空间上, 都有了很大的提高.
选择变量的目的在于化简解空间, 而并行的目的是基于化简基础上能够全面地对子句集求解.由于选择的变量组合的不同, 对子句集化简的程度也不同.基于该问题, 我们会选择几种化简后, 求解效率最高的那个子空间作为判断的标准.我们提出了PERM算法来解决这一问题.
PERM算法过程如下:
输入: CNF公式
输出: 不可扩展的极大项
1
2
3
4
5
6
7
算法2给出在极大项子空间中分割原始极大项解空间的并行算法PERM.首先输入原CNF公式和已选取的变量, 预处理程序通过二进制方法将变量的2
由第1节我们可知, NER和ERACC两种算法都是以寻找子句集扩展不出的极大项为目标来进行推理的, 所以我们采取的途径是变换和调整极大项的模型.在ERACC中已详细地说明了如何去变换调整极大项, 忽略了对初始极大项的重视, 采用了单纯的对初始极大项中没个变量赋值为1.初始的极大项中, 变量的赋值在整个推理过程中占据重要的位置.如果没有针对性地给初始极大项赋值, 则会在求解过程中走很大的弯路, 间接地增加了冗余的推理过程.
为了使推理过程更直接、高效, 我们提出了SIMT算法, 有针对性地解决对初始极大项中变量赋初始值的选择.由于极大项中的每个变量可以赋值为正和负两种文字形式, 而每种文字形式的赋值概率为50%, 我们提出的算法是每个变量根据原子句集中文字出现的比率来确定初始极大项中变量的取值概率.实验结果表明, 我们的策略是有效的.
SIMT算法过程如下.
输入: CNF公式
输出: 初始极大项
1
2
3
4
5
6
7
8
9
10
11
算法3中,
结合了以上算法, 基于ERACC算法, 我们提出了基于精确格局检测的并行扩展规则算法, 算法过程如下.
输入: CNF公式
输出: 不可扩展极大项
1
2
3
4
5
6
7
8 Compute the Candidate
9
10
11
12
13
14
15
16
17
18
19
20
21
22
算法PERACC的执行过程大致如下: 第1行~第4行通过调用CPVI算法选择初始变量, 通过变量选择的数量, 得到分解解空间的数量, 并对各个解空间进行化简, 然后对各个解空间进行求解; 第5行调用算法SIMT来计算各个解空间的初始极大项; 第6行~第18行是调用ERACC算法对每个解空间的求解, 其详细过程可参考文献[
本节对算法PERACC算法进行实现, 并且将其与扩展规则领域主流的求解器SER, ERACC以及国际主流的SWCC求解器进行了对比.实验结果证明了PERACC算法不仅胜过了传统的扩展规则方法, 而且大大地缩短了与国际主流求解器的距离.
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求解器或者是随机的局部搜索算法都是很难的问题.在以往的扩展规则算法测试中, 由于受到求解规模的限制, 只能求解一些小规模的测试用例.而在文献[
随机3-SAT测试用例uf250实验结果(CPU time/s)
Experiment results on uniform random-3-SAT instances 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 |
在
带着以上两个问题, 我们做出了以下实验.
图着色测试用例flat200-479实验结果(CPU time/s)
Experiment results on graph Colouring instances 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 |
为了测试SIMT算法的有效性, 我们在
PERACC(
我们将继续延伸我们的思路, 加入了当前国际著名的局部搜索求解器SWCC进行对比.从数据上不难看出, PERACC比ERACC的效率提升了1.6倍~117倍不等.虽然PERACC的求解效率并没有超过SWCC求解器, 但是相对于当前扩展规则领域最高效的ERACC而言, PERACC已大大地缩短了与SWCC的距离.
我们将实验的证明继续扩大化, 选择了AIM类问题.该类问题结构性很强, 变量个数以及正负文字比例存在一定规律, 解的个数只有一个, 求解难度较高.1_6和2_0代表子句与变量的比率, 测试用例的变量为100个.所以, 我们将运行1 200s未结束的测试用例定为Time out.
从
AIM类问题测试实验结果(CPU time/s)
Experiment results on AIM instances (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算法相比于成熟的局部搜索求解器确有不足, 因此, 我们在原有基础上做出了一系列改进, 进一步研究扩展规则的适用性.我们相信, 虽然扩展规则推理方法还处于初级阶段, 但与不完备的局部搜索方法相结合, 必将发挥出它更大的潜力.
本文基于ERACC算法提出了并行框架, 提出了PERACC算法, 我们先后提出了预处理、化简解空间等技术, 并行处理各个子空间.通过实验显示: 该算法较原算法的求解效率有较大的提高, 并不断缩短了与国际著名算法SWCC的差距.
PERACC算法在原有算法的基础上进一步大胆地尝试了扩展规则方法领域中不完备推理的发展.下一步, 我们决定将DPLL算法中的单文子传播机制加入其中, 从而进一步完善预处理的效果.另一方面, 我们将知识约简方法应用于并行前和并行后, 通过对复杂问题约简手段的不断提高, 才能让我们去不断地求解复杂性更高、规模更大的测试用例.具体的方法还需要进一步进行理论分析和大量的实验来证明想法的可行性, 合理与PERACC结合, 使算法的求解能力得到最大化的提升.
Selman B, Levesque HJ, Mitchell DG. A new method for solving hard satisfiability problems. In: Proc. of the 10th National Conf. on Artificial Intelligence. 1992. 400-446.
Li CM, Huang WQ. Diversification and determinism in local search for satisfiability. In: Proc. of the 8th Int'l Conf. on Theory and Applications of Satisfiability Testing. 2005. 158-172.
Li CM, Li Y. Satisfying versus falsifying in local search for satisfiability. In: Proc. of the 15th Int'l Conf. on Theory and Applications of Satisfiability Testing. 2012. 477-478.
KhudaBukhsh AR, Xu L, Hoos HH, Leyton-Brown K. SATenstein: Automatically building local search SAT solvers from components. Artificial Intelligence, 2016, 232(4): 20-42.
Cai SW, Su KL. Local search with configuration checking for SAT. In: Proc. of the 23rd IEEE Int'l Conf. on Tools with Artificial Intelligence. 2011. 59-66.
Cai SW, Su KL. Local search for Boolean satisfiability with configuration checking and subscore. Artificial Intelligence, 2013, 204(9): 75-98.
Luo C, Cai SW, Su KL, Wu W. Clause states based configuration checking in local search for satisfiability. IEEE Trans. on Cybernetics, 2015, 45(5): 1014-1027.
Luo C, Cai SW, Wu W, Jie Z, Su KL. CCLS: An efficient local search algorithm for weighted maximum satisfiability. IEEE Trans. on Computers, 2015, 64(7): 1830-1843.
Cai SW, Jie Z, Su KL. An effective variable selection heuristic in SLS for weighted Max-2-SAT. Journal of Heuristics, 2015, 21(3): 433-456.
Cai SW, Zhang XD. ReasonLS. In: Proc. of the SAT COMPETITION 2018 Solver and Benchmark Descriptions. 2018. 52-53.
Lin H, Sun JG, Zhang YM. Theorem proving based on the extension rule. Journal of Automated Reasoning, 2003, 31(1): 11-21.
Wu X, Sun JG, Lü S, Li Y, Meng W, Yin MH. Improved propositional extension rule. In: Proc. of the 1st Int'l Conf. on Rough Sets and Knowledge Technology. 2006. 592-597.
Sun JG, Li Y, Zhu XJ, Lü S. A novel theorem proving algorithm based on extension rule. Journal of Computer Research and Development, 2009, 46(1): 9-14(in Chinese with English abstract).
孙吉贵, 李莹, 朱兴军, 吕帅. 一种新的基于扩展规则的定理证明算法. 计算机研究与发展, 2009, 46(1): 9-14.
Zhang LM, Ouyang DT, Bai HT. Theorem proving algorithm based on semi-extension rule. Journal of Computer Research and Development, 2010, 47(9): 1522-1529(in Chinese with English abstract).
张立明, 欧阳丹彤, 白洪涛. 基于半扩展规则的定理证明方法. 计算机研究与发展, 2010, 47(9): 1522-1529.
Yin MH, Sun JG, Lin H, Wu X. Possibilistic extension rules for reasoning and knowledge compilation. Ruan Jian Xue Bao/Journal of Software, 2010, 20(11): 2826-2837(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/3690.htm[doi:10.3724/SP.J.1001.2010.03690]
殷明浩, 孙吉贵, 林海, 吴瑕. 可能性扩展规则的推理和知识编译. 软件学报, 2010, 20(11): 2826-2837. http://www.jos.org.cn/1000-9825/3690.htm[doi:10.3724/SP.J.1001.2010.03690]
Liu L, Niu DD, Lü S. Knowledge compilation methods based on the hyper extension rule. Chinese Journal of Computers, 2016, 39(8): 1681-1696(in Chinese with English abstract).
刘磊, 牛当当, 吕帅. 基于超扩展规则的知识编译方法. 计算机学报, 2016, 39(8): 1681-1696.
Wang Q, Liu L, Lü S. #SAT solving algorithms based on extension rule using heuristic strategies. Ruan Jian Xue Bao/Journal of Software, 2018, 29(11): 3517-3527(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5298.htm[doi:10.13328/j.cnki.jos.005298]
王强, 刘磊, 吕帅. 基于扩展规则的启发式#SAT求解算法. 软件学报, 2018, 29(11): 3517-3527. http://www.jos.org.cn/1000-9825/5298.tm[doi:10.13328/j.cnki.jos.005298]
Yang Y, Liu L, Li GL, Zhang TB, Lü S. A novel local search-based extension rule reasoning method. Chinese Journal of Computers, 2018, 14(4): 825-839(in Chinese with English abstract).
杨洋, 刘磊, 李广力, 张桐搏, 吕帅. 一种新的基于局部搜索的扩展规则推理方法. 计算机学报, 2018, 14(4): 825-839.
Yang Y. Research on the reasoning methods using the extension rule[MS. Thesis]. Changchun: Jilin University, 2017(in Chinese with English abstract).
杨洋. 基于扩展规则的推理方法研究[硕士学位论文]. 长春: 吉林大学, 2017.
Li Y, Sun JG, Wu X, Zhu XJ. Extension rule algorithms based on IMOM and IBOHM heuristics strategies. Ruan Jian Xue Bao/Journal of Software, 2009, 20(6): 1521-1527(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/3420.htm[doi:10.3724/SP.J.1001.2009.03420]
李莹, 孙吉贵, 吴瑕, 朱兴军. 基于IMOM和IBOHM启发式策略的扩展规则算法. 软件学报, 2009, 20(6): 1521-1527. http://www.jos.org.cn/1000-9825/3420.htm[doi:10.3724/SP.J.1001.2009.03420]
Zhang LM, Ouyang DT, Zhao J, Bai HT. The parallel theorem proving algorithm based on semi-extension rule. Applied Mathematics & Information Sciences, 2012, 6(1): 119-122.
Li Z. Studies on some issues of satisfiability problems[Ph. D. Thesis]. Changchun: Jilin University, 2020(in Chinese with English abstract).
李壮. 可满足性问题的相关问题研究[博士学位论文]. 长春: 吉林大学, 2020.