Z3统计解读

Question

我从 Z3 的运行中获得了一些统计数据。我需要明白这些是什么意思。 对于 sat 和 SMT 解决方案的最新发展，我相当生疏且不了解最新情况，因此我试图自己寻找解释，但我可能大错特错。 所以我的问题主要是：

1) 度量的名称是什么意思？

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

以下是其他观察结果，在概念上属于上述两个问题。 提前致谢！

我的解释如下。

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

  • :决定
    • 决策数量
  • :传播
    • 传播次数（我猜是单位传播）
  • ：二元传播，：三元传播
    • 同时传播两个和三个字面量
  • ：冲突
    • 冲突次数

• 分辨率。粗略地说，操作将解释子句作为集合；从分辨率中提取的技术，这是解决 SAT 的另一种范式。

  • :包含
  • :包容分辨率
    • 以上两者有什么区别？
  • :dyn-subsumption-resolution
    • 应在此处描述：Learning for Dynamic Subsumption，作者 Hamadi 等人。

• 其他技术

  • :最小化光
    • 没有明确的想法。可能和从句学习有关？
  • :探测分配
    • 我猜它会计算“探测”时所做的分配数，我猜这是某种前瞻技术。
  • :删除子句
    • 删除子句的数量（出于什么原因？冗余？）
  • :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
    • 创建的布尔变量和二元、三元和通用子句的数量。
  • :记忆
    • 已使用的最大内存量。
  • :gc 子句
    • 垃圾收集子句...？
    • 根据我的实验，这种解释是合理的，因为总是这样
      • :gc-clause del-clause ;就我而言，不等式是严格的。
    • 并非总是如此
      • :gc 子句elim 子句;也可以是 :gc-clause > :elim-clauses

Answer 1

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

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