Z3统计解读 [英] Interpretation of Z3 Statistics

问题描述

我从 Z3 的运行中获得了几个统计数据.我需要明白这些是什么意思.对于 sat 和 SMT 求解的最新发展，我相当生疏且不了解最新情况，因此我试图自己寻找解释，但我可能完全错了.所以我的问题主要是:

I obtained several statistics from runs of Z3. I need to understand what these mean. I am rather rusty and non up to date for the recent developments of sat and SMT solving, for this reason I tried to find explanations myself and I might be dead wrong. So my questions are mainly:

1) 度量的名称是什么意思?

1) What do the measures' names mean?

2) 如果错了，你能指点我更好地理解它们所指的是什么吗?

2) If wrong, can you give me pointers to understand better to what they refer to?

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

Other observations are made below and conceptually belong to the two questions above. Thanks in advance!

我的解释如下.

• DPLL.以下所有指标均参考了 DPLL 算法的术语，该算法是大多数求解器的基础.

• DPLL. All the metrics below refer to the jargon of the DPLL algorithm which is the foundation of most solvers.

• :决定
  • 决策数量
  • 传播次数(我猜是单位传播)
  • 同时传播两个和三个文字
  • 冲突数量

  解决方案.粗略地说，操作使从句解释为集合；取自分辨率的技术，这是求解 SAT 的另一种范式.

  RESOLUTION. Operations made interpreting clauses as sets, roughly speaking; techniques taken from resolution which is another paradigm for solving SAT.

  • :归入
  • :subsumption-resolution
    • 以上两者有什么区别?
    • 应在此处进行描述:Hamadi 等人的 Learning for Dynamic Subsumption.

    其他技术

    • :minimized-lits
      • 没有明确的想法.可能与子句学习有关吗?
      • 我猜它会计算探测"时分配的数量，我猜这是某种前瞻技术.
      • 已删除子句的数量(出于什么原因?多余的?)
      • elim- 消除后的实体数.这些指标指的是特定的 SAT 求解技术(参见 M.Järvisalo 等人撰写的 Blocked Clause Elimination 参考资料.)
      • Number of entities after the elim- eliminated. These metrics refer to particular SAT solving techniques (see for reference Blocked Clause Elimination, by M.Järvisalo et al.)
      • 重启次数.

      其他方面

      • :mk-bool-var :mk-binary-clause :mk-ternary-clause :mk-clause
        • 创建的布尔变量和二元、三元和泛型子句的数量.
        • 已使用的最大内存量.
        • 垃圾收集子句...?
        • 根据我的实验，这种解释是合理的，因为情况总是如此
          • :gc-clause <= :del-clause ;就我而言，这种不平等是很严重的.
          • Garbage-collected clauses ...?
          • This interpretation is plausible according to my experiments since it's always the case that
            • :gc-clause <= :del-clause ; in my case the disequality is strict.
            • :gc-clause<=:elim-clauses;它也可以是 :gc-clause > :elim-clauses
            • :gc-clause<=:elim-clauses; it can also be :gc-clause > :elim-clauses

            推荐答案

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

            I am afraid this is an open-ended question. Z3 exposes many counters that are collected in many different ways. While many capture abstract concepts, their meanings are ultimately based on implementation behaviors of the code.

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

            Fortunately the source code is available and provides the full context for understanding the behavior of each counter. So there is no single document that tracks the meaning of the counters, but the source code is made available to give the full context.

            这篇关于Z3统计解读的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！