encoding - 哪些统计数据表明 Z3 的有效运行？

Question

SMTLib2 指令(get-info all-statistics)显示几个数字，例如

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

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

从名字猜我会说num. qa. inst- 量词实例化的数量 - 是一个很好的指标（更低=更好），但其他呢？

Answer 1

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

“num. conflict”对于估计 Z3 遍历的搜索空间的大小很有用。如果搜索空间的大小更小，我们可以说公理化“更好”。

干杯，狮子座