Z3统计解释

Question

我从Z3的运行中获得了几个统计数据。我要明白这些是什么意思。对于sat和SMT解决方案的最新发展，我相当生疏和不及时，因此我试图找出自己的解释，我可能完全错了。因此，我的主要问题是：

1)这些措施的名称意味着什么？

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

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

我的解释如下。

• DPLL.下面所有的度量都引用了DPLL算法的行话，DPLL算法是大多数求解者的基础。

- _:decisions_ 
    - Number of decisions

​

- _:propagations_ 
    - Number of propagations (I guess unit propagations)

​

- _:binary-propagations,_ :_ternary-propagations_ 
    - Propagations of two and three literals at once

​

- _:conflicts_ 
    - Number of conflicts

​

​

• 分辨率.粗略地说，操作使解释从句成为集；从解译中获得的技巧是解决SAT的另一种范式。

- _:subsumed_
- _:subsumption-resolution_ 
    - What is the difference between the above two?

​

- _:dyn-subsumption-resolution_ 
    - Should be described here: Learning for Dynamic Subsumption, by Hamadi et al.

​

​

• 其他技术

- _:minimized-lits_ 
    - No clear idea. Is it probably related with clause learning?

​

- _:probing-assigned_ 
    - I guess it counts the number of assignment made when "probing", which I guess is some kind of lookahead technique.

​

- _:del-clause_ 
    - Number of deleted clauses (for what reason? Redundant?)

​

- :_elim-literals_ :_elim-clauses_ :_elim-bool-vars_ :_elim-blocked-clauses_ 
    - 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.)

​

- _:restarts_ 
    - Number of restarts.

​

​

• 其他方面

- _:mk-bool-var_ :_mk-binary-clause_ :_mk-ternary-clause_ :_mk-clause_ 
    - Number of boolean variables and binary,ternary and generic clauses created. 

​

- _:memory_ 
    - Maximum amount of memory used.

​

- _:gc-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.

​

    - It is not always the case that  
        - :_gc-clause_<=:_elim-clauses_; it can also be :_gc-clause_ > :_elim-clauses_

​

​

​

Answer 1

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

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