# zbMATH — the first resource for mathematics

Complexity of fixed-size bit-vector logics. (English) Zbl 1357.68086
Summary: Bit-precise reasoning is important for many practical applications of Satisfiability Modulo Theories (SMT). In recent years, efficient approaches for solving fixed-size bit-vector formulas have been developed. From the theoretical point of view, only few results on the complexity of fixed-size bit-vector logics have been published. Some of these results only hold if unary encoding on the bit-width of bit-vectors is used. In our previous work [the authors, “On the complexity of fixed-size bit-vector logics with binary encoded bit-width”, in: Proceedings of the 10th international workshop on satisfiability modulo theories, SMT’12. Amsterdam: Elsevier. 44–55 (2012)], we have already shown that binary encoding adds more expressiveness to various fixed-size bit-vector logics with and without quantification. In a follow-up work [the authors, Lect. Notes Comput. Sci. 7913, 378–390 (2013; Zbl 1345.68172)], we then gave additional complexity results for several fragments of the quantifier-free case. In this paper, we revisit our complexity results from the authors’ papers cited above and go into more detail when specifying the underlying logics and presenting the proofs. We give a better insight in where the additional expressiveness of binary encoding comes from. In order to do this, we bring together our previous work and propose several new complexity results for new fragments and extensions of earlier bit-vector logics. We also discuss the expressiveness of various bit-vector operations in more detail. Altogether, we provide the currently most complete overview on the complexity of common bit-vector logics.

##### MSC:
 68Q25 Analysis of algorithms and problem complexity 68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
##### Software:
Boolector; bv2epr; iProver; MathSAT; MONA; NASA PVS; NuSMV; SMT-LIB; STP; Yices; z3
Full Text: