CDCL算法的冷重启技术
CSTR:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

TP311

基金项目:

中科院战略先导科技专项A (XDA0320000,XDA0320300);


Cold Restart for CDCL Algorithms
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    SAT求解的CDCL算法被广泛应用于软硬件验证领域,重启策略是其中的核心的组件之一.目前,主流的CDCL求解器采用了“热重启”技术,保留了变元序、赋值倾向、学习子句等主要搜索信息,且重启频率极高.热重启技术会使CDCL重启之后更倾向于搜索重启前的搜索空间,有可能会长期陷于一个不利的局部区域,缺乏探索性.本文首先对现有的CDCL算法进行测试,证实了在不同的初始搜索设置下,主流CDCL求解器的求解时间有巨大的扰动.为了利用上述观察,本文提出了一种遗忘搜索信息的“冷重启”技术,即阶段性的遗忘变元序、赋值倾向、学习子句,实验证明了该技术可以有效的提高主流的CDCL算法.同时,本文也进一步拓展了其并行版本,每个线程探索不同的区域,提高了并行算法的性能.此外,冷重启技术主要改进了串并行求解器可满足实例的求解能力,为设计可满足导向的SAT求解器提供了新的改进思路.通过引入并行冷重启技术,PaKis求解器可满足性样例的PAR2打分平均提高41.81%.基于相关技术设计的并行SAT求解器ParKissat-RS以领先亚军24%的大幅领先优势取得国内首个国际SAT竞赛并行组冠军.

    Abstract:

    The CDCL algorithm for SAT solving is widely used in the field of hardware and software verification, with restart being one of its core components. Currently, mainstream CDCL solvers often employ the "warm restart" technique, which retains key search information such as variable order, assignment preferences, and learnt clauses, and has a very high restart frequency. The warm restart technique tends to make CDCL solvers more inclined to visit the search space that was explored before restarts, which may lead to being trapped in an unfavorable local search space for a long time, lacking exploration for another regions. This paper first tests the existing CDCL algorithms and confirms that under different initial search settings, the runtime for an instance of mainstream CDCL solvers exhibits significant fluctuations. To leverage this observation, the paper proposes the "cold restart" technique that forgets search information, specifically by periodically forgetting variable order, assignment preferences, and learned clauses. Experimental results demonstrate that this technique can effectively improve mainstream CDCL algorithms. Additionally, the paper further extends its parallel version, where each thread explores different search spaces, enhancing the performance of the parallel algorithm. Moreover, the cold restart technique primarily improves the performance of sequential and parallel solvers for the solving ability on satisfiable instances, providing new insights for designing satisfiable-oriented solvers. Specifically, our parallel cold restart techniques can improve 41.84% of the PAR2 score of Pakis on satisfiable instances. The parallel SAT solvers named ParKissat-RS including the ideas in this paper won the parallel track of SAT competitions with a significantly margin of 24% faster.

    参考文献
    相似文献
    引证文献
引用本文

张昕荻,陈志翰,蔡少伟. CDCL算法的冷重启技术.软件学报,,():0

复制
相关视频

分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2024-09-12
  • 最后修改日期:2025-05-28
  • 录用日期:
  • 在线发布日期: 2025-09-02
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号