Satisfiability of Quantified Bit-Vector Formulas: Theory and Practice

Multiple modern applications, ranging from bioinformatics, through job scheduling, to software and hardware analysis rely on ability to decide satisfiability of a given formula in a given logical theory. This decision problem is called satisfiability modulo theories (SMT). This thesis focuses on one particular theory, which is of paramount importance in analysis of software and hardware: the theory of fixed-size bit-vectors. In particular, this thesis focuses on both theoretical and practical aspects of deciding satisfiability of bit-vector formulas that contain quantifiers. In the first part of the thesis, we investigate the precise computational complexity of satisfiability of quantified bit-vector formulas in which the values of bit-widths are encoded in binary or decimal notation, which is often the case in practice. Afterwards, we introduce an approach to deciding satisfiability of quantified bit-vector formulas by using binary decision diagrams and abstractions of bit-vector operations. We also the extend known simplifications of formulas that contain unconstrained variables, i.e., variables that occur only once in the formula. The thesis further describes our implementation of state-of-the-art SMT solver called Q3B, which uses the approach of solving satisfiability of quantified bit-vector formulas by binary decision diagrams and abstractions and also implements the simplifications using unconstrained variables. Experimental evaluation shows that the implemented solver Q3B outperforms other state-of-the-art solvers for quantified bit-vector formulas. Furthermore, we also investigate the dependence of satisfiability of quantified bit-vector formulas on the bit-widths of the used variables. We show that in most formulas coming from practical applications, the satisfiability of the formula remains the same even after reducing the bit-widths in the formula to very small values. Finally, we show how to use this observation to improve the performance of quantified bit-vector SMT solvers by using reductions of bit-widths in the input formula.