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

Clc Number:

TP301

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:January 09,2025
  • Revised:April 21,2025
  • Adopted:
  • Online: November 05,2025
  • Published: August 06,2026
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063