《表1 基于Glucose求解器的改进策略结果对比》

  提示：宽带有限、当前游客访问压缩模式

本系列图表出处文件名：随高清版一同展现

《基于参与冲突分析次数的动态学习子句评估策略》

1. 获取 高清版本忘记账户？点击这里登录

1. 下载图表忘记账户？点击这里登录

表1给出了在相同实验环境下，五个含参求解器与原版求解器G+lbd的结果对比。表中分别记录了各求解器求解各类问题的个数及求解时间，黑体数字突出表示求解效果相对原版更好的求解器及对应求解问题类。实验发现对于Heule类的测试例（均为可满足测试例），不同参数的动态学习子句评估策略均比原版LBD策略求解出的问题个数多，所需求解时间更少；对于Ehlers类的测试例，在所求解问题个数变化不大的情况下，新策略在不同程度上减少了求解时间，如表2所示。Reduce DB表示求解器对学习子句集删除管理的次数，如果学习子句评估策略能有效评估学习子句的使用程度，则可以通过减少Reduce DB的次数提高求解效率。在不同参数下求解器的求解性能有所不同，针对不同问题求解器的求解性能也有差别，对于一些问题可能参数越大（在动态评估策略中保留更多参与冲突次数多的学习子句）求解性能越好，而对于一些问题则参数越小（在动态评估策略中保留较少参与冲突次数多的学习子句）越好。综合考虑上述情况，本文希望尽可能寻找到满足大部分问题求解最优情况下的参数，使得求解器在求解的总个数上能较原版求解器好。G+lbd+keep0.3求解器保留30%参与冲突分析次数最多的学习子句，在上述问题中求解出的问题个数比原版多5个，且求解时间与原版相差不大。因而，当threshold1取值为0.3时为最适合Glucose求解器的对应动态学习子句评估策略参数。