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

Question

以下 Z3 代码在在线回复中超时：

; 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)；因此，量词可以用 a, b 绑定到 2, 2 来实例化。这会产生 (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)

使用明确提供的模式，您将获得原始行为（对指定超时取模）。此外，统计数据报告了大量量词的实例化（如果增加超时，还会更多）。

如果您注释第一个模式并取消注释第二个模式，即如果您 "guard" 带有不会出现在证明搜索中的虚拟触发器的量词，则 Z3 会立即终止。但是，Z3 仍会报告 unknown，因为它 "knowns" 它没有考虑量化约束（这将是 sat 的要求；并且它也无法显示 unsat).

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

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

Why is this simple Z3 proof so slow?

z3