在Z3中证明归纳事实

Question

我试图在微软的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解决原始问题并不需要很长时间，但当我们将上限增加一时，它突然变得不可能。我尝试添加一个量词模式，如下所示：

(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来证明这些事实，还是我的问题表述有误？

- marczoid

Answer 1

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会超时，例如对于(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 在解决问题之前会对公式进行预处理，这意味着大多数包含算术符号的模式将无法匹配。关于如何有效地使用模式/触发器的更多信息，请参见这篇文章。作者还提供了一个幻灯片展示。

- Leonardo de Moura

---

非常感谢，非常有帮助！也许有一些资源可以提供更多关于所有可设置选项的信息？我知道这个列表(http://research.microsoft.com/en-us/um/redmond/projects/z3/config.html)，但那相当简洁，我希望可能会有更详细的解释。 - marczoid

很遗憾，我们没有详细描述选项的文档/页面。我正在尝试将Z3移动到一个新的参数设置框架中，其中每个组件都有自己的参数和文档。待办列表中的另一项任务是从您在评论中引用的列表中删除过时的选项。 - Leonardo de Moura

文章和幻灯片的链接已经失效。 - Kevin

@Kevin，你可以在moskal.me/pdf/prtrig.pdf和moskal.me/pdf/prtrig-slides.pdf上找到链接。 - Parth Thakkar