我从Z3运行中获得了一些统计数据。我需要理解这些数据的含义。
由于我对sat和SMT求解的最新发展不太熟悉,因此我尝试自己找出解释,但可能是完全错误的。
所以我的问题主要包括:
1) 这些度量名称代表什么意思?
2) 如果有误,能否给我指点如何更好地理解它们?
其他观察结果将在下文中提出,概念上属于以上两个问题。 先在此致谢!
以下是我的解释。
1) 这些度量名称代表什么意思?
2) 如果有误,能否给我指点如何更好地理解它们?
其他观察结果将在下文中提出,概念上属于以上两个问题。 先在此致谢!
以下是我的解释。
DPLL. 下面所有的指标都是 DPLL 算法术语,这是大多数求解器的基础。
- :decisions
- 决策次数
- :propagations
- 传播次数(我猜测是单位传播)
- :binary-propagations, :ternary-propagations
- 同时传播两个和三个文字的次数
- :conflicts
- 冲突次数
- :decisions
RESOLUTION。将子句解释为集合所进行的操作,粗略地说;取自于解决 SAT 的另一个范例的技术-Resolution。
- :subsumed
- :subsumption-resolution
- 上述两者之间的区别是什么?
- :dyn-subsumption-resolution
- 应该在此处描述:由 Hamadi 等人撰写的学习动态子句消减。
其他技术
- :minimized-lits
- 没有明确的想法。它可能与子句学习有关吗?
- :probing-assigned
- 我猜它计算的是“探测”时所做的赋值次数,我猜测这是某种先行搜索技术。
- :del-clause
- 删除的子句数(为什么?冗余?)
- :elim-literals :elim-clauses :elim-bool-vars :elim-blocked-clauses
- elim-之后的实体数量。 这些指标涉及特定的 SAT 求解技术 (参见 M.Järvisalo 等人的 Blocked Clause Elimination 作为参考)
- :restarts
- 重启次数。
- :minimized-lits
其他方面
- :mk-bool-var :mk-binary-clause :mk-ternary-clause :mk-clause
- 创建的布尔变量和二元、三元和通用子句的数量。
- :memory
- 使用的最大内存量。
- :gc-clause
- 垃圾收集的子句…?
- 根据我的实验,这种解释是合理的,因为在我的情况下总是有
- :gc-clause <= :del-clause;这个不等式是严格的。
- 并非总是有
- :gc-clause<=:elim-clauses;也可能是:gc-clause > :elim-clauses
- :mk-bool-var :mk-binary-clause :mk-ternary-clause :mk-clause