Abstract
In this paper, we show how proper benchmarking, which matches day-to-day use of formal methods, allows us to assess direct improvements for SAT use for formal methods. Proper uses of our benchmark allowed us to prove that previous results on tuning SAT solver for Bounded Model Checking (BMC) were overly optimistic and that a simpler algorithm was in fact more efficient.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Accelera. PSL/Sugar LRM.: http://www.eda.org/vfv/
Beer, I., et al.: RuleBase: An Industry Oriented Formal Verification Tool. In: 33rd Design Automation Conference, DAC 1996. ACM/IEEE (1996)
Beer, I., et al.: The Temporal Logic Sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 363. Springer, Heidelberg (2001)
Biere, A., et al.: Symbolic Model Checking Without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)
Biere, A., et al.: Bounded Model Checking. In: Advances in Computers, vol. 58. Academic Press, London (2003) (pre-print)
Cook, S.: The Complexity of Theorem Proving Procedures. In: Proceeding, Third Annual ACM Symp. on the Theory of Computing (1971)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. In: Journal of the ACM, vol. 5(7) (1962)
Een, N., Sorensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Emerson, E., Lei, C.: Modalities for Model Checking: Branching Time Strikes Back. Science of Computer Programming 8, 275–306 (1986)
Goldberg, E., Novikov, Y.: BerkMin: a Fast and Robust SAT-solver. In: Proceedings of the Design, Automation and Test in Europe. DATE 2002 (2002)
Le Berre, D., Simon, L.: The essentials of the SAT 2003 competition. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 468–487. Springer, Heidelberg (2004)
Moskewicz, M., et al.: Chaff: Engineering an Efficient SAT Solver. In: 38th Design Automation Conference, pp. 530–535. ACM/IEEE, NewYork (2001)
Nadel, A.: JeruSAT satisfiablility solver. Available on-line., http://www.geocities.com/alikn78/
Pnueli, A.: A Temporal Logic of Concurrent Programs. Theoretical Computer Science 13, 45–60 (1981)
Shacham, O., Zarpas, E.: Tuning the VSIDS Decision Heuristic for Bounded Model Checking. In: Proceeding of the 4th International Workshop on Microprocessor, Test and Verification. IEEE Computer Society, Austin (2003)
Silva, J., Sakallah, K.: Grasp - a New Search Algorithm for Satisfiability. In: Technical Report TR-CSE-292996, University of Michigan (1996)
Strichman, O.: Tuning SAT Checkers for Bounded Model Checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)
Yang, B., et al.: A Performance Study of BDD-Bases Model Checking. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 255–289. Springer, Heidelberg (1998)
Zhang, L., Malik, S.: The Quest for Efficient Boolean Satisfiability Solvers. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 17. Springer, Heidelberg (2002)
Berkley Logic Interechange Format (BLIF). University of California, Berkley (1992), http://www-cad.eecs.berkeley.edu/Respep/Research/vis/usrDoc.html
IBM Formal Verification Benchmark Library., http://www.haifa.il.ibm.com/projects/verification/RB_Homepage/fvbenchmarks.html
Benchmarks, C.N.F.: 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/bmcbenchmarks_illustrations.html
Web version of the RuleBase User Manual., http://www.haifa.il.ibm.com/projects/verification/RB_Homepage/
RuleBase University Program, http://www.haifa.il.ibm.com/projects/verification/Formal_Methods-Home/university.html
SAT2004 contest., http://satlive.org/SATCompetition/2004/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zarpas, E. (2004). Simple Yet Efficient Improvements of SAT Based Bounded Model Checking. In: Hu, A.J., Martin, A.K. (eds) Formal Methods in Computer-Aided Design. FMCAD 2004. Lecture Notes in Computer Science, vol 3312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30494-4_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-30494-4_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23738-9
Online ISBN: 978-3-540-30494-4
eBook Packages: Springer Book Archive