國立虎尾科技大學 |

FPGA Based Satisfiability Checking.

Record Type:	Language materials, printed : Monograph/item
Title/Author:	FPGA Based Satisfiability Checking./
Author:	Subramanian, Rishi Bharadwaj.
Published:	Ann Arbor : ProQuest Dissertations & Theses, : 2020,
Description:	103 p.
Notes:	Source: Masters Abstracts International, Volume: 82-03.
Contained By:	Masters Abstracts International82-03.
Subject:	Electrical engineering. -
Online resource:	http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=28108094
ISBN:	9798662503311

FPGA Based Satisfiability Checking.
Subramanian, Rishi Bharadwaj.

FPGA Based Satisfiability Checking. - Ann Arbor : ProQuest Dissertations & Theses, 2020 - 103 p.

Source: Masters Abstracts International, Volume: 82-03.

Thesis (M.S.)--University of Cincinnati, 2020.

This item must not be sold to any third party vendors.

The Boolean satisfiability problem, abbreviated as SAT, is the backbone of many applications in VLSI design automation and verification. Over the years, many SAT solvers, both complete and incomplete, have been developed. Complete solvers are usually based on the DPLL (Davis–Putnam–Logemann–Loveland) algorithm, which is a backtracking algorithm. Industrial strength problems are very large and make DPLL based solvers impractical for some applications. In such cases, local search algorithms that try to find a solution within a stipulated time can be used. These algorithms look at SAT problem as an optimization problem. They start with an initial random solution and explore a certain search space by iteratively making local changes to the solution using a greedy, heuristic algorithm to find a global optimum.Over the past few years, heterogeneous devices such as Graphics Processing Units (GPU) and Field Programmable Gate Arrays (FPGA) have been used to accelerate the SAT problem and handle large SAT instances. There has been a growing interest in exploiting the parallel and pipeline processing power of FPGAs for various applications. New process technologies have allowed for more logic blocks, memory elements, and faster FPGAs, making it a perfect candidate for parallel computing. This thesis presents a local search algorithm Walksat, implemented on the Xilinx Alveo U250 Accelerator card. The entire solver has been developed using the OpenCL framework. On-chip memory available on the FPGA has been exploited to a great extent and the solver can handle SAT problems of up to 98,000 variables and 401,800 clauses. We have also analyzed the performance of our solver against the state of the art complete and incomplete solvers.

ISBN: 9798662503311Subjects--Topical Terms:

596380
Electrical engineering.
Subjects--Index Terms:

FPGA based SAT solver

FPGA Based Satisfiability Checking.
LDR:02867nam a2200361 4500 001 1038040
005 20210910100701.5
008 211029s2020 ||||||||||||||||| ||eng d
020 $a 9798662503311
035 $a (MiAaPQ)AAI28108094
035 $a (MiAaPQ)OhioLINKucin1583154848438753
035 $a AAI28108094
040 $a MiAaPQ $c MiAaPQ
100 1 $a Subramanian, Rishi Bharadwaj. $3 1335373
245 1 0 $a FPGA Based Satisfiability Checking.
260 1 $a Ann Arbor : $b ProQuest Dissertations & Theses, $c 2020
300 $a 103 p.
500 $a Source: Masters Abstracts International, Volume: 82-03.
500 $a Advisor: Vemuri, Ranganadha.
502 $a Thesis (M.S.)--University of Cincinnati, 2020.
506 $a This item must not be sold to any third party vendors.
520 $a The Boolean satisfiability problem, abbreviated as SAT, is the backbone of many applications in VLSI design automation and verification. Over the years, many SAT solvers, both complete and incomplete, have been developed. Complete solvers are usually based on the DPLL (Davis–Putnam–Logemann–Loveland) algorithm, which is a backtracking algorithm. Industrial strength problems are very large and make DPLL based solvers impractical for some applications. In such cases, local search algorithms that try to find a solution within a stipulated time can be used. These algorithms look at SAT problem as an optimization problem. They start with an initial random solution and explore a certain search space by iteratively making local changes to the solution using a greedy, heuristic algorithm to find a global optimum.Over the past few years, heterogeneous devices such as Graphics Processing Units (GPU) and Field Programmable Gate Arrays (FPGA) have been used to accelerate the SAT problem and handle large SAT instances. There has been a growing interest in exploiting the parallel and pipeline processing power of FPGAs for various applications. New process technologies have allowed for more logic blocks, memory elements, and faster FPGAs, making it a perfect candidate for parallel computing. This thesis presents a local search algorithm Walksat, implemented on the Xilinx Alveo U250 Accelerator card. The entire solver has been developed using the OpenCL framework. On-chip memory available on the FPGA has been exploited to a great extent and the solver can handle SAT problems of up to 98,000 variables and 401,800 clauses. We have also analyzed the performance of our solver against the state of the art complete and incomplete solvers.
590 $a School code: 0045.
650 4 $a Electrical engineering. $3 596380
650 4 $a Computer engineering. $3 569006
653 $a FPGA based SAT solver
653 $a Boolean satisfiability
653 $a Local search algorithm
653 $a SAT solver
690 $a 0544
690 $a 0464
710 2 $a University of Cincinnati. $b Engineering and Applied Science: Computer Engineering. $3 1191054
773 0 $t Masters Abstracts International $g 82-03.
790 $a 0045
791 $a M.S.
792 $a 2020
793 $a English
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=28108094