可满足性问题(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)

在子句学习库中, 学习子句的多少严重影响了BCP速率.因此, SAT求解过程对应了博弈模型, 其中:参与者对应平均BCP速率和阶段BCP速率; 策略对应学习库的调整参数±0.01;利益对应求解效率提高和BCP速率提高; 信息对应平均BCP速率和阶段BCP速率.

综上, 博弈模型的支付矩阵如表 1所示.

2.2 博弈模型的分析

本文令重启总数为N, 每重启S次记为一个阶段, 第i阶段的BCP数量为s_i, 相应的第i阶段的执行时间为t_i, 则阶段BCP速率v_i=s_i/t_i.

截至第n阶段, BCP总量，BCP总传播时间, 则平均BCP速率为.

记p_i∈[-0.1, 0, 0.1]为每个阶段的增减参数.当时, p_i+1=-0.1;当时, p_i+1=0.1;当时, p_i+1=0.学习库增减参数P_n= .

以上分析不难看出:当v_i和都减小时, 可能出现等值, 这时达到了Pareto最优, 即两者的效用同时得到最大化; 当时, 说明学习库中的学习子句相对较少.在不影响BCP速率的情况下, 可以适量增加学习子句的数量, 这里采用增减参数设置为0.1来实现; 同理, 当时, 相应设置为-0.1来控制学习库的增长速率, 从而在不影响求解效率的同时增大阶段BCP的增长速率; 而两者皆增大的情况是不可能出现的.实际的支付矩阵见表 2.

这一过程是一个连续的博弈过程, 其根本目的是在不断地追求无限接近纳什均衡点, 实现已学习子句库的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求解器.

为了更准确地决定重启的次数对GTMiniSAT求解器的影响, 在上述200个算例中, 多次尝试了重启1次, 5次…直到重启65次, 增减参数默认为0.1, CPU在求解器运行时间至5 000 s时停止.实验结果如表 3所示.

由表 3可知, 重启次数固定在55次, 平均求解时间最短, 而且优于MiniSAT求解器.而其他参数的数据表明求解的平均效率较低, 且重启55次时求解个数也是最多的.因此, 在重启55次后调整增减参数是最合理的.

在固定了重启参数为55次之后, 接下来需要对增减参数进行测试.在上述算例中, 尝试增减0.01, 0.02…直至0.1.CPU在求解器运行时间至5 000 s时停止.实验结果如表 4所示.

由表 4可知, 增减参数为0.05和0.1的两组求解效率比较高, 而且优于MiniSAT求解器.但两者所处的距离较远, 中间出现了一系列的波动.出现的原因是否会受到重启参数的影响, 即重启参数越大, 所对应的增减参数则越大, 两者是否成正比关系呢?为了证明这个想法, 在以下实验中给出了更具体的证明, 并且验证本文的GTMiniSAT求解器对于一般的工业问题, 也是优于MiniSAT求解器的.

GTMiniSAT求解器主要针对规模较大的工业问题有效, 简单问题的优化效果并不明显.所以, 选择了2017年SAT竞赛中Random组的300个算例, CPU在求解器运行时间至5 000 s时停止.实验结果见表 5.

由表 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%.

为了验证GTMiniSAT求解器的有效性, 再次对GTMiniSAT求解器和MiniSAT求解器在共同求解出的114个算例中做出数据统计，如表 7所示.从表 7可知, GTMiniSAT求解器的求解效率也远超过MiniSAT求解器, 其求解效率提高了35.76%.

4 结语

本文首次将博弈论的思想应用于经典SAT求解中, 通过重启次数来调整学习库的增长参数, 将原有学习数据库的静态等比级数增长改进为动态的变化, 尽可能靠近学习数据库中子句存储量的均衡点, 从而使学习库的存储量尽可能达到Pareto最优.

GTMiniSAT还存在如下问题有待解决:1)之所以改进MiniSAT求解器, 因为MiniSAT是一款经典的求解器, 对于新方法的融入有更大的接受空间, 下一步工作将考虑改进Maple_CM等当前最先进的求解器.2)由于分析的角度不同, 选择的博弈模型也不同, 本文中求解效率和BCP速率具有竞争关系, 而同时又拥有共同目标——求解SAT问题, 即它们相互合作却又彼此竞争.下一步工作将站在两者共同的立场(即合作博弈), 对它们的合作做出进一步的博弈分析.