NDLI: Accelerating an FPGA-Based SAT Solver by Software and Hardware Co-design

Content Provider	IET Digital Library
Author	Ma, Kefan Xiao, Liquan Zhang, Jianmin Li, Tiejun
Abstract	The Boolean Satisfiability (SAT) problem is the key problem in computer theory and application. Field-programmable gate array (FPGA) has been addressed frequently to accelerate the SAT solving process in the last few years owing to its parallelism and flexibility. We have proposed a novel SAT solver based on an improved local search algorithm on the reconfigurable hardware platform. The new software preprocessing procedure and hardware architecture are involved to solve large-scale SAT problems instances. As compared with the past solvers, the proposed solver has the following advantages: the preprocessing technology can strongly improve the efficiency of solver; the strategy of strengthening the variable selection can avoid the same variable flipped continuously and repeatedly. It reduces the possibility of search falling into local minima. The experimental results indicate that the solver can solve problems of up to 32K variables/128K clauses without off-chip memory banks, and has better performance than previous works.
Starting Page	953
Ending Page	961
Page Count	9
ISSN	10224653
Volume Number	28
e-ISSN	20755597
Issue Number	Issue 5, Sep (2019)
Alternate Webpage(s)	https://digital-library.theiet.org/content/journals/cje/28/5
Alternate Webpage(s)	https://digital-library.theiet.org/content/journals/10.1049/cje.2019.06.015
Journal	Chinese Journal of Electronics
Publisher Date	2019-09-01
Access Restriction	Open
Rights Holder	© Chinese Institute of Electronics
Subject Keyword	Boolean Satisfiability Problem Combinatorial Mathematics Computability Computer Architecture Computer Theory Field Programmable Gate Array Field-programmable Gate Array Formal Logic FPGA-based SAT Solver Hardware Architecture Hardware-software Codeign Improved Local Search Algorithm Large-scale SAT Problem Instances Local Minima Logic And Switching Circuit Logic Circuit Novel SAT Solver Optimisation Technique Preprocessing Technology Reconfigurable Architectures Reconfigurable Hardware Platform SAT Solving Process Search Problem Software Preprocessing Procedure Software-hardware Co-design Temperature 128.0 K Temperature 32.0 K Variable Selection
Content Type	Text
Resource Type	Article
Subject	Applied Mathematics Electrical and Electronic Engineering

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

A software/reconfigurable hardware SAT solver

Floating Gate-Based Field Programmable Mixed-Signal Array

High-throughput and compact reconfigurable architectures for recursive filters

FPGA-RPI: A Novel FPGA Architecture With RRAM-Based Programmable Interconnects

Online Fault Tolerance for FPGA Logic Blocks

A Reconfigurable Hardware Architecture for Packet Processing

Floating-Point FPGA: Architecture and Modeling

FPGA PLB Architecture Evaluation and Area Optimization Techniques Using Boolean Satisfiability

Hardware Architectural Support for Caching Partitioned Reconfigurations in Reconfigurable Systems

Accelerating an FPGA-Based SAT Solver by Software and Hardware Co-design

Similar Documents

A software/reconfigurable hardware SAT solver

Floating Gate-Based Field Programmable Mixed-Signal Array

High-throughput and compact reconfigurable architectures for recursive filters

FPGA-RPI: A Novel FPGA Architecture With RRAM-Based Programmable Interconnects

Online Fault Tolerance for FPGA Logic Blocks

A Reconfigurable Hardware Architecture for Packet Processing

Floating-Point FPGA: Architecture and Modeling

FPGA PLB Architecture Evaluation and Area Optimization Techniques Using Boolean Satisfiability

Hardware Architectural Support for Caching Partitioned Reconfigurations in Reconfigurable Systems

Accelerating an FPGA-Based SAT Solver by Software and Hardware Co-design