5

我试图在微软的 SMT 求解器 Z3 中证明一个归纳事实。我知道 Z3 通常不提供此功能,如Z3 指南(第 8 节:数据类型)中所述,但是当我们限制要证明事实的域时,这似乎是可能的。考虑以下示例:

(declare-fun p (Int) Bool)
(assert (p 0))

(assert (forall ((x Int)) 
    (=> 
    (and (> x 0) (<= x 20))
    (= (p (- x 1)) (p x) ))))
(assert (not (p 20)))

(check-sat)

求解器以 正确响应unsat,这意味着它(p 20)是有效的。问题是,当我们进一步放宽这个约束时(我们20在前面的例子中用任何大于 20 的整数替换),求解器的响应是unknown

我觉得这很奇怪,因为 Z3 解决最初的问题并不需要很长时间,但是当我们将上限增加 1 时,它突然变得不可能了。我试图向量词添加一个模式,如下所示:

(declare-fun p (Int) Bool)
(assert (p 0))

(assert (forall ((x Int)) 
    (! (=> 
    (and (> x 0) (<= x 40))
    (= (p (- x 1)) (p x) )) :pattern ((<= x 40)))))
(assert (not (p 40)))

(check-sat)

哪个似乎更好,但现在上限是 40。这是否意味着我可以更好地不使用 Z3 来证明这些事实,还是我错误地表述了我的问题?

4

1 回答 1

6

Z3 使用许多启发式方法来控制量词实例化。其中之一是基于“实例化深度”。Z3 用“深度”属性标记每个表达式。所有用户提供的断言都被标记为深度 0。当一个量词被实例化时,新表达式的深度会增加。Z3 不会使用标记为深度大于预定义阈值的表达式来实例化量词。在您的问题中,已达到阈值:(p 40)深度为 0,(p 39)深度为 1,(p 38)深度为 2,等等。

要增加阈值,您应该使用以下选项:

(set-option :qi-eager-threshold 100)

这是使用此选项的示例:http ://rise4fun.com/Z3/ZdxO 。

当然,使用这个设置,Z3 会超时,例如 for (p 110).

未来Z3会对“有界量化”有更好的支持。在大多数情况下,处理这种量词的最佳方法是扩展它。使用编程 API,我们可以在将表达式发送到 Z3 之前轻松“实例化”表达式。这是 Python 中的一个示例(http://rise4fun.com/Z3Py/44lE):

p = Function('p', IntSort(), BoolSort())

s = Solver()

s.add(p(0))
s.add([ p(x+1) == p(x) for x in range(40)])
s.add(Not(p(40)))

print s.check()

最后,在 Z3 中,包含算术符号的模式不是很有效。问题是Z3在求解之前对公式进行了预处理。然后,大多数包含算术符号的模式将永远不会匹配。有关如何有效使用模式/触发器的更多信息,请参阅这篇文章。作者还提供了一个幻灯片

于 2012-11-02T16:06:28.120 回答