Andreas Fröhlich,
"Theoretical and Practical Aspects of Bit-Vector Reasoning"
, 3-2016
Original Titel:
Theoretical and Practical Aspects of Bit-Vector Reasoning
Sprache des Titels:
Englisch
Original Kurzfassung:
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.
Forschungs-