回跳层数评估的SAT求解器学习子句优化策略

"基于回跳层数的SAT求解器学习子句删除策略" 本文主要探讨了在可满足性问题（SAT）求解器中的学习子句删除策略优化。当前广泛使用的策略是基于最小割（LBD，Minimun Bounded Depth）的评估方式，它在每次删除操作中会去除LBD值较高的学习子句的一半。然而，这种策略可能过于激进地删除了某些有价值的高LBD子句。 针对这一问题，作者提出了一个新颖的策略，即利用冲突回跳层数（back-jump levels）作为评估标准来保留那些虽然LBD值大但依然重要的学习子句。这个策略是基于冲突驱动子句学习（CDCL）算法的框架，通过引入BJL（Back-Jump Levels）删除算法，可以在删除子句的过程中更加精细地判断哪些子句应当保留。 CDCL算法是一种核心的SAT求解方法，它通过不断解决冲突并学习新的子句来逐步缩小搜索空间。LBD是衡量子句复杂度的一个指标，它考虑了子句在解决过程中导致回溯的深度。而回跳层数则反映了在解决过程中遇到冲突后需要回退的深度，这可以反映出子句在解决过程中的作用。 实验部分，作者们使用了2017年SAT国际竞赛的数据集，将新提出的BJL策略与原版的求解器进行了对比。结果显示，BJL策略能够显著提升求解器的性能和求解效率，这意味着在解决复杂的SAT问题时，新策略可以更有效地找到解决方案，减少计算时间和资源消耗。 论文的作者包括沈雪、陈树伟、徐扬和吴贯锋，他们分别在西南交通大学的数学学院和信息科学与技术学院工作，并隶属于系统可信性自动验证国家地方联合工程实验室。他们的研究领域涵盖了智能信息处理、自动推理以及控制与决策。 总结来说，这篇研究为SAT求解器的优化提供了新的思路，通过利用回跳层数来指导学习子句的删除，能够在保持求解效率的同时，更好地保存了对解决问题有帮助的信息，从而提高了整体的求解性能。这项工作对于理解如何改善现代SAT求解器的性能以及在实际应用中解决复杂问题具有重要意义。