7

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

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

2）如果错了，你能给我指点以更好地理解他们所指的吗？

其他观察如下，概念上属于上述两个问题。提前致谢！

我的解释如下。

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

    • ：决定
      • 决定数
    • :传播
      • 传播次数（我猜是单位传播）
    • :binary-propagations, :三元传播
      • 一次传播两个和三个文字
    • ：冲突
      • 冲突数

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

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

  • 其他技术

    • :minimized-lits
      • 没有明确的想法。它可能与从句学习有关吗？
    • :probing-assigned
      • 我猜它计算了“探测”时所做的分配数量，我猜这是某种前瞻技术。
    • :del 子句
      • 删除子句的数量（出于什么原因？冗余？）
    • : elim-literals : elim-clauses : elim-bool-vars : elim-blocked-clauses
      • 消除后的实体数量。这些指标指的是特定的 SAT 求解技术（参见 M.Järvisalo 等人的 Blocked Clause Elimination，以获取参考）
    • :重启
      • 重启次数。

  • 其他方面

    • :mk-bool-var : mk-binary-clause : mk-ternary-clause : mk-clause
      • 创建的布尔变量和二元、三元和通用子句的数量。
    • ：记忆
      • 使用的最大内存量。
    • :gc 子句
      • 垃圾回收条款...？
      • 根据我的实验，这种解释是合理的，因为情况总是如此
        • : gc-clause <= : del-clause ; 就我而言，不平等是严格的。
      • 并非总是如此
        • : gc-clause <=: elim-clauses ; 它也可以是：gc-clause > : elim-clauses
4

1 回答 1

1

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

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

于 2013-09-06T15:24:56.463 回答