增量SAT/SMT问题的求解与应用综述
CSTR:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

TP301

基金项目:

国家重点研发计划(2023YFA1009500)


Review on Solving Techniques and Applications for Incremental SAT/SMT Problems
Author:
Affiliation:

Fund Project:

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

    命题可满足性问题(SAT)和可满足性模理论问题(SMT)是重要的计算机科学基础问题, 其在电路设计, 软件分析验证等领域都有着重要应用, 并且目前已有大量工作对其求解技术进行研究. 在实际应用场景中, SAT/SMT求解器通常需要求解一系列互相紧密联系的公式. 相比于每次都调用独立的求解器重新求解, 增量求解技术可以复用之前搜索得到的信息, 包括之前的求解结果以及学习子句等, 从而有效提高了求解效率. 目前, 增量SAT/SMT求解已经受到广泛重视与研究, 并成功应用于有界模型检测, 符号执行, 最大可满足性问题等领域中. 对增量SAT/SMT的求解技术进行详细综述与梳理, 涵盖了完备与非完备算法. 此外, 详细总结增量SAT/SMT求解技术在实际场景中的主要应用. 最后, 对该领域的发展方向进行总结和展望.

    Abstract:

    The propositional satisfiability problem (SAT) and the satisfiability modulo theories problem (SMT) are fundamental problems in computer science, with significant applications in circuit design, software analysis and verification, and other fields. At present, extensive research has been conducted on their solving techniques. In practical applications, SAT/SMT solvers often need to solve a series of closely related formulas. Compared to solving each problem from scratch using an independent solver, incremental solving techniques can reuse previously obtained search information, including previous solutions and learned clauses, thus effectively improving solving efficiency. Currently, incremental SAT/SMT solving has received extensive attention and research, and has been successfully applied in fields such as bounded model checking, symbolic execution, and the maximum satisfiability problem (MaxSAT). This study provides a detailed review and categorization of incremental SAT/SMT solving techniques, covering both complete and incomplete algorithms. In addition, the applications of incremental SAT/SMT solving techniques in practical scenarios are comprehensively summarized. Finally, the development directions in this field are summarized and discussed.

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

李博涵,蔡少伟.增量SAT/SMT问题的求解与应用综述.软件学报,,():1-28

复制
相关视频

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

京公网安备 11040202500063号