重访 CDCL 的重启: 是否应保留搜索信息?
计算机科学中的逻辑
2024-05-29 v2
摘要
SAT 汇解器是形式化硬件和软件验证中不可或缺的工具,并拥有众多重要应用。CDCL 是现代 SAT 汇解器最广泛使用的框架,重启是 CDCL 的 essential 技术。 在重启时,CDCL 汇解器会取消当前的变量分配,但保持分支顺序、变量相位和已学习子句。这种类型的重启被本文称为温重启。尽管已研究了不同的重启策略,但尚无人探讨在重启后是否应保留此类信息。本工作 addresses 此问题并发现了一些有趣的观察。本文指出,在这种流行的温重启方案下,由于随机化的初始顺序和相位的不同,运行时存在显著变动。这激励我们定期忘记一些已学习信息以防止陷入不利的搜索空间.我们提出一种新的重启类型称为冷重启,其与以前的重启不同之处在于忘记一些已学习信息。实验表明,现代 CDCL 汇解器可从定期进行冷重启中获益。基于对冷重启策略的分析,我们开发了一个并行 SAT 汇解器。序列和并行版本的冷重启都更适合满足可满足实例,这表明如果希望构建满足可满足性的求解器,则应修订现有的 CDCL 启发式方法以进行信息管理。
引用
@article{arxiv.2404.16387,
title = {Revisiting Restarts of CDCL: Should the Search Information be Preserved?},
author = {Xindi Zhang and Zhihan Chen and Shaowei Cai},
journal= {arXiv preprint arXiv:2404.16387},
year = {2024}
}