时间戳

首页 > 解决方案 > Z3 中的后果

z3 - Z3 中的后果

问题描述

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 之间。

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

标签： z3propagation

解决方案

这与之前的堆栈溢出问题非常相似：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），您还可以将 +/- infinity 作为边界：

(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 中的优化求解器与常规求解器相比肯定要慢一些。但它可能只是为您的问题域解决问题！

推荐阅读