吉林大学 计算机科学与技术学院, 吉林 长春 130012
收稿日期：2019-03-19
基金项目：国家重点研发计划项目(2017YFB1003103);国家自然科学基金资助项目(61300049, 61763003);吉林省科技发展计划项目(20180101053JC, 20190201193JC)。
作者简介：李壮(1988-), 男, 吉林白城人, 吉林大学博士研究生;
刘磊(1960-), 男, 吉林长春人, 吉林大学教授, 博士生导师。
摘要：以学习子句数据库优化为背景, 在原MiniSAT求解器的基础上提出了一种新的学习子句的优化方法.该方法基于博弈论的思想, 在若干次重启后, 根据当前求解器的实时反馈信息改进MiniSAT原有的增长参数, 尽可能靠近学习数据库中子句存储量的均衡点, 从而使学习库的存储量尽可能达到Pareto最优.实验表明:所提的优化方法是有效的, 并在随机SAT问题上胜过现有优化方法.该方法既不会因为学习数据库的子句过多而影响单元传播速度, 也不会因为学习数据库中的子句过少而破坏学习的整体性.
关键词：DPLL子句学习学习子句数据库MiniSAT求解器Pareto最优
Learnt Clauses Optimize Method Based on Restart Strategy
LI Zhuang, LIU Lei, ZHANG Tong-bo, LYU Shuai
College of Computer Science and Technology, Jilin University, Changchun 130012, China
Corresponding author: LYU Shuai, E-mail: lus@jlu.edu.cn.
Abstract: With the background of optimization of the learnt clauses database, a new optimization method for learnt clauses based on the original MiniSAT solver was proposed. Based on game theory, this method adjusts the growth parameters after several restarts on the basis of the real-time feedback of the current solver, in order to be as close as possible to the balance point of clauses in the learnt clauses database. This makes the storage capacity of the learnt clause database reach the Pareto optimality as much as possible. Experiments showed that the proposed method is effective and outperforms existing optimization methods in random SAT problems. This method neither affects the speed of unit propagation because of too many clauses in the learnt clause database, nor destroys the integrity of learning because of too few clauses in the learnt clause database.
Key words: DPLL(Davis-Putnam-Logemann-Loveland)clause learninglearnt clauses databaseMiniSAT solverPareto optimality
可满足性问题(SAT)是计算机领域的热点问题, 许多学者在该问题上作了大量研究, 并在问题求解效率方面取得了较大的突破, 当今SAT求解器已能够解决很多现实问题.随着SAT求解技术的发展, 子句学习技术进入了蓬勃发展的阶段[1].对于现实问题, 子句学习(clause learning)是DPLL求解中最重要的部分[2].
在实践中, SAT的求解效率很大程度上取决于对已学习子句数据库的管理策略.即发生冲突后, 新子句添加到已学习的子句数据库中, 其增长规模是呈指数增长的.保留太多的学习子句会减缓单元传播的速率, 而删除太多将会破坏学习的整体性[3].所以, 优化目标在于清除掉已学习子句数据库中被判定为在以后的搜索中无关的已学习子句.学习子句管理策略的效率, 很大程度上取决于消除频率和每次删除的子句数量[4].
为了优化已学习子句数据库, 近几年一些先进的管理策略已被提出.首次提出质量测量的是VSIDS启发式, 该优化策略假设一个过去学习的子句在未来的求解过程中可能是有用的[5]; Audemard等介绍了一个新的静态措施, 加入LBD子句这一概念, 更加完善了对学习子句的预处理技术[3]; Audemard等提出了一个基于动态的冻结与激活学习子句的原则, 即激活最相关的学习子句而冻结不相关的学习子句[6]; Hamadi等提出规约策略SBR, 保留文字数小于等于k的子句, 同时随机删除大于k的子句[7]; Luo等提出了学习子句最小化的方法, 该方法通过BCP删除学习子句中的冗余文字, 从而达到对学习子句质量的优化[4]; Luo等基于Maple_LCM求解器的子句最小化方法, 在Maple_CM求解器上扩展到原始子句的预处理[8].对学习库的优化主要包括:优化学习库的时机、应删除哪些子句以及每次优化应保留多少子句.经分析, 优化学习库的时机对求解效率的影响并不大, 多数研究人员将注意力集中在应删除哪些冗余子句, 即注重了学习子句的质量, 保留更多有用的学习子句, 而对应保留学习库中子句数量的工作甚少.
本文基于经典的SAT求解器, 提出了新的动态管理学习子句数据库的算法.在优化的过程中, 通过博弈论的思想, 在阶段重启的过程中, 通过程序中输出的阶段布尔约束传播(Boolean constraint propagation，BCP)速率和平均BCP速率的对比, 调整学习数据库的增长参数, 更大可能地靠近学习数据库中子句存储量的均衡点, 从而使学习库的存储量尽可能地达到Pareto最优.实验结果表明:新的优化方法在随机问题上胜过传统的优化方法, 在求解出相同的算例中, GTMiniSAT求解器的求解效率也远超过MiniSAT求解器.
1 CDCL和重启策略子句学习采用了强大的冲突分析技术, 其主要思想是在求解过程中发生冲突时, 分析冲突原因并推理出一些简洁地表达冲突原因的子句, 这种已学习的子句用于在后面的搜索过程中避免发生同样的冲突且减少搜索空间, 更加快了求解的效率.
当单元传播过程中出现了一对互补文字时, 求解器判定子句集F中出现了一个冲突, 这个冲突将驱动子句学习机制, 将冲突原因保存为一个新的子句C, 并将它添加到原子句集中, 以防止在接下来的搜索过程发生相同的冲突, 这便是冲突驱动子句学习(conflict-driven clause learning, CDCL)[2].
重启发生在子句被学习之后, 当指派过程中发生了ε(ε＞1)次冲突后, 重启策略被触发, 求解器终止当前搜索并返回到第0层, 即重新求解该子句集[9].冲突上界会通过参数ε来决定.
2 基于博弈论的学习子句优化方法学习库空间的占有主要体现在对学习库增长参数的控制.如何调整学习库空间的分配, 使之在优化过程中无限接近学习库的纳什均衡点, 达到Pareto最优状态, 将是子句学习的关键.
2.1 博弈模型求解效率是求解算法好坏的关键衡量指标.由于BCP时间占了总求解时间约90%以上[10], 所以本文将求解时间等同于BCP时间.
求解效率是无法量化而又客观存在的, 但满足:平均求解效率越高, 平均BCP速率也越高.所以在本文中用平均BCP速率代替求解效率.
在一个SAT问题求解过程中, 存在着最基本的数学公式:
 | (1) |
