z3 - Z3 中的后果

Question

Z3 能够推导出该理论的 bool 结果，如 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

这与之前的堆栈溢出问题非常相似:Using SMT-LIB to count the number of modules using a formula

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

如果你不关心不连续性，只想找出最大/最小值，你可以使用 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 中的优化求解器与常规求解器相比肯定更慢。但它可能只是解决您的问题领域!