z3 - SAT/SMT 求解器中的变量消除

Question

在 SMT/SAT 求解中，是否有一些技术可以从公式中确定不相关的变量？即那些可以有任何值并且不影响公式可满足性的那些。

Answer 1

对于命题可满足性的情况，公式是从句的合取，每个子句都是文字的析取。例如(A | B) & (!B | A) & (!A | B | A)

如果一个变量在整个公式中仅作为正字面量或仅作为负数字面出现，则可以安全地删除它，并且可以删除它出现的任何子句并将其视为满足。但从严格意义上讲，这样一个变量的值并不是无关紧要的，因为它可能是唯一可以在满足某些公式的赋值中满足这些子句的变量。此类变量称为纯变量，此阶段称为纯字面消除。

在纯字面消除之前，应清理公式，以便删除包含既未否定又出现否定的变量的任何子句。这可能导致一些变量变得纯粹。此外，在整个求解过程中，当一个变量被识别为纯变量时，它应该被消除。

例如，子句(!A | B | A)被平凡满足：无论 A 取什么值，它都被满足。

然后(A | B) & (!B | A) & (!A | B | A)->(A | B) & (!B | A)

现在 A 是纯的并且可以设置为 True 导致找到令人满意的分配。请注意，无需做出任何决定即可找到解决方案，我们只需应用两个规则。