综上, 博弈模型的支付矩阵如表 1所示.
表 1(Table 1)
 表 1 学习子句数据库的支付矩阵Table 1 Payment matrix of learnt clause database
| 表 1 学习子句数据库的支付矩阵 Table 1 Payment matrix of learnt clause database | |||||||||||
2.2 博弈模型的分析本文令重启总数为N, 每重启S次记为一个阶段, 第i阶段的BCP数量为si, 相应的第i阶段的执行时间为ti, 则阶段BCP速率vi=si/ti.
截至第n阶段, BCP总量
记pi∈[-0.1, 0, 0.1]为每个阶段的增减参数.当
以上分析不难看出:当vi和
表 2(Table 2)
表 2 学习子句数据库的实际支付矩阵Table 2 Real payment matrix of learnt clause database
| 表 2 学习子句数据库的实际支付矩阵 Table 2 Real payment matrix of learnt clause database | |||||||||||
这一过程是一个连续的博弈过程, 其根本目的是在不断地追求无限接近纳什均衡点, 实现已学习子句库的Pareto最优分配.
2.3 基于博弈论的学习子句优化算法算法1是GTMiniSAT求解器的简要求解过程, 其中包括了学习子句优化的函数.
算法1 ?DPLL with clause learning
输入:CNF formula F
输出:A solution P of F or UNSAT if F is not satisfiable
1.BCP_num++
2.if P assigns a value to every variable
3. return success
4.else
5. P contains a conflict
6. choose a conflict graph G to find clause C under P and add it to F
7. rollback variable or backjump
8. conflict_num++
9. if conflict_num>ε
10.restart++
11.if restart%S==0
12. BCP_total+=BCP_num
13. speed_average=BCP_total/nowtime
14. speed_now=BCP_num/(nowtime-lasttime)
15. if speed_now>speed_average
16.learntsize_inc+=p
17. else if speed_now＜speed_average
18.if learntsize_inc-p≥0.5
19. learntsize_inc-=p
20.restarts
在算法1中, 第9行表明当冲突数量达到了临界值ε时重启, 第11行表明重启次数达到S(实验表明55为最优值)次时, 触发重启参数调整策略.第12~19行描述了控制增长参数的过程.当冲突数达到55次后, 第12行统计从开始求解截止到目前的BCP数量.第13~14行计算平均BCP速率和阶段BCP速率.第15~19行通过对速率的比较, 来调整增减参数.当阶段BCP速率大于平均BCP速率时, 增长参数提高; 当阶段BCP速率小于平均BCP速率时, 增长参数降低.第18行控制了下界, 当参数小于0.5时, 增减参数不变.
3 实验与结果本文从2017年SAT比赛Agile组中随机选取了200个测试用例, 其规模为几百个变量(1 000条子句)至180万变量(668万条子句)不等, CPU在求解器运行时间至5 000 s时停止.其重启参数默认为50, 增减参数默认为0.1.实验环境:Arch Linux 16.04操作系统, 12核CPU, 8GB RAM.
图 1横坐标代表MiniSAT求解器的运行时间, 纵坐标代表GTMiniSAT求解器的运行时间.所以, 分布在斜线以下的点说明这些算例在GTMiniSAT求解器上的求解效果较好; 在斜线以上的点说明这些算例在MiniSAT求解器上的求解效果较好.可以看出, GTMiniSAT求解器效率较明显地优于MiniSAT求解器.斜线以上的点多半离斜线较近, 说明这些算例在MiniSAT求解器的求解效果略优于GTMiniSAT求解器; 而斜线以下的点有很大一部分离斜线较远, 说明这一部分的算例在GTMiniSAT求解器的求解效果明显优于MiniSAT求解器.
图 1(Fig. 1)
 | 图 1 200个随机算例的对比图Fig.1 Comparison of 200 random benchmarks |
