- Computing and Information Systems - Theses
Computing and Information Systems - Theses
Permanent URI for this collection
1 results
Filters
Reset filtersSettings
Statistics
Citations
Search Results
Now showing
1 - 1 of 1
-
ItemA bit-vector solver based on word-level propagationWang, Wenxi ( 2016)Reasoning with bit-vectors arises in a variety of applications in verification and cryptography. Michel and Van Hentenryck have proposed an interesting approach to bit-vector constraint propagation on the word level. Most of the operations are propagated in constant time, assuming the bit-vector fits in a machine word. In contrast, bit-vector SMT solvers usually solve bit-vector problems by bit-blasting, that is, mapping the resulting operations to conjunctive normal form clauses, and using SAT technology to solve them. This also means generating intermediate variables which can be an advantage, as these can be searched on and learnt about. Since each approach has advantages it is important to see whether we can benefit from these advantages by using a word-level propagation approach with learning. In this dissertation, we describe an approach to bit-vector solving using word-level propagation with learning. We provide alternative word-level propagators to Michel and Van Hentenryck, and we evaluate the variants of the approach empirically. We also experiment with different approaches to learning and back-jumping in the solver. Based on the insights gained, we propose a portfolio solver using machine learning which can enhance state-of-the-art solvers. We show that, with careful engineering, a word-level propagation based approach can compete with (or complement) bit-blasting.