Z3统计学解释

Question

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

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

2） 如果错了，你能给我一些建议，让我更好地理解它们指的是什么吗？

其他意见如下，在概念上属于上述两个问题。提前感谢！

我的解释如下。

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

  • ：决策
    • 决策数量
  • ：传播
    • 传播次数（我猜是单位传播）
  • ：二进制传播，：三元传播
    • 同时传播两种和三种文字
  • ：冲突
    • 冲突数量

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

  • ：包含
  • ：包容决议
    • 以上两者有什么区别
  • ：dyn包含分辨率
    • 应该在这里描述：动态抽取的学习，由Hamadi等人

• 其他技术

  • ：最小化lits
    • 没有明确的想法。这可能与从句学习有关吗
  • ：已分配探测
    • 我想它计算的是"探测"时所做的任务数量，我想这是某种前瞻性技术
  • ：del条款
    • 删除条款的数量（出于什么原因？多余？）
  • ：elim literals：：elim bool vars：elim阻塞子句
    • 消除elim-之后的实体数。这些指标指的是特定的SAT解决技术（参考M.Järvisalo等人的"阻止条款消除"）
  • ：重新启动
    • 重新启动的次数

• 其他方面

  • ：mk bool var：mk二进制子句
    • 创建的布尔变量以及二进制、三元和泛型子句的数目
  • ：内存
    • 已使用的最大内存量
  • ：gc子句
    • 垃圾回收条款
    • 根据我的实验，这种解释是合理的，因为总是这样
      • ：gc子句<=：del子句；就我而言，质量是严格的
    • 并非总是这样
      • ：gc子句<=：elim子句；它也可以是：gc子句>：elim子句

Answer 1

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

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