| 摘要: |
| 命题可满足性问题(propositional satisfiability problem, SAT)和可满足性模理论问题(satisfiability modulo theories problem, SMT)是重要的计算机科学基础问题, 其在电路设计, 软件分析验证等领域都有着重要应用, 并且目前已有大量工作对其求解技术进行研究. 在实际应用场景中, SAT/SMT求解器通常需要求解一系列互相紧密联系的公式. 相比于每次都调用独立的求解器重新求解, 增量求解技术可以复用之前搜索得到的信息, 包括之前的求解结果以及学习子句等, 从而有效提高了求解效率. 目前, 增量SAT/SMT求解已经受到广泛重视与研究, 并成功应用于有界模型检测, 符号执行, 最大可满足性问题等领域中. 对增量SAT/SMT的求解技术进行详细综述与梳理, 涵盖了完备与非完备算法. 此外, 详细总结增量SAT/SMT求解技术在实际场景中的主要应用. 最后, 对该领域的发展方向进行总结和展望. |
| 关键词: 命题可满足性问题 可满足性模理论问题 增量求解 |
| DOI：10.13328/j.cnki.jos.007489 |
| 分类号:TP301 |
| 基金项目:国家重点研发计划(2023YFA1009500) |
|
| Review on Solving Techniques and Applications for Incremental SAT/SMT Problems |
|
LI Bo-Han1,2, CAI Shao-Wei1,2
|
|
1.Key Laboratory of Systems Software (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China;2.School of Computer Science and Technology, University of Chinese Academy of Sciences, Beijing 100049, China
|
| 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. |
| Key words: propositional satisfiability problem (SAT) satisfiability modulo theories problem (SMT) incremental solving |
