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

Beschreibung

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

Zeitraum	18 Nov. 2008
Ereignistitel	8th Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'08)
Veranstaltungstyp	Konferenz
Ort	USA/Vereinigte StaatenAuf Karte anzeigen