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. Currently, extensive research has been conducted on their solving techniques. In practical application scenarios, SAT/SMT solvers often need to solve a series of closely related formulas. Compared to invoking an independent solver to solve each problem from scratch, incremental solving technology can reuse previously obtained search information, including previous solutions and learned clauses, thereby 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 paper provides a detailed review and organization of incremental SAT/SMT solving techniques, covering both complete and incomplete algorithms. Additionally, we comprehensively summarize the applications of incremental SAT/SMT solving techniques in practical scenarios. Finally, we summarize and outlook the development directions in this field.