自动推理可用于数学验证软件或硬件是否按预期工作。实践中，自动推理常依赖称为SAT求解器的程序，这些程序判断描述系统约束的形式表达式是否可满足。SAT问题 notoriously 难以解决（它是原始的NP完全问题），SAT求解器使用各种巧妙技巧使其易于处理：流行SAT求解器包含数万行代码。但如何确保SAT求解器关于给定表达式可满足性的决策可靠？这些程序规模庞大，使用形式化分析验证它们将耗费巨大精力。

一种解决方案是让SAT求解器生成其推理过程的记录——即跟踪信息，可由自动证明检查器验证。证明检查器是相对简单的程序，比SAT求解器更易验证。对于所有约束可一次性指定的SAT问题（即使非常复杂的问题），已有方法可可靠生成机器可验证证明。然而，大多数实际情况下，SAT问题的约束无法一次性全部指定。通常，在验证代码、硬件或网络性能时，我们希望先检查一个约束，根据其是否适用再检查第二个约束，依此类推，逐步构建约束集。现有生成可检查证明的方法不适用于此类增量SAT问题。

在今年计算机辅助设计形式化方法会议（FMCAD）上，我们提出了一种为增量SAT问题生成可验证证明的方法。SAT问题由一长串约束组成，每个约束的表达式称为子句。为使SAT问题易于处理，SAT求解器会删除那些可通过与其他子句相同真值分配满足的子句。对于增量SAT问题，有时需要恢复已删除的子句，以确保在添加新约束时的一致性。在这种情况下，我们的证明生成方法将恢复的子句视为从未被删除。这一简单技巧使现有证明生成框架能推广到增量SAT问题。

增量SAT问题中的子句删除与恢复操作给证明生成带来挑战。我们的方法从跟踪信息的末尾开始逆向处理，存储恢复的子句；若后续发现相同子句的删除操作，则同时删除原始删除与后续恢复操作。清理完跟踪信息后，再从头开始按常规方式构建证明。由于删除的子句与表达式中剩余子句在可满足性上等价，其删除对后续证明步骤的有效性无影响——直到与新添加子句冲突时，被删除的子句会被重新添加。因此，将删除操作视为未发生不会影响证明的可靠性。

为评估该方法的实用性，我们修改了当前最流行的SAT求解器之一来实现它，并在包含300个增量SAT问题的数据集上测试，其中6个可满足，294个不可满足。修改后的求解器为所有294个不可满足案例生成了有效证明（6个可满足案例通过真值分配选择证明其可满足性）。该算法效率足以实用，生成1GB证明约需1分钟，相对于求解时间开销约为5%。 更多精彩内容 请关注我的个人公众号 公众号（办公AI智能小助手）