CDCL SAT 求解器中基于单元传播的子句活化
人工智能
2018-07-31 v1 计算机科学中的逻辑
摘要
在冲突驱动子句学习（CDCL）SAT 求解器中，原始子句与学习子句常含有冗余文字。这可能对性能产生负面影响，因为冗余文字会削弱布尔约束传播的有效性以及后续学习子句的质量。为克服此缺陷，我们提出了一种通过应用单元传播来消除冗余文字的子句活化方法。所提出的子句活化在 SAT 求解器触发某些选定重启之前被激活，且仅影响原始与学习子句的一个子集，这些子句根据如文字块距离（LBD）等指标被认为更具相关性。此外，我们利用来自近期 SAT 竞赛中困难组合类与应用类实例进行了实证研究。结果表明，当所提方法被整合进五个表现最佳的 CDCL SAT 求解器（Glucose、TC_Glucose、COMiniSatPS、MapleCOMSPS 和 MapleCOMSPS_LRB）时，可解出数量可观的额外实例。更重要的是，该实证研究包含对子句活化有效性的深入分析。值得一提的是，本文所述 SAT 求解器之一因整合了所提子句活化而在 SAT 竞赛 2017 主赛道中排名第一。该求解器在本文中得到了进一步改进，并在 SAT 竞赛 2018 主赛道中获得铜牌。
引用
@article{arxiv.1807.11061,
title = {Clause Vivification by Unit Propagation in CDCL SAT Solvers},
author = {Chu-Min Li and Fan Xiao and Mao Luo and Felip Manyà and Zhipeng Lü and Yu Li},
journal= {arXiv preprint arXiv:1807.11061},
year = {2018}
}