Z3统计数据的解释

Question

我从Z3运行中获得了一些统计数据。我需要理解这些数据的含义。 由于我对sat和SMT求解的最新发展不太熟悉，因此我尝试自己找出解释，但可能是完全错误的。 所以我的问题主要包括：

1) 这些度量名称代表什么意思？

2) 如果有误，能否给我指点如何更好地理解它们？

其他观察结果将在下文中提出，概念上属于以上两个问题。 先在此致谢！

以下是我的解释。

• DPLL. 下面所有的指标都是 DPLL 算法术语，这是大多数求解器的基础。

  • :decisions
    • 决策次数
  • :propagations
    • 传播次数（我猜测是单位传播）
  • :binary-propagations, :ternary-propagations
    • 同时传播两个和三个文字的次数
  • :conflicts
    • 冲突次数

• RESOLUTION。将子句解释为集合所进行的操作，粗略地说；取自于解决 SAT 的另一个范例的技术-Resolution。

  • :subsumed
  • :subsumption-resolution
    • 上述两者之间的区别是什么？
  • :dyn-subsumption-resolution
    • 应该在此处描述：由 Hamadi 等人撰写的学习动态子句消减。

• 其他技术

  • :minimized-lits
    • 没有明确的想法。它可能与子句学习有关吗？
  • :probing-assigned
    • 我猜它计算的是“探测”时所做的赋值次数，我猜测这是某种先行搜索技术。
  • :del-clause
    • 删除的子句数（为什么？冗余？）
  • :elim-literals :elim-clauses :elim-bool-vars :elim-blocked-clauses
    • elim-之后的实体数量。 这些指标涉及特定的 SAT 求解技术 （参见 M.Järvisalo 等人的 Blocked Clause Elimination 作为参考）
  • :restarts
    • 重启次数。

• 其他方面

  • :mk-bool-var :mk-binary-clause :mk-ternary-clause :mk-clause
    • 创建的布尔变量和二元、三元和通用子句的数量。
  • :memory
    • 使用的最大内存量。
  • :gc-clause
    • 垃圾收集的子句…？
    • 根据我的实验，这种解释是合理的，因为在我的情况下总是有
      • ：gc-clause <= :del-clause；这个不等式是严格的。
    • 并非总是有
      • ：gc-clause<=:elim-clauses；也可能是：gc-clause > :elim-clauses

- gapag

---

这是一个很好的问题（连同部分答案），其他问题在SO上没有完全解决，但这里有一些相关的问题可能会有用：http://stackoverflow.com/questions/17856574/how-to-interpret-statistics-z3 http://stackoverflow.com/questions/10949633/z3-real-arithmetic-and-statistics http://stackoverflow.com/questions/7340888/z3-statistics-what-does-time-measure https://dev59.com/7VnUa4cB1Zd3GeqPcaW5 - Taylor T. Johnson

Answer 1

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

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

- Nikolaj Bjorner