NDLI: Variable and clause elimination in SAT problems using an FPGA

Content Provider	IEEE Xplore Digital Library
Author	Suzuki, M. Maruyama, T.
Copyright Year	2011
Description	Author affiliation: Systems and Information Engineering, University of Tsukuba 1-1-1 Ten-ou-dai Tsukuba Ibaraki 305-8573 Japan (Suzuki, M.; Maruyama, T.)
Abstract	The satisfiability (SAT) problem is to find an assignment of binary values to the variables which satisfy a given clausal normal form (CNF). Many practical application problems can be transformed to SAT problems, and many SAT solvers have been developed. SAT problem is, however, NP-complete and its computational cost is very high. In order to reduce the computational cost, preprocessors are widely used by SAT solvers. In this paper, we describe an approach for implementing a preprocessor (SatELite) on FPGA. In SatELite, the variables and clauses whose values can be uniquely determined from other variables and clauses are eliminated to reduce the search space of the given SAT problem. The algorithms used in SatELite have inherent parallelism, but the data size of the SAT problems is very large, and the performance of the system is limited by the throughput of the off-chip DRAM banks. In our implementation, several clauses are held on the FPGA, and are compared in parallel with a sequence of new clauses. The sequence is cached on the FPGA, and reused in order to hide the access delay to the DRAM banks. The speedup by our system depends on the problem size, however it becomes higher for larger problems.
Starting Page	1
Ending Page	8
File Size	255415
Page Count	8
File Format	PDF
ISBN	9781457717413
e-ISBN	9781457717406
DOI	10.1109/FPT.2011.6132681
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2011-12-12
Publisher Place	India
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Field programmable gate arrays Random access memory Benchmark testing Hardware Delay Data structures Software
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Just-in-time compilation for FPGA processor cores

Solving Sudokus through an incidence matrix on an FPGA

An FPGA Solver for SAT-Encoded Formal Verification Problems

FPGA acceleration of SAT/Max-SAT solving using variable-way cache

Relieving capacity limits on FPGA-based SAT-solvers

A Compact Transactional Memory Multiprocessor System on FPGA

GraphGen: An FPGA Framework for Vertex-Centric Graph Computation

An FPGA-based multi-core platform for testing and analysis of architectural techniques

A SAT solver using software and reconfigurable hardware

Variable and clause elimination in SAT problems using an FPGA

Similar Documents

Just-in-time compilation for FPGA processor cores

Solving Sudokus through an incidence matrix on an FPGA

An FPGA Solver for SAT-Encoded Formal Verification Problems

FPGA acceleration of SAT/Max-SAT solving using variable-way cache

Relieving capacity limits on FPGA-based SAT-solvers

A Compact Transactional Memory Multiprocessor System on FPGA

GraphGen: An FPGA Framework for Vertex-Centric Graph Computation

An FPGA-based multi-core platform for testing and analysis of architectural techniques

A SAT solver using software and reconfigurable hardware

Variable and clause elimination in SAT problems using an FPGA