Z3统计数据的解释

Question

我从Z3的运行中获得了一些统计数据。我需要了解这些含义。对于sat和SMT解决方案的最新发展，我感到非常生疏和陌生，因此，我试图自己寻找解释，而我可能会犯错。所以我的问题主要是：

1）措施的名称是什么意思？

2）如果错了，您能给我一些指导以更好地理解他们指的是什么吗？

以下其他意见在概念上属于上述两个问题。预先感谢！

我的解释如下。

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

  • ：决定
    • 决定数
  • ：传播
    • 传播次数（我想是单位传播）
  • ：binary-propagations，：ternary-propagations
    • 一次传播两个和三个文字
  • ：冲突
    • 冲突数

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

  • ：已包含
  • ：包含分辨率
    • 以上两者有什么区别？
  • ：dyn-subsumption-resolution
    • 应该在这里描述：Hamadi等人的动态包容学习

• 其他技术

  • ：minimized-lits
    • 不清楚。它可能与子句学习有关吗？
  • :: probing-assigned
    • 我想它计算“探测”时分配的数量，我想这是一种先行技术。
  • ：del-clause
    • 已删除子句的数量（由于什么原因？冗余？）
  • ：elim-literals：elim-clauses：elim-bool-vars：elim-blocked子句
    • 消除elim-之后的实体数。这些度量标准涉及特定的SAT解决技术（请参阅M.Järvisalo等人的参考，以“消除子句消除”）
  • ：重新启动
    • 重新启动次数。

• 其他方面

  • ：mk-bool-var：mk-二进制子句：mk-三元子句：mk-子句
    • 创建的布尔变量和二进制，三元和泛型子句的数量。
  • ：内存
    • 已使用的最大内存量。
  • ：gc-clause
    • 垃圾收集条款...？
    • 根据我的实验，这种解释是合理的，因为在这种情况下，
      • ：gc-clause <=：del-clause;就我而言，不平等是严格的。
    • 并非总是这样
      • ：gc子句 <=：elim子句;它也可以是：gc-clause>：elim-clauses>]

我从Z3的运行中获得了一些统计数据。我需要了解这些含义。对于sat和SMT解决方案的最新发展，我颇为生疏，不了解最新信息，因此，我试图...

Answer 1

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