BerkMin: A fast and robust SAT-solver
Top Cited Papers
- 25 June 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 48 (15301591) , 142-149
- https://doi.org/10.1109/date.2002.998262
Abstract
We describe a SAT-solver, BerkMin, that inherits such features of GRASP, SATO, and Chaff as clause recording, fast BCP, restarts, and conflict clause "aging". At the same time BerkMin introduces a new decision making procedure and a new method of clause database management. We experimentally compare BerkMin with Chaff, the leader among SAT-solvers used in the EDA domain. Experiments show that our solver is more robust than Chaff. BerkMin solved all the instances we used in experiments including very large CNFs from a microprocessor verification benchmark suite. On the other hand, Chaff was not able to complete some instances even with the timeout limit of 16 hours.Keywords
This publication has 8 references indexed in Scilit:
- Symbolic model checking using SAT procedures instead of BDDsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Tight integration of combinational verification methodsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Using SAT for combinational equivalence checkingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A constraint-based approach to narrow search trees for satisfiabilityInformation Processing Letters, 1999
- GRASP: a search algorithm for propositional satisfiabilityIEEE Transactions on Computers, 1999
- SAT versus UNSATPublished by American Mathematical Society (AMS) ,1996
- Combinational test generation using satisfiabilityIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1996
- A machine program for theorem-provingCommunications of the ACM, 1962