Constraint Satisfaction over Bit-Vectors

Select |




Print


Michel, Laurent; Van Hentenryck, Pascal


2012-10-08


Conference Material


International Conference on Principles and Practice of Constraint Programming (CP)


Quebec, Canada


527-543


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 correcty 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.


http://www.cp2012.org/


nicta:5991


Michel, Laurent; Van Hentenryck, Pascal. Constraint Satisfaction over Bit-Vectors. In: International Conference on Principles and Practice of Constraint Programming (CP); Quebec, Canada. 2012-10-08. 527-543. http://hdl.handle.net/102.100.100/99233?index=1



Loading citation data...

Citation counts
(Requires subscription to view)