为什么这个简单的Z3证明这么慢?

Question

以下 Z3 代码在联机 repl 上超时：

; I want a function
(declare-fun f (Int) Int)
; I want it to be linear
(assert (forall ((a Int) (b Int)) (
= (+ (f a) (f b)) (f (+ a b))
)))
; I want f(2) == 4
(assert (= (f 2) 4))
; TIMEOUT :(
(check-sat)

这个版本也是如此，它正在寻找实数上的函数：

(declare-fun f (Real) Real)
(assert (forall ((a Real) (b Real)) (
= (+ (f a) (f b)) (f (+ a b))
)))
(assert (= (f 2) 4))
(check-sat)

当我给它一个矛盾时，它会更快：

(declare-fun f (Real) Real)
(assert (forall ((a Real) (b Real)) (
= (+ (f a) (f b)) (f (+ a b))
)))
(assert (= (f 2) 4))
(assert (= (f 4) 7))
(check-sat)

我对定理证明者相当不了解。这里有什么这么慢的？证明者只是在证明 f(2) = 4 的线性函数存在时遇到了很多麻烦吗？

Answer 1

速度缓慢很可能是由于有问题的模式/触发器导致的量词实例过多。如果您还不知道这些，请查看 Z3 指南的相应部分。

底线：模式是一种语法启发式方法，向 SMT 求解器指示何时实例化量词。模式必须涵盖所有量化变量，并且模式中不允许使用加法(+)等解释函数。匹配循环是每个量词实例化都会产生进一步量词实例化的情况。

在您的情况下，Z3 可能会:pattern ((f a) (f b))选择模式集(因为您没有显式提供模式)。这表明 Z3 实例化每个a, b的量词，这些的基项(f a)和(f b)已经出现在当前证明搜索中。最初，证明搜索包含(f 2);因此，量词可以用绑定到2, 2的a, b来实例化。这会产生(f (+ 2 2))，它可以用来再次实例化量词(也可以与(f 2)结合使用)。因此，Z3 卡在匹配循环中。

这里有一个片段来论证我的观点：

(set-option :smt.qi.profile true)
(declare-fun f (Int) Int)
(declare-fun T (Int Int) Bool) ; A dummy trigger function
(assert (forall ((a Int) (b Int)) (! 
(= (+ (f a) (f b)) (f (+ a b)))
:pattern ((f a) (f b))
; :pattern ((T a b))
)))
(assert (= (f 2) 4))
(set-option :timeout 5000) ; 5s is enough
(check-sat)
(get-info :reason-unknown)
(get-info :all-statistics)

使用显式提供的模式，您将获得原始行为(对指定的超时进行模化)。此外，统计信息报告了量词的大量实例化(如果增加超时，则更多实例化)。

如果您注释第一个模式并取消注释第二个模式，即如果您使用不会显示在证明搜索中的虚拟触发器"保护"量词，则 Z3 将立即终止。不过，Z3仍然会报告unknown，因为它"知道"它没有考虑量化约束(这将是sat的要求;它也不能显示unsat)。

有时可以重写量词以获得更好的触发行为。例如，Z3指南在单射函数/反函数的上下文中说明了这一点。也许您可以在此处执行类似的转换。