z3 - Z3统计的解释

我从Z3的运行中获得了一些统计数据。我需要了解这些意思。
对于sat和SMT解决方案的最新发展，我颇为生疏，不了解最新信息，因此，我试图自己寻找解释，而我可能会犯错。
所以我的问题主要是:

1)措施名称是什么意思？

2)如果有错，您能否给我指点以更好地理解它们所指的内容？

其他意见在下面进行，从概念上来说，属于上述两个问题。
提前致谢!

我的解释如下。

DPLL 。以下所有指标均指DPLL算法的行话，而DPLL算法是大多数求解器的基础。

:决定

决策数量

:传播

传播数量(我想单位传播)

:二进制传播，:三元传播

一次传播两个和三个文字

:冲突

冲突数

解决方案。粗略地说，运算将解释子句设置为集合。从分辨率中获取的技术，这是解决SAT的另一范式。

:包含在

中

:包含分辨率

两者之间有什么区别？

:dyn包含分辨率

应该在此处进行描述:Hamadi等人的“动态包容的学习”。

其他技术

:最小化

不清楚。它可能与从句学习有关吗？

:探测分配

我想它计算的是“探测”时进行的分配数量，我想这是某种先行技术。

:del-clause

删除的子句数(由于什么原因？冗余？)

:elim-literals:elim子句:elim-bool-vars:elim-blocked子句

消除后的实体数。
这些度量标准涉及特定的SAT解决技术
(请参阅M.Järvisalo等人的引用，《消除子句消除》)

:重新启动

重新启动次数。

其他方面

:mk-bool-var:mk-binary-clause:mk-ternary-clause:mk-clause

创建的 bool 变量和二进制，三进制和泛型子句的数量。

:内存

已使用的最大内存量。

:gc子句

垃圾收集条款...？

根据我的实验，这种解释是合理的，因为在这种情况下

:gc-clause

并非总是这样

:gc-clause :elim-clauses

最佳答案

恐怕这是一个开放性问题。
Z3公开了许多以许多不同方式收集的计数器。
尽管许多捕获抽象概念，但它们的最终含义是
基于代码的实现行为。

幸运的是，源代码可用并且提供了完整的上下文
了解每个计数器的行为。所以没有一个
跟踪计数器含义的文档，但是源代码
提供完整的上下文信息。

关于z3 - Z3统计的解释，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/18491922/