增量可满足性问题解决方案的正确性证明

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

不可满足SAT问题示例：前两个子句((x ∨ y)和(x ∨ ¬y))仅在x为真时可满足，而最后子句((¬x))要求x为假

解决方案是让SAT求解器生成推理记录（追踪），由自动证明检查器验证。证明检查器是相对简单的程序，比SAT求解器更容易验证。对于可一次性指定所有约束的SAT问题（即使非常复杂），存在可靠生成机器可验证证明的方法。然而在多数实际场景中，SAT问题的约束无法一次性指定。在验证代码、硬件或网络性能时，通常需要先检查一个约束，根据其适用性再检查第二个约束，依此逐步构建约束集。现有生成可检查证明的方法不适用于此类增量SAT问题。

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

增量SAT

SAT问题是使用变量名和布尔运算符∧（与）及∨（或）表达的约束序列。问题在于是否存在使表达式为真的变量真值分配。例如表达式(A ∨ B) ∧ (¬A ∨ ¬B)可满足，因为当A或B为真且另一个为假时表达式为真。该表达式有两个子句：(A ∨ B)和(¬A ∨ ¬B)。

随着子句数量增加，这一看似直接的问题变得难以处理。SAT求解器使用的简化技巧之一是：若某子句与第二子句的合取与第二子句单独 equisatisfiable（等可满足性），则删除该子句。“等可满足性"指两个表达式要么都可满足，要么都不可满足。

例如增量SAT问题包含子句(A ∨ B)和(¬A ∨ ¬B)，求解器可能保留第一子句并删除第二子句，因为(A ∨ B)与合取(A ∨ B) ∧ (¬A ∨ ¬B)等可满足。随后因是增量问题，添加两个新子句(A)和(B)。(A ∨ B) ∧ (A) ∧ (B)可满足，因为当A和B均为真时(A ∨ B)为真。但若A和B均为真时(¬A ∨ ¬B)为假，故需将其添加回表达式，否则SAT求解器可能给出错误答案。

当SAT求解器处理增量SAT问题删除子句时，会将其存储在称为重构栈的缓冲区中，并附带真值分配以确保能从求解器修改后的问题重构原始问题中的有效分配。当向问题表达式添加新子句时，若满足该子句所需的真值与重构栈中任何分配冲突，冲突子句将被恢复到问题表达式并重新评估。它们可能获得不同的真值分配——或求解器可能判定表达式不可满足。

算法上，此过程有效：确保SAT求解器的判断可靠。但其逻辑难以用形式化证明语言捕捉。因此尽管当前SAT求解器能解决增量SAT问题，它们很少尝试证明其解决方案的可靠性。

生成证明

这正是我们方法的用武之地。除从问题表达式删除子句外，SAT求解器还添加子句。这些添加由表达式中已有子句逻辑蕴含，故不影响可满足性，但可能使求解器更容易识别子句间的潜在冲突。

典型证明生成器逐步处理所有这些添加和删除的追踪，构建其有效性证明。我们的方法则从追踪末尾开始逆向工作。当发现证明中恢复子句的步骤时，将该子句存储在缓冲区；若后续（即追踪中较早位置）发现同一子句的删除，则直接删除原始删除和后续恢复操作。从底至上清理追踪后，再从上至下常规构建证明。

由于删除的子句与表达式中剩余子句等可满足，其删除对后续证明步骤有效性无影响——至少直到与新添加子句冲突点，此处被删除子句已被重新添加。因此将删除操作视为从未发生不会影响证明的可靠性。

为评估方法的实用性，我们修改了当前最流行的SAT求解器以实现该方法，并在包含300个增量SAT问题的数据集上测试，其中6个可满足、294个不可满足。修改后的求解器为所有294个不可满足案例生成了有效证明。（6个可满足案例通过真值分配选择证明可满足性。）我们的算法也足够高效实用，生成1GB证明约需1分钟，相对于求解时间开销约5%。