z3 - Z3 使用什么方法来求解无量词位向量公式 (QF_BV)？

Question

特别是，它是否使用 DPLL(T)？它是否使用欠/过近似？它是否处理单词级别的线性算术？非线性算术呢？

我在论文 Efficiently Solving Quantified Bit-Vector Formulas 中只发现表面上提到了“类似于 MathSAT/Boolector 中的简化”。 .

非常有趣的是，是什么方法帮助Z3在smtcomp的QF_BV部分获得了第一名。

Answer 1

DPLL(T) 根本不用于解决 QF_BV 问题。
关于“有效求解量化位向量公式”一文的评论是关于 Z3 2.x 的。
QF_BV 是关于问题编码的。预处理有很大的不同。
我从头开始为 Z3 3.0 构建了一个新的预处理堆栈和 SAT 求解器。
新的预处理器比 Z3 2.x 中使用的预处理器快得多，并且执行更积极的简化。
没有魔法，或花哨的技术。在预处理步骤之后，Z3 对所有内容进行位爆破并调用新的 SAT 求解器。
Z3 不使用位向量的欠/过近似，或字级算术推理，或对非线性运算符的特殊支持。
顺便说一句，很少有求解器考虑到的一件事是，一些简化可能会在本地减少公式的大小，但会在全局范围内增加它，因为它们破坏了共享。
Z3 还使用了一个预处理步骤，试图增加线性和非线性位向量算法中的共享量。