Robert Brummayer, Armin Biere,
"Consistency Checking of All Different Constraints over Bit-Vectors within a SAT-Solver"
: Proc. 8th Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'08), IEEE, 2008, ISBN: 978-1-4244-2735-2
Original Titel:
Consistency Checking of All Different Constraints over Bit-Vectors within a SAT-Solver
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 8th Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'08)
Original Kurzfassung:
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.
Forschungs-