哪些统计数据表明Z3运行效率高？

Question

SMTLib2指令(get-info all-statistics)显示了一些数字，例如：

num. conflicts:     4
num. propagations:  0 (binary: 0)
num. qa. inst:      23

为了测试不同的公理化和编码，我想知道哪些数字适合声明一个 Z3 运行比另一个更好/更高效。

从名称上猜测，我认为“num. qa. inst”——量词实例数量——是一个很好的指标（越低越好），但其他指标如何呢？

- Malte Schwerhoff

Answer 1

量词实例数是检查公理化是否产生过多实例的好方法。您还可以使用QI_PROFILE=true。它将为每个量词生成统计信息。您可以使用属性：qid为量词命名。您还可以使用DEFAULT_QID=true，Z3将基于行号生成名称。QI_PROFILE_FREQ=将在生成每个实例后显示统计信息。这些选项有助于检测实例化循环。

"num. conflicts"有助于估计Z3遍历的搜索空间大小。如果搜索空间的大小较小，则可以说公理化更好。

祝好， Leo

- Leonardo de Moura

---

谢谢指出其他选项！但是其他数字呢，例如“num. decisions”？在基准测试Z3编码时应该考虑哪些数字？ - Malte Schwerhoff

“num.冲突”比“num.决策”更相关。另外，Z3 使用非时间顺序回溯。因此，n 决策并不意味着 Z3 探索了2^n个分支。“num.冲突”大约等于 Z3 探索的分支数。还有其他有用的数字来检测理论推理中的瓶颈。例如，“主元素”--> Z3 在线性算术方面有问题，“戈莫里割”-->整数算术，“界面方程”--> 理论组合等等。 - Leonardo de Moura