自动推理可用于数学证明软件或硬件是否按预期工作。实践中，自动推理常依赖称为SAT求解器的程序，其判定描述系统约束的形式表达式是否可满足。SAT问题具有极高的计算复杂度（原始NP完全问题），现代SAT求解器通过数万行代码的复杂算法实现高效求解。但如何确保求解器判定结果的可靠性？传统形式化验证方法因代码规模过大而难以实施。
解决方案是让SAT求解器生成推理过程记录（追踪），由自动化证明检查器验证。对于约束可一次性指定的SAT问题，已有成熟的机器可验证证明生成方法。但在实际场景中，约束往往需要逐步添加形成增量SAT问题，现有证明方法对此失效。
在某机构举办的计算机辅助设计形式化方法会议（FMCAD 2023）上，我们提出了增量SAT问题的可验证证明生成方法。关键技术在于：当求解器因新约束添加而需要恢复已删除子句时，证明生成过程将该子句视为从未被删除。这种处理使得现有证明框架可扩展到增量SAT场景。具体而言：
-
增量SAT特性
SAT求解器会删除与保留子句等可满足性的冗余子句。对于增量问题，删除的子句被存入重构栈并关联真值指派。当新增约束与栈内真值冲突时，相关子句将被恢复并重新评估。 -
证明生成算法
与传统正向追踪不同，本方法逆向处理追踪记录：遇到子句恢复操作时缓存该子句，若后续发现对应删除操作则同时消除这两个记录。清理后的追踪记录可按常规方法构建证明。
实验验证方面，我们在主流SAT求解器上实现该方法，测试包含294个不可满足问题和6个可满足问题的数据集。改进后的求解器对所有不可满足案例均生成有效证明，平均每GB证明生成时间约1分钟，相对求解时间仅增加5%开销。
该方法解决了增量SAT问题缺乏可验证证明的难题，为形式化验证领域提供了新的技术路径。相关论文《Proofs for incremental SAT with inprocessing》已在FMCAD 2023会议发表。