MEMICS - Doctoral Workshop on Mathematical and Engineering Methods in Computer Science
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
Bit-precise reasoning is essential for many automated reasoning tasks and usually relies on SMT solvers for the theory of fixed-width bit-vectors. After applying simplification through rewriting these solvers usually rely on bit-blasting. The resulting propositional problem is then handed to SAT solvers. On the theoretical side we discuss the complexity of decision problems for bit-vectors. The main argument is that bit-blasting is actually exponential. We discuss subclasses where the exponential explosion is not immediate. On the practical side we show how to use local search for bit-vectors, which avoids bit-blasting. This approach is particularly effective on hard satisfiable bit-vector problems.
Sprache der Kurzfassung:
Englisch
Vortragstyp:
Hauptvortrag / Eingeladener Vortrag auf einer Tagung
Forschungs-