为了更准确地决定重启的次数对GTMiniSAT求解器的影响, 在上述200个算例中, 多次尝试了重启1次, 5次…直到重启65次, 增减参数默认为0.1, CPU在求解器运行时间至5 000 s时停止.实验结果如表 3所示.
表 3(Table 3)
表 3 GTMiniSAT求解器重启次数的测试Table 3 Test of restart times for GTMiniSAT solver
| 表 3 GTMiniSAT求解器重启次数的测试 Table 3 Test of restart times for GTMiniSAT solver | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
由表 3可知, 重启次数固定在55次, 平均求解时间最短, 而且优于MiniSAT求解器.而其他参数的数据表明求解的平均效率较低, 且重启55次时求解个数也是最多的.因此, 在重启55次后调整增减参数是最合理的.
在固定了重启参数为55次之后, 接下来需要对增减参数进行测试.在上述算例中, 尝试增减0.01, 0.02…直至0.1.CPU在求解器运行时间至5 000 s时停止.实验结果如表 4所示.
表 4(Table 4)
表 4 GTMiniSAT求解器增减参数的测试Table 4 Test of Increasing or decreasing the parameters for GTMiniSAT solver
| 表 4 GTMiniSAT求解器增减参数的测试 Table 4 Test of Increasing or decreasing the parameters for GTMiniSAT solver | ||||||||||||||||||||||||||||||||||||||||||||||
由表 4可知, 增减参数为0.05和0.1的两组求解效率比较高, 而且优于MiniSAT求解器.但两者所处的距离较远, 中间出现了一系列的波动.出现的原因是否会受到重启参数的影响, 即重启参数越大, 所对应的增减参数则越大, 两者是否成正比关系呢?为了证明这个想法, 在以下实验中给出了更具体的证明, 并且验证本文的GTMiniSAT求解器对于一般的工业问题, 也是优于MiniSAT求解器的.
GTMiniSAT求解器主要针对规模较大的工业问题有效, 简单问题的优化效果并不明显.所以, 选择了2017年SAT竞赛中Random组的300个算例, CPU在求解器运行时间至5 000 s时停止.实验结果见表 5.
表 5(Table 5)
表 5 2017年SAT竞赛随机组300算例Table 5 Test of 300 Benchmark in the random trackof the 2017 SAT competition
| 表 5 2017年SAT竞赛随机组300算例 Table 5 Test of 300 Benchmark in the random trackof the 2017 SAT competition |
由表 5可知, GTMiniSAT求解器所求出的两组算例是相同的114个, 且包含在MiniSAT求解器所求出的124个算例中, 平均求解时间也略高于MiniSAT求解器.(±0.1)-GTMiniSAT求解器所解出的114个算例中, 有72个算例比MiniSAT求解器快, 而(±0.05)-GTMiniSAT仅有50个算例优于MiniSAT求解器.因此, 选择增减参数为0.1是最合理的.
虽然GTMiniSAT求解器平均求解时间并没有胜过MiniSAT求解器, 但是通过统计实验结果, 在这72个算例中, MiniSAT求解器的平均求解时间为136.56 s, 而GTMiniSAT求解器的平均求解时间为44.44 s.表 6中统计了所有问题的求解个数和平均求解时间, 数据表明:GTMiniSAT求解器的效率远高于MiniSAT求解器, 其求解效率提高了67.45%.
表 6(Table 6)
表 6 GTMiniSAT和MiniSAT求解器的对比实验结果Table 6 Comparative evaluation between GTMiniSAT and MiniSAT solvers
| 表 6 GTMiniSAT和MiniSAT求解器的对比实验结果 Table 6 Comparative evaluation between GTMiniSAT and MiniSAT solvers |
为了验证GTMiniSAT求解器的有效性, 再次对GTMiniSAT求解器和MiniSAT求解器在共同求解出的114个算例中做出数据统计，如表 7所示.从表 7可知, GTMiniSAT求解器的求解效率也远超过MiniSAT求解器, 其求解效率提高了35.76%.
表 7(Table 7)
表 7 GTMiniSAT和MiniSAT求解器的对比实验(共同求解算例)Table 7 Comparative evaluation of between GTMiniSAT and MiniSAT solvers(common instances solved)
| 表 7 GTMiniSAT和MiniSAT求解器的对比实验(共同求解算例) Table 7 Comparative evaluation of between GTMiniSAT and MiniSAT solvers(common instances solved) |
4 结语本文首次将博弈论的思想应用于经典SAT求解中, 通过重启次数来调整学习库的增长参数, 将原有学习数据库的静态等比级数增长改进为动态的变化, 尽可能靠近学习数据库中子句存储量的均衡点, 从而使学习库的存储量尽可能达到Pareto最优.
GTMiniSAT还存在如下问题有待解决:1)之所以改进MiniSAT求解器, 因为MiniSAT是一款经典的求解器, 对于新方法的融入有更大的接受空间, 下一步工作将考虑改进Maple_CM等当前最先进的求解器.2)由于分析的角度不同, 选择的博弈模型也不同, 本文中求解效率和BCP速率具有竞争关系, 而同时又拥有共同目标——求解SAT问题, 即它们相互合作却又彼此竞争.下一步工作将站在两者共同的立场(即合作博弈), 对它们的合作做出进一步的博弈分析.
参考文献
| [1] | Beame P, Kautz H, Sabharwal A. Towards understanding and harnessing the potential of clause learning[J]. Journal of Artificial Intelligence Research, 2004, 22: 319-351. DOI:10.1613/jair.1410 |
| [2] | Silva J, Sakallah K.Grasp—a new search algorithm for satisfiability[C]//IEEE/ACM International Conference on Computer-aided Design(CAD 1996).Ann Arbor, 1996: 220-227. http://link.springer.com/10.1007/978-1-4615-0292-0_7 |
| [3] | Audemard G, Simon L.Predicting learnt clauses quality in modern SAT solvers[C]//International Joint Conference on Artificial Intelligence(IJCAI 2009).Pasadena, 2009: 399-404. http://www.researchgate.net/publication/220812877_Predicting_Learnt_Clauses_Quality_in_Modern_SAT_Solvers |
| [4] | Luo M, Li C, Xiao F, et al.An effective learnt clause minimization approach for CDCL SAT solvers[C]//Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence(IJCAI 2017).Melbourne, 2017: 703-711. |
| [5] | Moskewicz M, Madigan C, Zhao Y, et al.Chaff: engineering an efficient SAT solver[C]//Proceedings of Design Automation Conference(DAC 2001).Las Vegas, 2001: 530-535. http://www.researchgate.net/publication/2409503_Chaff_Engineering_an_Efficient_SAT_Solver |
| [6] | Audemard G, Lagniez J M, Mazure B, et al.On freezing and reactivating learnt clauses[C]//Proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing(SAT 2011).Ann Arbor, 2011: 188-200. http://www.springerlink.com/content/57802321lv535381 |
| [7] | Hamadi Y, Jabbour S, Sa?s L. What we can learn from conflicts in propositional satisfiability[J]. Annals of Operations Research, 2016, 240(1): 13-37. |
| [8] | Luo M, Xiao F, Li C, et al.Maple_CM, Maple_CM_Dist, Maple_CM_ordUIP and Maple_CM_ordUIP+ in the SAT competition 2018[C]//Proceedings of SAT Competition 2018—Solver and Benchmark Descriptions.Oxford, 2018: 44-46. |
| [9] | Atserias A, Fichte J K, Thurley M. Clause-learning algorithms with many restarts and bounded-width resolution[J]. Journal of Artificial Intelligence Research, 2011, 40: 353-373. DOI:10.1613/jair.3152 |
| [10] | Dixon H E, Ginsberg M L, Parkes A J. Generalizing boolean satisfiability Ⅰ:background and existing work[J]. Journal of Artificial Intelligence Research, 2004, 21: 193-243. DOI:10.1613/jair.1353 |
