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.