提升SAT求解效率：基于演绎长度的学习子句删除策略

"本文主要探讨了基于演绎长度的学习子句删除策略在CDCL-SAT求解器中的应用，以及如何通过结合现有策略来提高求解效率。作者提出了一个新的学习子句评估方法，该方法基于演绎长度，并与基于文字块距离的评估方法相结合，形成两种不同的结合算法。实验结果显示，这种结合策略能更有效地评估学习子句的有用性，从而提升求解性能。" 在计算机科学领域，布尔可满足性问题（SAT问题）是一个基础且关键的难题，属于NP完全问题。解决SAT问题的方法之一是使用冲突驱动合取范式求解器（Conflict-Driven Clause Learning, CDCL），其中，学习子句的管理与删除策略是关键优化环节。学习子句是在解决过程中产生的辅助信息，用于避免重复探索，但过多的子句可能导致内存消耗过大，影响求解速度。 传统的学习子句删除策略基于各种标准，如文字块距离，它衡量子句中相邻变量的差异。然而，这篇论文指出，这些标准可能不充分，因为它们未能全面反映学习子句在推理过程中的作用。作者引入了基于演绎长度的新评估方法，演绎长度反映了学习子句在归结过程中的贡献。通过这种方式，可以更准确地判断哪些学习子句在后续推理中可能不再重要，从而进行有效删除。 为了进一步增强策略的效能，作者将演绎长度的评估与基于文字块距离的方法融合，形成了两种结合算法。这两种算法根据不同的子句排序基准运作，以适应不同的问题特性。通过在国际SAT竞赛的标准实例上进行实验，他们对比了新策略与当前主流求解器的性能。实验结果表明，提出的结合算法在评估学习子句的有用性上表现更优，解决了更多问题，比单纯基于文字块距离的策略提高了4.1%的求解成功率。 这一研究成果对于提升CDCL-SAT求解器的性能具有重要意义，尤其是在处理大规模、复杂问题时。通过改进学习子句的管理，不仅可以节省计算资源，还可以加速问题求解，对实际应用，如软件验证、电路设计和优化问题等领域有显著的促进作用。