boolean-logic - SAT真实编程场景

Question

我阅读了有关 SAT 和 SMT 的信息。我一直想知道如何将它应用到实际的编程场景中。

这是一个例子：

鉴于这var a = 20; var b = a;是真的，我们想知道b = 20是真的还是假的。

我应该如何将其转换为布尔代数表达式并应用 SAT？

Answer 1

这是使用许多 SMT 求解器支持的 SMT-LIB 2.0 标准的最简单示例：

(declare-fun a () Int)
(declare-fun b () Int)
(assert (= a b))
(assert (= a 20))
(assert (= b 20))
(check-sat)

您可以使用http://rise4fun.com/z3进行试验。它将响应“sat”，表示可以满足断言，这意味着 b可以是 20。

然后您可以将 (assert (= b 20)) 替换为 (assert (distinct b 20))。Z3 将以“unsat”响应，这意味着 b 不可能是其他任何东西。