特别是它是否使用DPLL(T)？它使用下/上近似值吗？它可以处理字级的线性算术吗？非线性算术呢？
我在论文 有效求解量化位向量公式。
非常有趣的是，是什么方法帮助Z3在smtcomp的QF_BV部分获得了第一名。
Particularly, does it use DPLL(T)? Does it use under/over approximations? Does it handle linear arithmetic on a word level? What about non-linear arithmetic?
I found only a superficial mention of "simplifications similar to those in MathSAT/Boolector" in paper Efficiently Solving Quantified Bit-Vector Formulas.
It is extremely interesting what methods helped Z3 to get the first place in QF_BV section of smtcomp.
发布评论
评论（1）
DPLL(T) 根本不用于解决 QF_BV 问题。
“有效求解量化位向量公式”论文的评论是关于 Z3 2.x 的。
QF_BV 是关于编码问题的。预处理有很大的不同。
我从头开始为 Z3 3.0 构建了一个新的预处理堆栈和 SAT 求解器。
新的预处理器比 Z3 2.x 中使用的预处理器快得多，并且执行更积极的简化。
没有魔法，也没有花哨的技术。预处理步骤之后，Z3 对所有内容进行位爆破并调用新的 SAT 求解器。
Z3 不使用位向量的欠/过近似，或字级算术推理，或对非线性运算符的特殊支持。
顺便说一句，很少有求解器考虑到的一件事是，一些简化可能会在局部减小公式的大小，但会在全局范围内增加公式的大小，因为它们破坏了共享。
Z3 还使用了一个预处理步骤，试图增加线性和非线性位向量算术中的共享量。
DPLL(T) is not used at all for solving QF_BV problems.
The comment on the paper “Efficiently Solving Quantified Bit-Vector Formulas” is about Z3 2.x.
QF_BV is all about problem encoding. Preprocessing makes a big difference.
I built a new preprocessing stack and SAT solver from scratch for Z3 3.0.
The new preprocessor is much faster than the one used in Z3 2.x and performs more aggressive simplifications.
There is no magic, or fancy techniques. After the preprocessing step, Z3 bit-blasts everything and invokes the new SAT solver.
Z3 does not use under/over approximation for bit-vectors, or word-level arithmetic reasoning, or special support for nonlinear operators.
BTW, one thing that few solvers take into account is that some simplifications may reduce the size of the formula locally, but increase it globally because they destroy sharing.
Z3 also uses a preprocessing step that tries to increase the amount of sharing in linear and nonlinear bit-vector arithmetic.