Satisfiability Modulo Theories (SMT) is a broad field of research and an important topic for many practical applications. In this thesis, we focus on theories of bit-vectors as used, e.g., in hardware and software verification, but also in many other areas. In particular, 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. We show that 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. As one of our central results, 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 ν-NEXPTIME-completeness result, when considering bit-vector logics with ν-logarithmic scalar encodings. We further analyze how the choice of operators affects the expressiveness of certain bit-vector logics and can lead to specific fragments of quantifier-free bit-vector logics that are PSPACE-complete or NP-complete. On the practical side, this implies that the bit-blasting followed by the use of a CDCL (conflict driven clause learning) SAT solver, which is the common approach in state-of-the-art bit-vector solvers, can be exponential. Our complexity results directly point to several possibilities for new solving approaches, proposing reductions to model checking (for the PSPACE-complete 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. |