Abstract
Modern SAT solvers are highly dependent on heuristics. Therefore, benchmarking is of prime importance in evaluating the performances of different solvers. However, relevant benchmarking is not necessarily straightforward. We present our experiments using the IBM CNF Benchmark on several SAT solvers. Using the results, we attempt to define guidelines for a relevant benchmarking methodology, using SAT solvers for real life BMC applications.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Biere, A., et al.: Symbolic Model Checking Without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)
Goldberg, E., Novikov, Y.: BerkMin: a Fast and Robust SAT-solver. In: Proc. of the Design, Automation and Test in Europe. IEEE Computer Society, Los Alamitos (2002)
Mahajan, Y., Fu, Z., Malik, S.: Zchaff2004: An Efficient SAT Solver. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 360–375. Springer, Heidelberg (2005)
Le Berre, D., Simon, L.: The essentials of the SAT 2003 competition. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 452–467. Springer, Heidelberg (2004)
Le Berre, D., Simon, L.: SAT 2003 contest results (2003), http://www.lri.fr/simon/contest03/results/
Le Berre, D., Simon, L.: 55 Solvers in Vancouver: The SAT 2004 competition. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 321–344. Springer, Heidelberg (2005)
Moskewicz, M., et al.: Chaff: Engineering an Efficient SAT Solver. In: 38th Design Automation Conference. ACM/IEEE (2001)
Ryan, L.: The siege satisfiability solver, http://www.cs.sfu.ca/~loryan/personal/
Shacham, O., Zarpas, E.: Tuning the VSIDS Decision Heuristic for Bounded Model Checking. In: Proc. of the 4th International Workshop on Microprocessor, Test and Verification. IEEE Computer Society, Los Alamitos (2003)
Van Gelder, A., Tsuji, Y.K.: Satisfiability Testing with More Reasoning and Less Guessing. In: Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge. American Mathematical Society, Providence (1996)
Zarpas, E.: Simple yet efficient improvements of SAT based Bounded Model Checking. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 174–185. Springer, Heidelberg (2004)
CNF Benchmarks from IBM Formal Verification Benchmarks Library, http://www.haifa.il.ibm.com/projects/verification/RB_Homepage/bmcbenchmarks.html
IBM CNF Benchmark Illustration, http://www.haifa.il.ibm.com/projects/verification/RB_Homepage/papers/comparaison2.zip
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zarpas, E. (2005). Benchmarking SAT Solvers for Bounded Model Checking. In: Bacchus, F., Walsh, T. (eds) Theory and Applications of Satisfiability Testing. SAT 2005. Lecture Notes in Computer Science, vol 3569. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11499107_25
Download citation
DOI: https://doi.org/10.1007/11499107_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26276-3
Online ISBN: 978-3-540-31679-4
eBook Packages: Computer ScienceComputer Science (R0)