Consistency Checking of All Different Constraints over Bit-Vectors within a SAT-Solver.

Description

This paper shows how all different constraints (ADCs) over bit-vectors can be handled within a SAT solver. It also contains encouraging experimental results in applying this technique to encode simple path constraints in bounded model checking. Finally, we present a new compact encoding of equalities and inequalities over bit-vectors in CNF

Period	18 Nov 2008
Event title	8th Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'08)
Event type	Conference
Location	United StatesShow on map