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

Question

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

Mal*_*off 3 statistics encoding solver smt z3

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

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

Run Code Online (Sandbox Code Playgroud)

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

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

Answer 1

Leo*_*ura 5

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

“数量冲突”对于估计Z3遍历的搜索空间的大小很有用。我们可以说，如果搜索空间的大小较小，则公理化会“更好”。

干杯，狮子座

“数量冲突”比“数量决定”重要得多。顺便说一句，Z3使用非按时间顺序回溯。因此，n个决策并不意味着Z3探索了2 ^ n个分支。“冲突数量”大约等于Z3探索的分支数量。还有其他一些数字可用于检测理论推理中的瓶颈。例如，“枢轴”-> Z3在使用线性算法时遇到问题，“切分”->整数算法，“接口等式”->理论组合等。 (2认同)

归档时间：	14 年，2 月前
查看次数：	704 次
最近记录：	14 年，2 月前