《表2 不同求解器求解Ehlers测试例的运行时间和学习子句集删除次数》
表1给出了在相同实验环境下,五个含参求解器与原版求解器G+lbd的结果对比。表中分别记录了各求解器求解各类问题的个数及求解时间,黑体数字突出表示求解效果相对原版更好的求解器及对应求解问题类。实验发现对于Heule类的测试例(均为可满足测试例),不同参数的动态学习子句评估策略均比原版LBD策略求解出的问题个数多,所需求解时间更少;对于Ehlers类的测试例,在所求解问题个数变化不大的情况下,新策略在不同程度上减少了求解时间,如表2所示。Reduce DB表示求解器对学习子句集删除管理的次数,如果学习子句评估策略能有效评估学习子句的使用程度,则可以通过减少Reduce DB的次数提高求解效率。在不同参数下求解器的求解性能有所不同,针对不同问题求解器的求解性能也有差别,对于一些问题可能参数越大(在动态评估策略中保留更多参与冲突次数多的学习子句)求解性能越好,而对于一些问题则参数越小(在动态评估策略中保留较少参与冲突次数多的学习子句)越好。综合考虑上述情况,本文希望尽可能寻找到满足大部分问题求解最优情况下的参数,使得求解器在求解的总个数上能较原版求解器好。G+lbd+keep0.3求解器保留30%参与冲突分析次数最多的学习子句,在上述问题中求解出的问题个数比原版多5个,且求解时间与原版相差不大。因而,当threshold1取值为0.3时为最适合Glucose求解器的对应动态学习子句评估策略参数。
图表编号 | XD00222764500 严禁用于非法目的 |
---|---|
绘制时间 | 2020.10.05 |
作者 | 孙菁、钟小梅、徐扬 |
绘制单位 | 西南交通大学数学学院、系统可信性自动验证国家地方联合工程实验室、西南交通大学数学学院、系统可信性自动验证国家地方联合工程实验室、西南交通大学数学学院、系统可信性自动验证国家地方联合工程实验室 |
更多格式 | 高清、无水印(增值服务) |