Evaluation of Cardinality Constraints on SMT-Based Debugging

11 years 5 months ago
Evaluation of Cardinality Constraints on SMT-Based Debugging
For formal verification of hardware Satisfiability Modulo Theory (SMT) solvers are increasingly applied. Today’s state-of-the-art SMT solvers use different techniques like term-rewriting, abstraction, or bit-blasting. The performance does not only depend on the underlying decision problem but also on the encoding of the original problem into an SMT instance. In this work, encodings for cardinality constraints in SMT are investigated. Three different encodings are considered: an adder network, an encoding with multiplexors, and a newly proposed encoding with shifters. The encodings are analyzed with respect to size and complexity. The experimental evaluation on debugging instances that contain cardinality constraints shows the strong influence of the encoding on the resulting run-times.
André Sülflow, Robert Wille, Görs
Added 24 May 2010
Updated 24 May 2010
Type Conference
Year 2009
Authors André Sülflow, Robert Wille, Görschwin Fey, Rolf Drechsler
Comments (0)