FPGA-Based Hardware Acceleration for Boolean Satisfiability

被引：16

作者：

Gulati, Kanupriya ^{[1
]}

Paul, Suganth

Khatri, Sunil P. ^{[1
]}

Patil, Srinivas

Jas, Abhijit

机构：

[1] Texas A&M Univ, College Stn, TX 77843 USA

来源：

ACM TRANSACTIONS ON DESIGN AUTOMATION OF ELECTRONIC SYSTEMS | 2009年 / 14卷 / 02期

关键词：

Performance; Algorithms; Design; Boolean satisfiabilty (SAT); boolean constant propagation (BCP); conflict induced clauses; non-chronological backtrack; FPGA;

D O I：

10.1145/1497561.1497576

中图分类号：

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

学科分类号：

0812 ;

摘要：

We present an FPGA-based hardware solution to the Boolean satisfiability (SAT) problem, with the main goals of scalability and speedup. In our approach the traversal of the implication graph as well as conflict clause generation are performed in hardware, in parallel. The experimental results and their analysis, along with the performance models are discussed. We show that an order of magnitude improvement in runtime can be obtained over MiniSAT (the best-in-class software based approach) by using a Virtex-4 (XC4VFX140) FPGA device. The resulting system can handle instances with as many as 10K variables and 280K clauses.

引用

页数：11

共 18 条

[1]

ABRAMOVICI M, 1999, DES AUT C, P684

[2]

Cook S. A., 1971, P 3 ANN ACM S THEOR, P151, DOI [10.1145/800157.805047, DOI 10.1145/800157.805047]

[3] BerkMin: a fast and robust SAT-solver [J].

Goldberg, E ;

Novikov, Y .

DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION, 2002 PROCEEDINGS, 2002, :142-149

[4]

GU J, 1997, DIMACS SERIES DISCRE, P19

[5] Efficient, scalable hardware engine for Boolean satisfiability and unsatisfiable core extraction [J].

Gulati, K. ;

Waghmode, M. ;

Khatri, S. P. ;

Shi, W. .

IET COMPUTERS AND DIGITAL TECHNIQUES, 2008, 2 (03) :214-229

[6]

MENCER O, 1999, P 32 ANN HAUB INT C, P3044

[7]

Moskewicz MW, 2001, DES AUT CON, P530, DOI 10.1109/DAC.2001.935565

[8] Parallel and scalable architecture for solving SATisfiability on reconfigurable FPGA [J].

Pagarani, T ;

Kocan, F ;

Saab, DG ;

Abraham, JA .

PROCEEDINGS OF THE IEEE 2000 CUSTOM INTEGRATED CIRCUITS CONFERENCE, 2000, :147-150

[9]

Platzner M., 1998, Field-Programmable Logic and Applications. From FPGAs to Computing Paradigm. 8th International Workshop, FPL'98. Proceedings, P69, DOI 10.1007/BFb0055234

[10]

REDEKOPP M, 2000, P 10 INT C FIELD PRO, P462

← 1 2 →