BerkMin: a fast and robust SAT-solver

被引：315

作者：

Goldberg, E ^{[1
]}

Novikov, Y ^{[1
]}

机构：

[1] Cadence Berkeley Labs USA, Berkeley, CA USA

来源：

DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION, 2002 PROCEEDINGS | 2002年

关键词：

D O I：

10.1109/DATE.2002.998262

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：142 / 149

页数：8

共 18 条

[1]

BAPTISTA L, 2000, P AAAI WORKSH LEV PR

[2]

BENSASSON E, 2000, P SAT 2000 3 WORKSH, P14

[3]

BIERE A, 1999, P DES AUT C DAC99

[4]

Brayton R.K., 1984, LOGIC MINIMIZATION A

[5]

BURCH J, 1998, P INT C COMP AID DES

[6] A MACHINE PROGRAM FOR THEOREM-PROVING [J].

DAVIS, M ;

LOGEMANN, G ;

LOVELAND, D .

COMMUNICATIONS OF THE ACM, 1962, 5 (07) :394-397

[7]

DUBOIS O, 1996, 2 DIMACS SERIES DISC, P415

[8]

Freeman J. W., 1995, Improvements to Propositional Satisfiability Search Algorithms

[9] Using SAT for combinational equivalence checking [J].

Goldberg, EI ;

Prasad, MR ;

Brayton, RK .

DESIGN, AUTOMATION AND TEST IN EUROPE, CONFERENCE AND EXHIBITION 2001, PROCEEDINGS, 2001, :114-121

[10]

GOMES CP, 1997, P INT C PRINC PRACT

← 1 2 →