Z3 中的后果

Question

Z3 能够推导出理论的布尔结果，如 https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-consequences

中所述

现在我想知道是否也可以对数值执行此操作。例如给出以下理论：

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(assert (= (+ x y) 10))
(assert (and (>= y 20) (>= x -20)))
(check-sat)
(get-model)

我想知道是否可以推导出 "y" 必须介于 20 和 30 之间，而 x 必须介于 -20 和 -10 之间。

我能想出的一个解决方法是最大化和最小化这些变量，然后我会得到可能性的范围，但在我看来，可以有更好的方法来做到这一点。

Answer 1

这与之前的堆栈溢出问题非常相似：

底线：如果涉及的变量不止一个，那么这个问题一般很难解决；除非您使用问题的特定知识。如果只有一个变量，那么你确实可以使用优化和其他技巧来给你 "ranges"，但通常这样的算法不一定是高性能的。（虽然在实践中它可以轻松处理最简单的事情。）

如果你不关心不连续性，只想找出max/min，你可以使用z3的优化器。请注意，这不是标准 SMTLib 的一部分，而是 z3 扩展。这是一个例子：

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(assert (= (+ x y) 10))
(assert (and (>= y 20) (>= x -20)))

(assert (distinct x (- 15)))
(assert (distinct y 25))

(push) (minimize y) (check-sat) (get-objectives) (pop)
(push) (maximize y) (check-sat) (get-objectives) (pop)
(push) (minimize x) (check-sat) (get-objectives) (pop)
(push) (maximize x) (check-sat) (get-objectives) (pop)

这会打印：

sat
(objectives
 (y 20)
)
sat
(objectives
 (y 30)
)
sat
(objectives
 (x (- 20))
)
sat
(objectives
 (x (- 10))
)

因此，您可以获得范围，但请注意我添加的 x != -15 和 y != 25 的要求如何超出您获得的范围。

请注意，如果您的类型是无界的（例如 Int），您还可以获得 +/- 无穷大作为边界：

(declare-const x Int)
(assert (< x 10))
(push) (minimize x) (check-sat) (get-objectives) (pop)
(push) (maximize x) (check-sat) (get-objectives) (pop)

这会打印：

sat
(objectives
 (x (* (- 1) oo))
)
sat
(objectives
 (x 9)
)

优化通常是一个难题，z3 中的优化求解器与常规求解器相比肯定更慢。但它可能只是解决您的问题领域！

Z3 中的后果

Consequences in Z3

propagation

z3