CEGAR SMT-Solving for Bit Vectors Arithmetic Seminar Satisfiability Checking

Bit vectors are an efficient representation of arithmetic problems. In this essay some techniques are introduced to transform bit-vector-arithmetic problems to satisfiability-equivalent propositional logic problems, whose satisfiability can be decided by SAT solvers. First, we describe how the problems can be translated into positional logic by flattening and decided by SAT solvers. We also introduce an improvement of this technique, incremental bit flattening.