What methods does Z3 use to solve quantifier-free bit-vector formulas (QF_BV)?

Question

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.

Answer 1

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.