Z3不同smt.qi.eager_threshold配置下运行时间差异大但日志一致问题

我有两个仅set-option :smt.qi.eager_threshold配置不同的smt2文件，分别将该参数设置为30和60。使用Z3 4.8.5版本运行时，前者耗时约45秒，后者耗时约55秒，进一步提高该参数值时，运行时间差距会进一步拉大。

我原本推测该差异的原因是阈值越高，Z3实例化的量词数量越多，因此参考axiom profiler和Dafny的官方指导，添加trace=true proof=true参数重新运行Z3，记录所有量词实例化情况。开启日志功能后Z3运行耗时大幅上升，两个文件分别耗时5分钟和10分钟，但意外的是两份运行日志几乎完全一致，仅末尾部分形如0x7f8404159430的标识符（疑似内存指针）存在差异，这类差异可忽略，diff对比示例如下：

...
195284,195294c195284,195294
< [new-match] 0x7f8404159430 #60259 #1223 #4938 #107732 ; #109421 (#4956 #4956)
< [new-match] 0x7f8404159468 #68823 #4926 #11519 #11523 ; #109090 (#4902 #4902)
< [new-match] 0x7f84041594a0 #72403 #6078 #11519 #11527 ; #109128 (#6054 #6054)
< [new-match] 0x7f84041594d8 #79964 #6078 #11519 #11527 ; #109128 (#6054 #6054)
< [new-match] 0x7f8404159510 #77477 #7869 #11519 #11531 ; #109155 (#7434 #7434)
< [new-match] 0x7f8404159548 #80168 #7869 #11519 #11531 ; #109155 (#7434 #7434)
< [new-match] 0x7f8404159580 #895 #894 #107821 #1141 ; #109377
< [new-match] 0x7f84041595b8 #895 #894 #107864 #1141 ; #109400
< [new-match] 0x7f84041595f0 #12897 #647 #4938 ; #4956
< [new-match] 0x7f8404159620 #648 #647 #4938 ; #4956
< [new-match] 0x7f8404159650 #12793 #647 #4938 ; #4956
---
> [new-match] 0x7fa96b39c230 #60259 #1223 #4938 #107732 ; #109421 (#4956 #4956)
> [new-match] 0x7fa96b39c268 #68823 #4926 #11519 #11523 ; #109090 (#4902 #4902)
> [new-match] 0x7fa96b39c2a0 #72403 #6078 #11519 #11527 ; #109128 (#6054 #6054)
> [new-match] 0x7fa96b39c2d8 #79964 #6078 #11519 #11527 ; #109128 (#6054 #6054)
> [new-match] 0x7fa96b39c310 #77477 #7869 #11519 #11531 ; #109155 (#7434 #7434)
> [new-match] 0x7fa96b39c348 #80168 #7869 #11519 #11531 ; #109155 (#7434 #7434)
> [new-match] 0x7fa96b39c380 #895 #894 #107821 #1141 ; #109377
> [new-match] 0x7fa96b39c3b8 #895 #894 #107864 #1141 ; #109400
> [new-match] 0x7fa96b39c3f0 #12897 #647 #4938 ; #4956
> [new-match] 0x7fa96b39c420 #648 #647 #4938 ; #4956
> [new-match] 0x7fa96b39c450 #12793 #647 #4938 ; #4956
...

核心疑问 #

如果Z3的运行日志完全一致，为什么运行时间会存在如此大的差异？是否是因为即便证明探索过程完全相同，阈值更高的运行任务中Z3分配了更大的数据结构导致耗时上升？

我进行了多组测试，排除了Z3随机种子导致差异的可能性。看起来我的smt2文件存在一个最优的smt.qi.eager_threshold取值：提高该值时，Z3耗时呈指数级增长但日志保持不变；降低该值时，Z3耗时同样会上升，且符合预期地部分unsat求解结果会变为unknown，同时日志内容也会发生变化。

统一配置参数 #

我使用的smt2文件统一配置参数如下：

(set-option :auto_config false)
(set-option :type_check true)
(set-option :smt.case_split 3)
(set-option :smt.delay_units true)
(set-option :smt.arith.solver 2)
(set-option :smt.mbqi false)
(set-option :model.compact false)
(set-option :model.v2 true)
(set-option :pp.bv_literals false)

运行统计数据 #

开启trace=true proof=true参数时，低阈值（30）文件的Z3运行统计数据如下：

(:added-eqs            294
 :arith-assert-lower   1
 :arith-assert-upper   5
 :arith-eq-adapter     1
 :conflicts            1
 :del-clause           90
 :max-generation       2
 :max-memory           527.79
 :memory               23.39
 :mk-bool-var          6726
 :mk-clause            5174
 :num-allocs           87550496
 :num-checks           1
 :propagations         5105
 :quant-instantiations 78
 :rlimit-count         278808
 :time                 0.01
 :total-time           300.06)

高阈值（60）文件的运行统计数据如下：

(:added-eqs            294
 :arith-assert-lower   1
 :arith-assert-upper   5
 :arith-eq-adapter     1
 :conflicts            1
 :del-clause           90
 :max-generation       2
 :max-memory           682.75
 :memory               23.39
 :mk-bool-var          6726
 :mk-clause            5174
 :num-allocs           147909479
 :num-checks           1
 :propagations         5105
 :quant-instantiations 78
 :rlimit-count         278808
 :time                 0.01
 :total-time           617.86)

可以看到第二种高阈值配置下的num-allocs值比低阈值配置高出70%。

内容的提问来源于stack exchange，提问作者Federico