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