解读Z3统计

Question

我从Z3的运行中获得了几个统计数据.我需要了解这些意味着什么.对于sat和SMT解决方案的最新发展,我相当生疏,并且没有及时更新,因此我试图自己找到解释并且我可能会出错.所以我的问题主要是:

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

2)如果错了,你能指点我更好地理解他们所指的内容吗？

其他观察结果如下,概念上属于上述两个问题.提前致谢!

我的解释如下.

• DPLL.下面的所有指标都参考了DPLL算法的行话,这是大多数求解器的基础.

  • :决定
    • 决定数量
  • :的传播
    • 传播次数(我猜单位传播)
  • :二进制传播,:三元传播
    • 一次传播两个和三个文字
  • :冲突
    • 冲突数量

• 决议.粗略地说,操作使解释条款成为集合; 从分辨率中获取的技术是解决SAT的另一种范例.

  • :归入
  • :包容分辨率
    • 上面两个有什么区别？
  • :DYN-包容分辨率
    • 应该在这里描述:学习动态包容,由Hamadi等人.

• 其他技术

  • :最小化,双床
    • 没有明确的想法.它可能与条款学习有关吗？
  • :探诊分配
    • 我想它会计算"探测"时所做的任务数量,我猜这是一种先行技术.
  • :德尔子句
    • 已删除子句的数量(出于什么原因？冗余？)
  • :elim-literals:elim-clauses:elim-bool-vars:elim-blocked-clauses
    • 消除elim后的实体数量.这些指标涉及特定的SAT解决技术(参见M.Järvisalo等人的参考阻止条款消除)
  • :重新启动
    • 重启次数.

• 其他方面

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

Answer 1

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

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