BerkMin: A fast and robust SAT-solver

Author

Goldberg, Evgueni ; Novikov, Yakov

Author_Institution

Cadence Berkeley Labs. (USA), CA, USA

fYear

2002

fDate

2002

Firstpage

142

Lastpage

149

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Design, Automation and Test in Europe Conference and Exhibition, 2002. Proceedings

Conference_Location

Paris

ISSN

1530-1591

Print_ISBN

0-7695-1471-5

Type

conf

DOI

10.1109/DATE.2002.998262

Filename

998262