Title :
BerkMin: A fast and robust SAT-solver
Author :
Goldberg, Evgueni ; Novikov, Yakov
Author_Institution :
Cadence Berkeley Labs. (USA), CA, USA
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 :
backtracking; computability; distributed databases; distributed decision making; logic CAD; tree searching; BerkMin; EDA domain; clause database management; clause recording; conflict analysis; conflict clause aging; conjunctive normal form; decision making procedure; fast BCP; fast robust SAT solver; logic synthesis; microprocessor verification benchmark; nonchronological backtracking; restarts; satisfiability problem; very large CNFs; Automatic test pattern generation; Business continuity; Cities and towns; Databases; Decision making; Electronic design automation and methodology; Identity-based encryption; Logic; Microprocessors; Robustness;
Conference_Titel :
Design, Automation and Test in Europe Conference and Exhibition, 2002. Proceedings
Conference_Location :
Paris
Print_ISBN :
0-7695-1471-5
DOI :
10.1109/DATE.2002.998262
