Reasoning over bit-vectors arises in a variety of applications in verification and cryptography. This paper presents a bit-vector domain for constraint programming and its associated filtering algorithms. The domain supports all the traditional bit operations and correctly models modulo-arithmetic and overflows. The domain implementation uses bit operations of the underlying architecture, avoiding the drawback of a bit-blasting approach that associates a variable with each bit. The filtering algorithms implement either domain consistency on the bit-vector domain or bit consistency, a new consistency notion introduced in this paper. Filtering algorithms for logical and structural constraints typically run in constant time, while arithmetic constraints such as addition run in time linear in the size of the bit-vectors. The paper also discusses how to channel bit-vector variables with an integer variable. © 2012 Springer-Verlag.
CITATION STYLE
Michel, L. D., & Van Hentenryck, P. (2012). Constraint satisfaction over bit-vectors. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7514 LNCS, pp. 527–543). https://doi.org/10.1007/978-3-642-33558-7_39
Mendeley helps you to discover research relevant for your work.