Skip to Main Content
 

Global Search Box

 
 
 
 

Files

File List


36544.pdf (3.99 MB)

ETD Abstract Container

Abstract Header

FPGA Based Satisfiability Checking

Subramanian, Rishi Bharadwaj
http://orcid.org/0000-0002-7066-3577
http://rave.ohiolink.edu/etdc/view?acc_num=ucin1583154848438753

Abstract Details

2020, MS, University of Cincinnati, Engineering and Applied Science: Computer Engineering.
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.
Ranganadha Vemuri, Ph.D. (Committee Chair)
Wen-Ben Jone, Ph.D. (Committee Member)
Carla Purdy, Ph.D. (Committee Member)
100 p.
Electrical Engineering
FPGA Based SAT Solver; Boolean Satisfiability; Local Search Algorithm; SAT Solver

Recommended Citations

Citations

  • Subramanian, R. B. (2020). FPGA Based Satisfiability Checking [Master's thesis, University of Cincinnati]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=ucin1583154848438753

    APA Style (7th edition)

  • Subramanian, Rishi Bharadwaj. FPGA Based Satisfiability Checking. 2020. University of Cincinnati, Master's thesis. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=ucin1583154848438753.

    MLA Style (8th edition)

  • Subramanian, Rishi Bharadwaj. "FPGA Based Satisfiability Checking." Master's thesis, University of Cincinnati, 2020. http://rave.ohiolink.edu/etdc/view?acc_num=ucin1583154848438753

    Chicago Manual of Style (17th edition)

ucin1583154848438753
455
© 2020, all rights reserved.
This open access ETD is published by University of Cincinnati and OhioLINK.