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

Question

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

我在论文 Efficiently Solveving Quantiified 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 不对位向量或字级算术推理或对非线性运算符的特殊支持使用欠/过近似。顺便说一句，很少有求解器考虑到的一件事是，一些简化可能会在局部减小公式的大小，但会在全局范围内增加它，因为它们破坏了共享。