Titelaufnahme

Erfüllbarkeit Modulo einer Theorie (SMT) ist ein breites Forschungsgebiet mit vielen praktische Anwendungen. Diese Dissertation setzt ihren Fokus auf Theorien über Bitvektoren, wie sie zum Beispiel in der Hardware und Software Verfikation - aber auch in vielen anderen Bereichen - Verwendung finden. Insbesondere diskutieren wir die Erfüllbarkeit von Bitvektor-Logiken und verwandte Probleme. Das Erfüllbarkeitsproblem der Aussagenlogik (SAT) ist ein sehr bekanntes NP-vollständiges Problem. Bisher wurde oft angenommen, dass das Erfüllbarkeitsproblem für quantorenfreie Bitvektor-Logiken ebenfalls NP-vollständig sei. Wir zeigen, dass viele frühere Komplexitäts-Resultate für Bitvektor-Logiken nur dann gelten, wenn enthaltene Skalare unär kodiert werden. Im Gegensatz dazu steigt die Komplexität vieler Entscheidungsprobleme drastisch, wenn eine kompaktere logarithmische Kodierung zur Darstellung verwendet wird. Unter anderem beweisen wir, dass das Erfüllbarkeitsproblem für quantorenfreie Bitvektor Formeln NEXPTIME-vollständig ist. Des Weiteren zeigen wir, dass vergleichbare Resultate auch für das Erfüllbarkeitsproblem von quantifizierten Bitvektor-Logiken mit uninterpretierten Funktionen (2-NEXPTIME-vollständig), sowie für Logiken mit multi-logarithmisch kodierten Skalaren gelten. Für den zweiten Fall zeigen wir ν-NEXPTIME-Vollständigkeit, wenn eine ν-logarithmische Kodierung für Skalare verwendet wird. Wir analysieren zudem, wie sich die Wahl der Operatoren auf die Komplexität von verschiedenen Bitvektor-Logiken auswirkt und wie sie dazu führen kann, dass bestimmte Fragmente von quantorenfreien Bitvektor-Logiken PSPACE-vollständig oder NP-vollständig werden. Für die Praxis bedeuten unsere Resultate, dass der übliche Ansatz von Bitvektor Algorithmen, der "bit-blasting" mit der Verwendung von CDCL (konfliktgesteuerte Klauseln lernende) SAT Algorithmen kombiniert, exponentiell sein kann. Unsere Resultate eröffnen direkt mehrere neue Ansätze, z.B. durch Modellprüfung (für das PSPACE-vollständige Fragment), Übersetzung nach EPR (für die allgemeine, NEXPTIME-vollständige Klasse), oder Anwendung eines SLS (stochastische lokale Suche) Algorithmus direkt auf der Theorie-Repräsentation. Wir entwickeln zudem zwei Algorithmen um DQBF zu lösen, ein weiteres NE XP T IME-vollständiges Problem; entweder mit einem DPLL-basierten Algorithmus, oder durch einen auf Instanziierung basierenden Ansatz, ähnlich dem für EPR.

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.