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的论文“Efficiently Solving Quantified Bit-Vector Formulas”的评论。QF_BV都是关于编码的问题。预处理起到了很大的作用。我从头开始为Z3 3.0构建了一个新的预处理堆栈和SAT求解器。新的预处理器比Z3 2.x中使用的要快得多，并且执行了更积极的简化。没有魔法，也没有花哨的技巧。在预处理步骤之后，Z3对所有内容进行位爆炸并调用新的SAT解算器。Z3不使用位向量的欠/过近似、字级算术推理或非线性运算符的特殊支持。顺便说一句，很少有求解器考虑到的一件事是，一些简化可能会局部减少公式的大小，但会在全局范围内增加公式的大小，因为它们会破坏共享。Z3还使用预处理步骤，尝试在线性和非线性位向量算术中增加共享量。