Theoretical and Practical Aspects of Bit-Vector Reasoning

In this thesis, we focus on theories of bitvectors as used, e.g., in hardware and software verification, etc. We discuss satisfiability of bit-vector logics and related problems. The satisfiability problem of propositional formulas (SAT) is a well-known NP-complete problem. In the past, satisfiability for quantifier-free bit-vector logics was often assumed to be NP-complete as well. Several earlier complexity results for bit-vector logics only hold if a unary encoding for scalars is used. Instead, complexity for many decision problems grows significantly, if a more succinct logarithmic encoding is used for representation. We prove that satisfiability of quantifier-free bit-vector formulas turns out to be NEXPTIME-complete. We also show that similar results can be obtained for satisfiability of quantified bit-vector logics with uninterpreted functions (2-NEXPTIME-complete), and can even be extended to multi-logarithmic encodings. For the latter case, we give a very general v-NEXPTIME-completeness result, when considering bit-vector logics with v-logarithmic scalar encodings. We further analyze how the choice of operators affects the expressiveness of certain bitvector logics and can lead to specific fragments of quantifier-free bit-vector logics that are PSPACE-complete or NP-complete. This implies that the bit-blasting followed by the use of a CDCL (conflict driven clause learning) SAT solver can be exponential. Our complexity results directly point to several possibilities for new solving approaches, proposing reductions to model checking (for the PSPACEcomplete fragment), to EPR (for the general, NEXPTIME-complete class), or by applying SLS (stochastic local search) directly on the theory level. We also develop two algorithms for solving Dependency Quantified Boolean Formulas (DQBF), a further NEXPTIME-complete problem, either using a DPLL based algorithm or an instantiation based approach, similar to the one applied in EPR solving.