BerkMin: A Fast and Robust Sat-Solver

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.

• Type: Conference
• Year: 2002
• Where: DATE
• Authors: Evguenii I. Goldberg, Yakov Novikov
• Keywords: Chaff, Clause Database Management, Conflict Clause, DATE 2002, Hardware