z3 - 为什么这个简单的 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 guide的相应部分。 .

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

在您的情况下，Z3 可能会选择模式集 :pattern ((f a) (f b)) (因为您没有明确提供模式)。这建议 Z3 为每个 a, b 实例化量词，其中基本项 (f a) 和 (f b) 已经出现在当前证据搜索。最初，证明搜索包含(f 2)；因此，可以使用绑定(bind)到 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 仍会报告未知，因为它“知道”它没有考虑量化约束(这将是 sat 的要求；而且它也无法显示不饱和)。

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