我从 Z3 的运行中获得了几个统计数据。我需要明白这些是什么意思。
对于 sat 和 SMT 求解的最新发展，我相当生疏且不了解最新情况，因此我试图自己寻找解释，但我可能完全错了。
所以我的问题主要是:
1) 措施的名称是什么意思？
2)如果错了，您能否给我指点以更好地理解它们所指的内容？
其他意见如下，在概念上属于上述两个问题。
提前致谢!
我的解释如下。
DPLL .以下所有指标均指 DPLL 算法的行话，这是大多数求解器的基础。
:决定
决策数量 :传播
传播次数(我猜是单位传播) :binary-propagations, :ternary-propagations
一次传播两个和三个文字 :冲突
冲突数量 分辨率 .粗略地说，操作使从句解释为集合；从分辨率中获取的技术，这是解决 SAT 的另一种范式。
:包含 :包含分辨率
以上两者有什么区别？ :dyn-包含分辨率
应该在这里描述:学习动态包容，哈马迪等人。 其他技术
:minimized-lits
没有明确的想法。它可能与子句学习有关吗？ :探测分配
我猜它会计算“探测”时所做的分配数量，我猜这是某种前瞻技术。 :del 子句
已删除子句的数量(出于什么原因？冗余？) :elim-literals :elim-clauses :elim-bool-vars :elim-blocked-clauses
elim 消除后的实体数。
这些指标指的是特定的 SAT 求解技术
(参见 M.Järvisalo 等人的 Blocked Clause Elimination 引用资料) :重启
重启次数。 其他方面
:mk-bool-var :mk-binary-clause :mk-ternary-clause :mk-clause
创建的 bool 变量和二元、三元和泛型子句的数量。 :内存
使用的最大内存量。 :gc 子句
垃圾收集条款...？ 根据我的实验，这种解释是合理的，因为情况总是如此
:gc-clause <= :del-clause ;就我而言，不平等现象很严重。 情况并非总是如此
:gc-clause<=:elim-clauses;它也可以是 :gc-clause > :elim-clauses
恐怕这是一个开放式问题。
Z3 公开了许多以多种不同方式收集的计数器。
虽然许多捕获抽象概念，但它们的含义最终是
基于代码的实现行为。
幸运的是，源代码可用并提供了完整的上下文
了解每个计数器的行为。所以没有单
跟踪计数器含义的文档，但源代码
提供完整的上下文。