A bit-vector solver with word-level propagation.

*(English)*Zbl 06598678
Quimper, Claude-Guy (ed.), Integration of AI and OR techniques in constraint programming. 13th international conference, CPAIOR 2016, Banff, AB, Canada, May 29 – June 1, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-33953-5/pbk; 978-3-319-33954-2/ebook). Lecture Notes in Computer Science 9676, 374-391 (2016).

Summary: 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. Each of the operations except comparison are 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 paper 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 give the first empirical evaluation of their approach that we are aware of. We show that, with careful engineering, a word-level propagation based approach can compete with (or complement) bit-blasting.

For the entire collection see [Zbl 1337.68017].

For the entire collection see [Zbl 1337.68017].