基于演绎长度的学习子句删除策略

来源：计算机工程与应用杂志2018年第16期北京时间：

作者：常文静1，3，徐 扬2，3，吴贯锋1，3

单位：1.西南交通大学 信息科学与技术学院，成都 610036；2.西南交通大学 数学学院，成都 610036；3.系统可信性自动验证国家地方联合工程实验室，成都 610036

摘要：学习子句删除策略是CDCL-SAT求解器中的一个重要内容，可以避免内存爆炸和加速单元传播。评估学习子句有用性的标准不同导致所删除的学习子句是不同的，极大地影响求解效率。基于CDCL算法的求解过程可被形式化为增加管理学习子句策略的归结演绎过程，基于此，提出一种基于演绎长度的学习子句评估方法，并与现有的基于文字块距离的评估方法结合，根据排序子句的基准不同，形成两种不同的结合算法。采用国际SAT竞赛的基准实例，与目前主流的求解器进行了实验对比分析。结果表明，所提的结合算法能更好地评估学习子句的有用性，较基于文字块距离策略的求解个数提高了4.1%，说明所提策略具有一定的优势。

关键词：可满足性问题,冲突驱动子句学习,学习子句删除,演绎长度